Merge branch 'master' into fix-issue-5554-soundness

.github/workflows/check-for-workflow-run.js

@@ -14,21 +14,32 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
   // These are ordered by creation time, so decide based on the first
   // run for this SHA we see.
   const runFilterDesc = sha ? `${workflow_id} on ${sha}` : workflow_id
-  for (const run of result.data.workflow_runs) {
-    if ((!sha || run.head_sha === sha)) {
-      // The status property can be one of: “queued”, “in_progress”, or “completed”.
-      if (run.status === "completed") {
-        // The conclusion property can be one of:
-        // “success”, “failure”, “neutral”, “cancelled”, “skipped”, “timed_out”, or “action_required”.
-        if (run.conclusion === "success") {
-          // The SHA is fully tested, exit with success
-          console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
-          return
-        } else if (run.conclusion === "failure" || run.conclusion === "timed_out") {
-          core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
-          return
-        }
-      }
+  const workflow_runs =  result.data.workflow_runs.filter(run => !sha || run.head_sha === sha)
+  const workflow_runs_completed = workflow_runs.filter(run => run.status === "completed")
+  // The status property can be one of: “queued”, “in_progress”, or “completed”.
+  const workflow_runs_in_progress = workflow_runs.filter(run => run.status !== "completed")
+  for (const run of workflow_runs_completed) {
+    // The conclusion property can be one of:
+    // “success”, “failure”, “neutral”, “cancelled”, “skipped”, “timed_out”, or “action_required”.
+    if (run.conclusion === "success") {
+      // The SHA is fully tested, exit with success
+      console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
+      return
+    } else if (run.conclusion === "failure" || run.conclusion === "timed_out") {
+      const extraMessage = workflow_runs_in_progress.length > 0 ?
+        `\nA run of ${runFilterDesc} is currently ${workflow_runs_in_progress[0].status}:`+
+        ` ${workflow_runs_in_progress[0].html_url}, just re-run this test once it is finished.` :
+        `\nAt the time of checking, no fix was underway.\n`+
+        `- Please first check https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml. `+
+        `If you see any queued or in progress run on ${runFilterDesc}, just re-run this test once it is finished.`+
+        `- If not, and you are a Dafny developer, please fix the issue by creating a PR with the label [run-deep-tests], have it reviewed and merged, ` +
+        `and then trigger the workflow on ${runFilterDesc} with the URL https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml.\n`+
+        `With such a label, you can merge a PR even if tests are not successful, but make sure the deeps one are!\n`+
+        `If you do not have any clue on how to fix it, `+
+        `at worst you can revert all PRs from the last successful run and indicate the authors they need to re-file`+
+        ` their PRs and add the label [run-deep-tests] to their PRs`;
+      core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}${extraMessage}`)
+      return
     }
   }
   core.setFailed(`No completed runs of ${runFilterDesc} found!`)

.github/workflows/integration-tests-reusable.yml

@@ -128,6 +128,22 @@ jobs:
 #    - name: Clean up libraries for testing
 #      run: |
 #        rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override
+    - name: Use the default Rust linker (Non-Windows)
+      if: runner.os != 'Windows'
+      run: rustup default stable
+    - name: Use specific Toolchain (Windows)
+      if: runner.os == 'Windows'
+      run: rustup default stable-x86_64-pc-windows-gnu
+    - name: Rust-related System information
+      run: |
+        echo "What is the Rust version?"
+        rustc -vV
+        echo "What is the cargo version?"
+        cargo --version
+        echo "What is the architecture?"
+        uname -m
+        echo "What are Rust toolchains installed?"
+        rustup toolchain list
     - name: Create release
       if: inputs.all_platforms
       run: |

.github/workflows/nightly-build.yml

@@ -23,11 +23,11 @@ on:
   workflow_dispatch:
 
 jobs:
-  nightly-build-for-4-9:
+  nightly-build-for-master:
     if: github.repository_owner == 'dafny-lang'
     uses: ./.github/workflows/nightly-build-reusable.yml
     with:
-      ref: 4.9
+      ref: master
       publish-prerelease: true
     secrets:
       nuget_api_key: ${{ secrets.NUGET_API_KEY }}

.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: 'GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs'
+        exclude: '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#"]

RELEASE_NOTES.md

@@ -2,6 +2,28 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.9.0
+
+## New features
+
+- Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (https://github.com/dafny-lang/dafny/pull/5761)
+
+- By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't. (https://github.com/dafny-lang/dafny/pull/5779)
+
+- Use --suggest-proof-refactoring to be alerted of function definitions, which have no contribution to a method's proof, and facts, which are only used once in a proof. (https://github.com/dafny-lang/dafny/pull/5812)
+
+- Support for [top-level @-attributes](https://dafny.org/latest/DafnyRef/DafnyRef#sec-at-attributes) (https://github.com/dafny-lang/dafny/pull/5825)
+
+## Bug fixes
+
+- Enable abstract imports to work well with match expression that occur in specifications (https://github.com/dafny-lang/dafny/pull/5808)
+
+- Fix a bug that prevented using reveal statement expressions in the body of a constant. (https://github.com/dafny-lang/dafny/pull/5823)
+
+- Improve performance of `dafny verify` for large applications, by removing memory leaks (https://github.com/dafny-lang/dafny/pull/5827)
+
+- Green gutter icons cover constants without RHS (https://github.com/dafny-lang/dafny/pull/5841)
+
 # 4.8.1
 
 ## New features

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -142,6 +142,7 @@ public enum ErrorId {
     p_general_traits_full,
     p_decreases_without_to,
     p_binding_in_decreases_to,
+    p_ghost_in_decreases_to,
   }
 
   static ParseErrors() {

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

@@ -170,6 +170,17 @@ bool IsFunctionDecl() {
     return IsFunctionDecl(kind);
   }
 
+  bool IsDecreasesTo() {
+    scanner.ResetPeek();
+    if (la.kind is _decreases or _nonincreases) {
+      Token x = scanner.Peek();
+      if (x.kind == _ident && x.val == "to") {
+        return true;
+      }
+    }
+    return false;
+  }
+
   private bool IsFunctionDecl(int kind) {
     switch (kind) {
       case _function: