Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable specifying a dependency while staying agnostic of its dependencies #3005

Open
keyboardDrummer opened this issue Nov 7, 2022 · 0 comments
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Nov 7, 2022

If there's a chain of Dafny library dependencies, where a Dafny application or library A, depends on a library B, which depends on a library C, then it should be possible for A to declare its dependency on B without having to know about C.

How

  • Enable the --library option to take a Dafny project file
  • If --library is called with the exact same Dafny project multiple times, either directly or indirectly through a dependency, then those are deduplicated. If two arguments of --library are not exactly the same but contain root level modules with the same name, then a compilation error occurs.

Prerequisites

@keyboardDrummer keyboardDrummer added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line labels Nov 7, 2022
@keyboardDrummer keyboardDrummer changed the title [Feature request]: enable specifying a dependency on a Dafny library without having to take into account the library's dependencies [Feature request]: enable specifying a dependency while staying agnostic of its dependencies Nov 7, 2022
@keyboardDrummer keyboardDrummer changed the title [Feature request]: enable specifying a dependency while staying agnostic of its dependencies Enable specifying a dependency while staying agnostic of its dependencies Nov 7, 2022
@keyboardDrummer keyboardDrummer added this to the Library support milestone Nov 7, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line
Projects
None yet
Development

No branches or pull requests

1 participant