Standard libraries and separate compilation #5981
Conversation
There was a problem hiding this comment.
Love the option, just quibbling about default behavior and documentation.
I think it's worth mentioning this option in https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md too, so users are more likely to discover it.
| if (options.Backend is LibraryBackend) { | ||
| options.Set(CommonOptionBag.TranslateStandardLibrary, false); | ||
| } | ||
|
|
||
| // For now the standard libraries are still translated from scratch. | ||
| // This breaks separate compilation and will be addressed in https://github.com/dafny-lang/dafny/pull/4877 |
There was a problem hiding this comment.
I think you're addressing "this breaks separate compilation" with this change so just that part of the comment can be removed, although I think the rest still applies (although I think we might publish the libraries separately rather than embed them in the runtimes)
| if (Options.Backend is LibraryBackend) { | ||
| Options.Set(CommonOptionBag.TranslateStandardLibrary, false); | ||
| } | ||
|
|
||
| // For now the standard libraries are still translated from scratch. | ||
| // This breaks separate compilation and will be addressed in https://github.com/dafny-lang/dafny/pull/4877 |
| @@ -102,6 +102,7 @@ static DafnyCommands() { | |||
| CommonOptionBag.NewTypeInferenceDebug, | |||
| Method.ReadsClausesOnMethods, | |||
| CommonOptionBag.UseStandardLibraries, | |||
| CommonOptionBag.TranslateStandardLibrary, | |||
There was a problem hiding this comment.
Shouldn't it be a translation option? It doesn't make sense to pass this to resolve or verify
| @"Currently Dafny does not prevent separately built Dafny projects from each including the standard library, | ||
| leading to conflicts. When combining such projects, please ensure that only one of them has --translate-standard-library set to true. |
There was a problem hiding this comment.
The first sentence feels overly defensive to me, but it might be because we see the current state differently. I don't think it's inherently wrong to merge doo files personally, building larger aggregate libraries, as long as you don't use them incorrectly.
| public static readonly Option<bool> TranslateStandardLibrary = new("--translate-standard-library", () => true, | ||
| @"Currently Dafny does not prevent separately built Dafny projects from each including the standard library, | ||
| leading to conflicts. When combining such projects, please ensure that only one of them has --translate-standard-library set to true. | ||
| When building a Dafny library (.doo file), this option will automatically be set to false. |
There was a problem hiding this comment.
This feels like it's going to be confusing and hard to debug, especially since it's a change in behavior. Wouldn't it be better to fail instead, and make users set --translate-standard-library:false explicitly?
Fixes dafny-lang/dafny-gradle-plugin#11
What was changed?
--translate-standard-librarythat enables using--standard-librariesin conjunction with separate compilationHow has this been tested?
comp/separate-compilation/standard-libaries/user.dfyBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.