feat: Legacy module names option #5679
Conversation
| // Use an "underscore-escaped" character as a module name separator, since | ||
| // underscores are already used as escape characters in SanitizeName() | ||
| compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name); | ||
| if (options.Get(LegacyModuleNames)) { |
There was a problem hiding this comment.
We should make it so that read translation record options are automatically stored in the module specific options that are attached to ModuleDecl, and then let the options here be those module specific options, so that if a Dafny 4.7 project that does not use --legacy-module-names, imports a Dafny 4.7 project that does use --legacy-module-names, it still works.
There was a problem hiding this comment.
I had that in mind as a future improvement when I added translation records too.
|
The build failure is because the property // This is primarily here to exclude prefix modules
// (e.g. something like A.B that only appears in a module A.B.C { ... } declaration)
// since those can appear in multiple separately-compiled projects.
if (ModuleEmptyForCompilation(module)) {
continue;
}I'm having a bit of a blackout with regards to coming up with a good solution :D Can you refresh my memory on the use-case that was problematic here? Why do different projects need to have outermost modules with the same name? We also had issues with collisions of declarations in the default module right? Should projects have a name, which serves like an |
|
Fixed the build by avoiding the empty parent module in the test, since it's not directly relevant to the new option. But it's a valid concern so I cut #5683 for follow up. |
Description
Similar to the previously added
--legacy-data-constructorsoption,--legacy-module-namesoutputs module names in the schemeA_mB_mC, as previous versions of Dafny did, instead ofA.B.C, in the name of backwards compatibility with other Dafny-generated consumers.How has this been tested?
Updated
comp/separate-compilation/usesTimesTwo-oldDafnyCompatibility.dfyto use a nested library module name, and therefore test both--legacy-data-constructorsand--legacy-module-names.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.