Add —default-module, unify Makefile testing in CI

.github/workflows/runtime-tests.yml → .github/workflows/make-tests.yml

@@ -1,4 +1,4 @@
-name: Build and Test Dafny Runtimes
+name: Run Makefile-based tests
 
 on:
   workflow_dispatch:
@@ -13,12 +13,23 @@ jobs:
   check-deep-tests:
      uses: ./.github/workflows/check-deep-tests-reusable.yml
 
-  build:
+  run-make-tests:
     needs: check-deep-tests
     if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
 
     runs-on: ubuntu-latest
-
+    strategy:
+      matrix:
+        project: [
+          DafnyCore,
+          DafnyRuntime,
+          DafnyRuntime/DafnyRuntimeDafny,
+          DafnyRuntime/DafnyRuntimeGo,
+          DafnyRuntime/DafnyRuntimeJava,
+          DafnyRuntime/DafnyRuntimePython,
+          DafnyRuntime/DafnyRuntimeJs
+        ]
+      fail-fast: false
     steps:
       - name: Checkout Dafny
         uses: actions/checkout@v4
@@ -33,32 +44,7 @@ jobs:
         run: dotnet build Source/Dafny.sln
       - name: Get Z3
         run: make z3-ubuntu
-      - name: Test DafnyCore
+      - name: Test ${{ matrix.project }}
         run: |
-          cd ./Source/DafnyCore
+          cd ./Source/${{ matrix.project }}
           make test
-          make check-format
-      - name: Test DafnyRuntime (C#)
-        run: |
-          cd ./Source/DafnyRuntime
-          make all
-      - name: Test DafnyRuntimeDafny
-        run: |
-          cd ./Source/DafnyRuntime/DafnyRuntimeDafny
-          make all
-      - name: Test DafnyRuntimeGo
-        run: |
-          cd ./Source/DafnyRuntime/DafnyRuntimeGo
-          make all
-      - name: Test DafnyRuntimeJava
-        run: |
-          cd ./Source/DafnyRuntime/DafnyRuntimeJava
-          make all
-      - name: Test DafnyRuntimePython
-        run: |
-          cd ./Source/DafnyRuntime/DafnyRuntimePython
-          make all
-      - name: Test DafnyRuntimeJs
-        run: |
-          cd ./Source/DafnyRuntime/DafnyRuntimeJs
-          make all

Source/DafnyCore/AST/ShouldCompileOrVerify.cs

@@ -13,17 +13,21 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p
     }
 
     if (module.FullName == "_System") {
-      return program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.Omit;
+      return program.Options.SystemModuleTranslationMode != CommonOptionBag.ModuleTranslationMode.Omit;
     }
-    if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+    if (program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
       return false;
     }
 
     if (module is DefaultModuleDefinition) {
       // If things from precompiled files live in the default module, that can cause downstream compilation issues:
       // https://github.com/dafny-lang/dafny/issues/4009
-      return true;
+      return program.Options.DefaultModuleTranslationMode != CommonOptionBag.ModuleTranslationMode.Omit;
+    }
+    if (program.Options.DefaultModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
+      return false;
     }
+
     return program.UrisToCompile.Contains(module.Tok.Uri);
   }
 

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -73,21 +73,21 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       wr.WriteLine("// Optionally, you may want to include compiler switches like");
       wr.WriteLine("//     /debug /nowarn:162,164,168,183,219,436,1717,1718");
       wr.WriteLine();
-      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
       wr.WriteLine("using System;");
       wr.WriteLine("using System.Numerics;");
       wr.WriteLine("using System.Collections;");
-      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
         wr.WriteLine("#endif");
       }
       Synthesize = ProgramHasMethodsWithAttr(program, "synthesize");
       if (Synthesize) {
         CsharpSynthesizer.EmitImports(wr);
       }
 
