Bundle stdlibs with runtimes

.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,24 @@ 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,
+          DafnyStandardLibraries
+        ]
+      fail-fast: false
     steps:
       - name: Checkout Dafny
         uses: actions/checkout@v4
@@ -33,32 +45,8 @@ jobs:
         run: dotnet build Source/Dafny.sln
       - name: Get Z3
         run: make z3-ubuntu
-      - name: Test DafnyCore
+      - run: npm install bignumber.js
+      - 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

@@ -66,28 +66,32 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
     }
 
     protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
+      var isPartialTranslate =
+        program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules
+        || program.Options.DefaultModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.Omit;
+
       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
       wr.WriteLine("// To recompile, you will need the libraries");
       wr.WriteLine("//     System.Runtime.Numerics.dll System.Collections.Immutable.dll");
       wr.WriteLine("// but the 'dotnet' tool in net6.0 should pick those up automatically.");
       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 (isPartialTranslate) {
         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 (isPartialTranslate) {
         wr.WriteLine("#endif");
       }
       Synthesize = ProgramHasMethodsWithAttr(program, "synthesize");
       if (Synthesize) {
         CsharpSynthesizer.EmitImports(wr);
       }
 
-      if (program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (!isPartialTranslate) {
         EmitDafnySourceAttribute(program, wr);
       }
 
@@ -131,11 +135,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;
           }
@@ -149,8 +153,11 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
       // Instead we just make sure to guard them with "#if ISDAFNYRUNTIMELIB" when compiling the system module,
       // so they don't become duplicates when --include-runtime is used.
       // See comment at the top of DafnyRuntime.cs.
+      if (Options.DefaultModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.Omit) {
+        return;
+      }
 
-      if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
+      if (Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) {
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
 
@@ -161,7 +168,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/DafnyDriver/Commands/DafnyCli.cs

@@ -488,7 +488,10 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
     // which is not handled well.
     if (options.Get(CommonOptionBag.UseStandardLibraries)) {
       options.CliRootSourceUris.Add(StandardLibrariesDooUri);
-      dafnyFiles.Add(new DafnyFile(options, StandardLibrariesDooUri));
+      var stdlibDooFile = new DafnyFile(options, StandardLibrariesDooUri);
+      // Precompiled into the runtimes
+      stdlibDooFile.IsPrecompiled = true;
+      dafnyFiles.Add(stdlibDooFile);
     }
 
     return ExitValue.SUCCESS;

Source/DafnyPipeline/DafnyPipeline.csproj

@@ -57,6 +57,10 @@
       <LinkBase>DafnyRuntimeCsharp</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyRuntime\DafnyStandardLibraries.cs">
+      <LinkBase>DafnyRuntimeCsharp</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
     <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeGo\**\*.go" Exclude="..\DafnyRuntime\DafnyRuntimeGo\**\*_test.go">
       <LinkBase>DafnyRuntimeGo</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>

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/DafnyStdLibs/DafnyStdLibs.go

@@ -0,0 +1,25 @@
+// Package DafnyStdLibs
+// Dafny module DafnyStdLibs compiled into Go
+
+package DafnyStdLibs
+
+import (
+  _dafny "dafny"
+  os "os"
+  _System "System_"
+  DafnyStdLibs_BoundedInts "DafnyStdLibs_BoundedInts"
+  DafnyStdLibs_Functions "DafnyStdLibs_Functions"
+  DafnyStdLibs_Relations "DafnyStdLibs_Relations"
+  DafnyStdLibs_Wrappers "DafnyStdLibs_Wrappers"
+)
+var _ _dafny.Dummy__
+var _ = os.Args
+var _ _System.Dummy__
+var _ DafnyStdLibs_BoundedInts.Dummy__
+var _ DafnyStdLibs_Functions.Dummy__
+var _ DafnyStdLibs_Relations.Dummy__
+var _ DafnyStdLibs_Wrappers.Dummy__
+
+type Dummy__ struct{}
+
+