Merge branch 'master' into triggers-for-such-that

# Conflicts:
#	Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs

.github/workflows/nightly-build.yml

@@ -28,14 +28,6 @@ jobs:
     uses: ./.github/workflows/nightly-build-reusable.yml
     with:
       ref: master
-    secrets:
-      nuget_api_key: ${{ secrets.NUGET_API_KEY }}
-
-  nightly-build-for-4-10-0:
-    if: github.repository_owner == 'dafny-lang'
-    uses: ./.github/workflows/nightly-build-reusable.yml
-    with:
-      ref: 4.10.0
       publish-prerelease: true
     secrets:
       nuget_api_key: ${{ secrets.NUGET_API_KEY }}

Makefile

@@ -110,6 +110,8 @@ update-rs-module:
 
 update-go-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
+	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
+
 
 update-runtime-dafny:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)

RELEASE_NOTES.md

@@ -2,6 +2,28 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.10.0
+
+## New features
+
+- Support for code actions in the language server to:
+  - Insert failing implicit assertions in a "by" clause by preference.
+  - Insert forall statement for any forall expressions that could not be proved
+  - Insert calc statement for any equality that cannot be proved.
+  (https://github.com/dafny-lang/dafny/pull/6044)
+
+- Besides `--filter-position :<line>`, also support `--filter-position :<start>-<end>`, `--filter-position :<start>-` and `--filter-position :-<end>` (https://github.com/dafny-lang/dafny/pull/6077)
+
+- The options --iterations from the command `measure-complexity`, has been renamed to `--mutations`. The option `--progress VerificationJob` has been renamed to `--progress Batch`. (https://github.com/dafny-lang/dafny/pull/6078)
+
+## Bug fixes
+
+- By clauses for assign-such-that statements (:|), are now never ignored. (https://github.com/dafny-lang/dafny/pull/6024)
+
+- The code action for assertion no longer suggests asserting the same assertion. (https://github.com/dafny-lang/dafny/pull/6025)
+
+- Fix a bug that caused a crash when translating by blocks (https://github.com/dafny-lang/dafny/pull/6050)
+
 # 4.9.1
 
 ## New features

Scripts/bump_version_number.js

@@ -49,6 +49,9 @@ async function synchronizeRepositoryWithNewVersionNumber() {
   //# * Compile the standard libraries and update their binaries which are checked in
   await executeWithTimeout("make -C Source/DafnyStandardLibraries update-binary", 50*minutes);
 
+  // Verify that binaries have been updated.
+  await sanityCheckStandardLibraries(version);
+
   //# * Recompile Dafny so that standard libraries are in the executable.
   await execute("make exe");
 
@@ -97,6 +100,29 @@ async function synchronizeRepositoryWithNewVersionNumber() {
     `Source/DafnyRuntime/DafnyRuntime.csproj`, existingVersion);
 }
 
+// Unzips the file Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo (it's actually a zip file)
+// Fetch the content of Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries/manifest.toml
+// Verify that dafny_version = "Major.Minor.Patch.0" corresponds ot the version that is provided
+async function sanityCheckStandardLibraries(version) {
+  if(testMode) {
+    console.log("Would have run a sanity check");
+    return;
+  }
+  console.log("Sanity-checking standard libraries");
+  try {
+    await execute("unzip -o Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo -d Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries");
+  } catch(e) {
+    console.log("Could not unzip Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo", e);
+    throw e;
+  }
+  var manifest = await fs.promises.readFile("Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries/manifest.toml", "utf-8");
+  var match = manifest.match(/dafny_version = "(\d+\.\d+\.\d+)/);
+  assert_eq(match != null, true, "Could not find dafny_version in manifest.toml");
+  assert_eq(match[1], version, `dafny_version in manifest.toml is ${match[1]} but should have been ${version}. Something went wrong`);
+  await execute("rm -rf Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries");
+}
+
+
 // Returns the current version number
 async function getVersionNumber() {
   var versionFileContent = await fs.promises.readFile(versionFile, "utf-8");
@@ -362,8 +388,8 @@ async function ensureTakesIntoAccountAllReleaseInstructions() {
   }
 }
 
-function assert_eq(got, expected) {
+function assert_eq(got, expected, msg=undefined) {
   if(got != expected) {
-    throw "Expected " + expected + ", got " + got;
+    throw "Expected " + expected + ", got " + got + (msg != undefined ? " - " + msg : "");
   }
 }

Source/DafnyCore/DafnyOptions.cs

@@ -6,6 +6,7 @@
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
 using System.CommandLine;
+using System.CommandLine.Binding;
 using System.Diagnostics;
 using System.Globalization;
 using System.Linq;
@@ -75,6 +76,17 @@ public T Get<T>(Option<T> option) {
       return (T)Options.OptionArguments.GetOrDefault(option, () => (object)default(T));
     }
 
+
+    public T GetOrOptionDefault<T>(Option<T> option) {
+      return (T)Options.OptionArguments.GetOrDefault(option, () =>
+       ((IValueDescriptor<T>)option) is {
+         HasDefaultValue: true
+       } valueDescriptor
+          ? valueDescriptor.GetDefaultValue()
+          : (object)default(T)
+      );
+    }
+
     public object Get(Option option) {
       return Options.OptionArguments[option];
     }

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -107,9 +107,14 @@ static BoogieOptionBag() {
     });
     DafnyOptions.RegisterLegacyBinding(Cores,
       (o, f) => o.VcsCores = f == 0 ? (1 + System.Environment.ProcessorCount) / 2 : (int)f);
-    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, value) => {
-      var shouldVerify = !value && !options.Get(HiddenNoVerify);
-      options.Verify = shouldVerify;
+    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => {
+      var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify);
+      options.Verify = shouldVerify; // Boogie won't verify
+      options.DafnyVerify =
+        shouldVerify ||
+        options.Get(DeveloperOptionBag.BoogiePrint) != null ||
+        options.Get(DeveloperOptionBag.SplitPrint) != null ||
+        options.Get(DeveloperOptionBag.PassivePrint) != null;
     });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -22,6 +22,7 @@
 using JetBrains.Annotations;
 using Microsoft.Dafny;
 using Microsoft.Dafny.Triggers;
+using Serilog.Events;
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
@@ -700,6 +701,10 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) {
         return new Bpl.Program();
       }
 
+      if (Options.GetOrOptionDefault(CommonOptionBag.LogLevelOption).CompareTo(LogEventLevel.Verbose) <= 0) {
+        Options.OutputWriter.WriteLine("Starting translation to Boogie of module " + forModule.FullDafnyName);
+      }
+
       foreach (var plugin in p.Options.Plugins) {
         foreach (var rewriter in plugin.GetRewriters(p.Reporter)) {
           rewriter.PreVerify(forModule);