-      if (program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (program.Options.SystemModuleTranslationMode != CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
         EmitDafnySourceAttribute(program, wr);
       }
 
@@ -131,11 +131,11 @@ void EmitDafnySourceAttribute(Program program, ConcreteSyntaxTree wr) {
 
     protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
       switch (Options.SystemModuleTranslationMode) {
-        case CommonOptionBag.SystemModuleMode.Omit: {
+        case CommonOptionBag.ModuleTranslationMode.Omit: {
             CheckCommonSytemModuleLimits(systemModuleManager);
             break;
           }
-        case CommonOptionBag.SystemModuleMode.OmitAllOtherModules: {
+        case CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules: {
             CheckSystemModulePopulatedToCommonLimits(systemModuleManager);
             break;
           }
@@ -150,7 +150,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
       // so they don't become duplicates when --include-runtime is used.
       // See comment at the top of DafnyRuntime.cs.
 
-      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
 
@@ -161,7 +161,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
       }
       EmitFuncExtensions(systemModuleManager, wr);
 
-      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
         wr.WriteLine("#endif");
       }
     }

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -312,11 +312,11 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
 
     protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
       switch (Options.SystemModuleTranslationMode) {
-        case CommonOptionBag.SystemModuleMode.Omit: {
+        case CommonOptionBag.ModuleTranslationMode.Omit: {
             CheckCommonSytemModuleLimits(systemModuleManager);
             return;
           }
-        case CommonOptionBag.SystemModuleMode.OmitAllOtherModules: {
+        case CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules: {
             CheckSystemModulePopulatedToCommonLimits(systemModuleManager);
             break;
           }

Source/DafnyCore/DafnyOptions.cs

@@ -302,7 +302,8 @@ public enum IncludesModes {
     public IncludesModes PrintIncludesMode = IncludesModes.None;
     public int OptimizeResolution = 2;
     public bool IncludeRuntime = true;
-    public CommonOptionBag.SystemModuleMode SystemModuleTranslationMode = CommonOptionBag.SystemModuleMode.Omit;
+    public CommonOptionBag.ModuleTranslationMode SystemModuleTranslationMode = CommonOptionBag.ModuleTranslationMode.Omit;
+    public CommonOptionBag.ModuleTranslationMode DefaultModuleTranslationMode = CommonOptionBag.ModuleTranslationMode.Include;
     public bool UseJavadocLikeDocstringRewriter = false;
     public bool DisableScopes = false;
     public bool UseStdin = false;

Source/DafnyCore/Makefile

@@ -16,8 +16,10 @@ build-regenerated-from-dafny:
 	chmod u+x DafnyGeneratedFromDafny.sh
 	./DafnyGeneratedFromDafny.sh $(REGENERATED_FROM_DAFNY)
 
-test: build-regenerated-from-dafny
+check-regenerated-from-dafny: build-regenerated-from-dafny
 	(diff $(GENERATED_FROM_DAFNY).cs $(REGENERATED_FROM_DAFNY).cs && (echo 'Consider running ./DafnyGeneratedFromDafny.sh GeneratedFromDafny'))
 
 check-format:
 	../../Scripts/dafny format . --check
+
+test: check-regenerated-from-dafny check-format

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -236,15 +236,20 @@ May slow down verification slightly.
     IsHidden = true
   };
 
-  public enum SystemModuleMode {
+  public enum ModuleTranslationMode {
     Include,
     Omit,
     // Used to pre-compile the System module into the runtimes
     OmitAllOtherModules
   }
 
-  public static readonly Option<SystemModuleMode> SystemModule = new("--system-module", () => SystemModuleMode.Omit,
-    "How to handle the built-in _System module.") {
+  public static readonly Option<ModuleTranslationMode> SystemModule = new("--system-module", () => ModuleTranslationMode.Omit,
+    "How to translate the built-in _System module.") {
+    IsHidden = true
+  };
+
+  public static readonly Option<ModuleTranslationMode> DefaultModule = new("--default-module", () => ModuleTranslationMode.Include,
+    "How to translate the default module.") {
     IsHidden = true
   };
 
@@ -400,6 +405,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DafnyOptions.RegisterLegacyBinding(IncludeRuntimeOption, (options, value) => { options.IncludeRuntime = value; });
     DafnyOptions.RegisterLegacyBinding(InternalIncludeRuntimeOptionForExecution, (options, value) => { options.IncludeRuntime = value; });
     DafnyOptions.RegisterLegacyBinding(SystemModule, (options, value) => { options.SystemModuleTranslationMode = value; });
+    DafnyOptions.RegisterLegacyBinding(DefaultModule, (options, value) => { options.DefaultModuleTranslationMode = value; });
     DafnyOptions.RegisterLegacyBinding(UseBaseFileName, (o, f) => o.UseBaseNameForFileName = f);
     DafnyOptions.RegisterLegacyBinding(UseJavadocLikeDocstringRewriterOption,
       (options, value) => { options.UseJavadocLikeDocstringRewriter = value; });
@@ -517,7 +523,8 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       UseStandardLibraries,
       OptimizeErasableDatatypeWrapper,
       AddCompileSuffix,
-      SystemModule
+      SystemModule,
+      DefaultModule
     );
   }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -53,7 +53,8 @@ static DafnyCommands() {
     CommonOptionBag.TestAssumptions,
     DeveloperOptionBag.Bootstrapping,
     CommonOptionBag.AddCompileSuffix,
-    CommonOptionBag.SystemModule
+    CommonOptionBag.SystemModule,
+    CommonOptionBag.DefaultModule
   }.Concat(VerificationOptions).ToList();
 
   public static IReadOnlyList<Option> ExecutionOptions = new Option[] {

Source/DafnyRuntime/DafnyRuntimeDafny/Makefile

@@ -8,7 +8,7 @@ SOURCES=$(shell find $(SOURCE_DIR) -name '*.dfy')
 GENERATED_CODE_GO_SOURCE=src/dafnyRuntimeGo-go/src/dafny/dafny.go
 GENERATED_CODE_GO_TARGET=../DafnyRuntimeGo/dafny/dafnyFromDafny.go
 
-all: test check-format
+test: verify check-go check-format
 
 verify:
 	$(DAFNY) verify $(SOURCES)
@@ -22,8 +22,6 @@ check-go: build-go
 update-go: build-go
 	cp $(GENERATED_CODE_GO_SOURCE) $(GENERATED_CODE_GO_TARGET)
 
-test: check-go
-
 format:
 	$(DAFNY) format .
 

Source/DafnyRuntime/DafnyRuntimeGo/Makefile

@@ -8,9 +8,9 @@ GENERATED_SYSTEM_MODULE_TARGET=System_/System_.go
 GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-go/src
 GENERATED_STDLIBS_TARGET=.
 
-all: check-system-module check-stdlibs test
+test: check-system-module check-stdlibs go-tests
 
-test:
+go-tests:
 	cd dafny &&	GO111MODULE=auto go test
 
 build-system-module:
@@ -23,8 +23,7 @@ update-system-module: build-system-module
 	cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)
 
 build-stdlibs:
-	$(DAFNY) translate go --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
-	rm $(GENERATED_STDLIBS_SOURCE)/DafnyStandardLibraries.go
+	$(DAFNY) translate go --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false  --default-module:Omit ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
 
 check-stdlibs: build-stdlibs
 	diff -r -x Makefile -x System_ -x dafny $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET)

Source/DafnyRuntime/DafnyRuntimeJava/Makefile

@@ -11,9 +11,9 @@ GENERATED_DAFNY_MODULE_TARGET=src/main/dafny-generated/dafny
 GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-java/DafnyStdLibs
 GENERATED_STDLIBS_TARGET=src/main/dafny-generated/DafnyStdLibs
 
-all: check-system-module check-stdlibs test
+test: check-system-module check-stdlibs gradle-tests
 
-test:
+gradle-tests:
 	./gradlew test
 
 # TODO: Add --optimize-erasable-datatype-wrapper:false elsewhere too
@@ -31,7 +31,7 @@ update-system-module: build-system-module
 	cp -r $(GENERATED_DAFNY_MODULE_SOURCE) $(GENERATED_DAFNY_MODULE_TARGET)
 
 build-stdlibs:
-	$(DAFNY) translate java --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
+	$(DAFNY) translate java --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --default-module:Omit ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
 
 check-stdlibs: build-stdlibs
 	diff $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET)

Source/DafnyRuntime/DafnyRuntimeJs/Makefile

@@ -5,10 +5,10 @@ DAFNY = dotnet run --project ../../Dafny --no-build --
 GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator.js
 GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.js
 
-GENERATED_STDLIBS_SOURCE=obj/DafnyStandardLibraries.js
+GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries.js
 GENERATED_STDLIBS_TARGET=DafnyStandardLibraries.js
 
-all: check-system-module check-stdlibs
+test: check-system-module check-stdlibs
 
 build-system-module:
 	$(DAFNY) translate js --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
@@ -20,7 +20,7 @@ update-system-module: build-system-module
 	cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)
 
 build-stdlibs:
-	$(DAFNY) translate js --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
+	$(DAFNY) translate js --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --default-module:Omit ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
 
 check-stdlibs: build-stdlibs
 	diff $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET)

Source/DafnyRuntime/DafnyRuntimePython/Makefile

@@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=System_.py
 GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-py
 GENERATED_STDLIBS_TARGET=.
 
-all: check-system-module check-stdlibs
+test: check-system-module check-stdlibs
 
 build-system-module:
 	$(DAFNY) translate py --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator
@@ -20,10 +20,10 @@ update-system-module: build-system-module
 	cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)
 
 build-stdlibs:
