Merge branch 'master' of github.com:dafny-lang/dafny into actions-and…

…-streaming-stdlibs

.github/workflows/msbuild.yml

@@ -37,7 +37,7 @@ jobs:
       run: dotnet tool restore
     - name: Check whitespace and style
       working-directory: dafny
-      run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+      run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Generic/Deserializer/Generated.cs --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
     - name: Check that it's possible to bump the version
       working-directory: dafny
       run: make bumpversion-test

.github/workflows/runtime-tests.yml

@@ -49,6 +49,9 @@ jobs:
         run: dotnet build Source/Dafny.sln
       - name: Get Z3
         run: make z3-ubuntu
+      - name: Test using outer Makefile
+        run: |
+          make test-integration
       - name: Test DafnyCore
         run: |
           cd ./Source/DafnyCore

.pre-commit-config.yaml

@@ -5,5 +5,5 @@ repos:
         name: dotnet-format
         language: system
         entry: dotnet format whitespace Source/Dafny.sln -v:d --include
-        exclude: 'Source/DafnyCore/Scanner.cs|Source/DafnyCore/Parser.cs|.git/modules/Source/boogie|Source/DafnyCore/GeneratedFromDafny|Source/DafnyCore.Test/GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs'
+        exclude: 'Source/DafnyCore/Generic/Deserializer/Generated.cs|Source/DafnyCore/Scanner.cs|Source/DafnyCore/Parser.cs|.git/modules/Source/boogie|Source/DafnyCore/GeneratedFromDafny|Source/DafnyCore.Test/GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs'
         types_or: ["c#"]

Makefile

@@ -87,7 +87,7 @@ z3-ubuntu:
 	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 
 format:
-	dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+	dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Generic/Deserializer/Generated.cs --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
 
 clean:
 	(cd "${DIR}"; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
@@ -110,11 +110,13 @@ 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)
 
-pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module update-rs-module
+pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module
 
 update-standard-libraries:
 	(cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary)
@@ -130,3 +132,17 @@ pr: exe dfy-to-cs-exe pr-nogeneration
 
 # Same as `make pr` but useful when resolving conflicts, to take the last compiled version of Dafny first
 pr-conflict: dfy-to-cs-exe dfy-to-cs-exe pr-nogeneration
+
+gen-integration: gen-schema gen-deserializer
+
+PARSED_AST_FILE=Source/Scripts/Syntax.cs-schema
+gen-schema:
+	./script.sh generate-parsed-ast $(PARSED_AST_FILE)
+
+GENERATED_DESERIALIZER_FILE=Source/DafnyCore/AST/SyntaxDeserializer/generated.cs
+gen-deserializer:
+	./script.sh generate-syntax-deserializer ${GENERATED_DESERIALIZER_FILE}
+
+test-integration: gen-integration
+	(git status --porcelain || (echo 'Consider running `make gen-integration`'; exit 1; ))
+

README.md

@@ -27,7 +27,7 @@ A reference manual is available both [online](https://dafny-lang.github.io/dafny
 
 ## Community
 
-You can ask questions about Dafny on [Stack Overflow](https://stackoverflow.com/questions/tagged/dafny) or participate in general discussion on Dafny's [![Gitter](https://badges.gitter.im/dafny-lang/community.svg)](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge).
+Feel free to report issues here on GitHub or to ask for questions on our :speech_balloon: [Zulip](https://dafny.zulipchat.com/) channel. 
 
 ## Try Dafny
 

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/AutoExtern/AutoProgram.cs

@@ -215,7 +215,7 @@ private bool IsSkippedBaseType(BaseTypeSyntax bt) {
     syntax.BaseList?.Types
       .Where(bt => !IsSkippedBaseType(bt))
       .Select(bt => new Type(bt.Type, model))
-    ?? Enumerable.Empty<Type>();
+    ?? [];
 
   public override void Pp(TextWriter wr, string indent) {
     var baseTypes = BaseTypes.ToList();
@@ -388,8 +388,8 @@ public override void Pp(TextWriter wr, string indent) {
 internal class Name {
   private const string EscapePrefix = "CSharp_";
 
-  private static readonly List<string> DisallowedNameWords = new List<string>
-    {"type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"};
+  private static readonly List<string> DisallowedNameWords =
+    ["type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"];
   private static readonly Regex DisallowedNameRe =
     new Regex($"^(_|({String.Join("|", DisallowedNameWords)})$)");
 

Source/DafnyCore.Test/ClonerTest.cs

@@ -11,8 +11,7 @@ class DummyDecl : Declaration {
     public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) {
     }
 
-    public DummyDecl(IOrigin origin, Name name, Attributes attributes, bool isRefining) : base(origin, name,
-      attributes, isRefining) {
+    public DummyDecl(IOrigin origin, Name name, Attributes attributes) : base(origin, name, attributes) {
     }
 
     public override SymbolKind? Kind => null;
@@ -33,11 +32,11 @@ public void ClonerKeepsBodyStartTok() {
       IsTypeExplicit = false
     };
     var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
-      false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
-      new List<Formal>(), new List<AttributedExpression>(),
-      new Specification<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null),
-      new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
-      new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);
+      false, false, [], [formal1, formal2],
+      [], [],
+      new Specification<FrameExpression>(), new Specification<FrameExpression>([], null),
+      [], new Specification<Expression>([], null),
+      new BlockStmt(rangeToken, []), null, Token.NoToken, false);
 
     dummyDecl.BodyStartTok = tokenBodyStart;
     var cloner = new Cloner();