-	$(DAFNY) translate py --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
+	$(DAFNY) translate py --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --default-module:Omit ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries
 
 check-stdlibs: build-stdlibs
-	diff -r -x Makefile -x System_.py -x _dafny.py -x __main__.py -x module_.py $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET)
+	diff -r -x Makefile -x System_.py -x _dafny.py -x __main__.py $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET)
 
 update-stdlibs: build-stdlibs
 	rsync -rt $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs* $(GENERATED_STDLIBS_TARGET)

Source/DafnyRuntime/Makefile

@@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.cs
 GENERATED_STDLIBS_SOURCE=obj/DafnyStandardLibraries.cs
 GENERATED_STDLIBS_TARGET=DafnyStandardLibraries.cs
 
-all: check-system-module check-stdlibs
+test: check-system-module check-stdlibs
 
 build-system-module:
 	$(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --system-module:OmitAllOtherModules systemModulePopulator.dfy --output:obj/systemModulePopulator
@@ -20,7 +20,7 @@ update-system-module: build-system-module
 	cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)
 
 build-stdlibs:
-	$(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../DafnyStandardLibraries/src/dfyconfig.toml --output:obj/DafnyStandardLibraries.cs
+	$(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --default-module:Omit ../DafnyStandardLibraries/src/dfyconfig.toml --output:obj/DafnyStandardLibraries.cs
 
 check-stdlibs: build-stdlibs
 	diff $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET)