Merge branch 'master' into fix-5647-tail-recursion-rust-fixup

.github/workflows/compfuzzci_close_pr.yaml

@@ -0,0 +1,29 @@
+# This workflow is triggered on PR being closed.
+# It dispatches workflow on CompFuzzCI repository, where the bugs found in the PR head is discarded from the database.
+
+name: Updating CompFuzzCI on PR Closed
+on:
+  pull_request:
+    branches:
+      - master
+    types: [closed]
+
+jobs:
+  UpdatePRClosed:
+    if: github.event.pull_request.base.ref == 'master' && github.event.pull_request.head.repo.owner.login == 'dafny-lang'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_pr_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      pr_head_ref: '${{github.event.pull_request.head.ref}}' 
+                  }
+              })

.github/workflows/compfuzzci_fuzz_no_forks.yaml

@@ -0,0 +1,32 @@
+# This workflow is triggered on PR being opened, synced, reopened, closed.
+# It dispatches workflow on CompFuzzCI repository, where fuzzing of the PR is handled.
+
+name: Fuzzing on PR (excluding forks)
+on:
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  FuzzOnPR:
+    if: github.event.pull_request.base.ref == 'master' && github.event.pull_request.head.repo.owner.login == 'dafny-lang'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'fuzz.yaml',
+                  ref: 'main',
+                  inputs: {
+                      commit: '${{ github.event.pull_request.head.sha }}',
+                      main_commit: '${{github.event.pull_request.base.sha}}',
+                      branch: '${{github.event.pull_request.head.ref}}',
+                      duration: '3600',
+                      instance: '2'
+                  }
+              })

.github/workflows/compfuzzci_process_issues.yaml

@@ -0,0 +1,51 @@
+# This workflow is triggered on issue being opened, closed, reopened.
+# The CompFuzzCI fuzzer needs to keep track of active issues in the repository to ensure that the fuzzer does not report the same issue multiple times.
+# For open and reopen events: It dispatches workflow on CompFuzzCI repository, where the issue is added to the database.
+# For close event: It dispatches workflow on CompFuzzCI repository, where the issue is removed from the database.
+
+name: Issue Update for Fuzzer
+on:
+  issues:
+    branches:
+      - master
+    types: [opened, closed, reopened]
+
+jobs:
+  UpdateIssueOpened:
+    if: github.event.action == 'opened' || github.event.action == 'reopened'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_open.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}',
+                      issuer: '${{github.event.issue.user.login}}',
+                      commit: '${{ github.sha }}'          
+                  }
+              })
+  UpdateIssueClosed:
+    if: github.event.action == 'closed'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}'
+                  }
+              })

.github/workflows/msbuild.yml

@@ -161,7 +161,7 @@ jobs:
           output: both
           # Fail if less than 86% total coverage, measured across all packages combined.
           # Report "yellow" status if less than 90% total coverage.
-          thresholds: '86 90'
+          thresholds: '85 90'
 
       - name: Code coverage report (LSP)
         uses: irongut/[email protected]

.github/workflows/runtime-tests.yml

@@ -48,7 +48,7 @@ jobs:
           cd ./Source/DafnyCore
           make test
           make check-format
-      - name: Test DafnyRuntime (C#)
+      - name: Test DafnyRuntime (C#, Rust)
         run: |
           cd ./Source/DafnyRuntime
           make all
@@ -72,3 +72,7 @@ jobs:
         run: |
           cd ./Source/DafnyRuntime/DafnyRuntimeJs
           make all
+      - name: Test DafnyRuntimeRust
+        run: |
+          cd ./Source/DafnyRuntime/DafnyRuntimeRust
+          make all

.gitignore

@@ -88,3 +88,5 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json
 Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1
+/Source/DafnyCore/Prelude/DafnyPrelude.bpl
+/Source/DafnyCore/Prelude/Sequences.bpl

Makefile

@@ -26,6 +26,10 @@ boogie: ${DIR}/boogie/Binaries/Boogie.exe
 tests:
 	(cd "${DIR}"; dotnet test Source/IntegrationTests)
 
+# make test name=<part of the path of an integration test>
+test:
+	(cd "${DIR}"; dotnet test Source/IntegrationTests --filter "DisplayName~${name}")
+
 tests-verbose:
 	(cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
 
@@ -87,17 +91,28 @@ clean:
 update-cs-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module)
 
+update-rs-module:
+	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeRust; make update-system-module)
+
 update-go-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
 
 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-standard-libraries:
+	(cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary)
+
 # `make pr` will bring you in a state suitable for submitting a PR
 # - Builds the Dafny executable
 # - Use the build to convert core .dfy files to .cs
 # - Rebuilds the Dafny executable with this .cs files
 # - Apply dafny format on all dfy files
 # - Apply dotnet format on all cs files except the generated ones
 # - Rebuild the Go and C# runtime modules as needed.
-pr: exe dfy-to-cs-exe format-dfy format update-runtime-dafny update-cs-module update-go-module
+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

RELEASE_NOTES.md

@@ -2,6 +2,37 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.8.0
+
+## New features
+
+- Introduce `hide` statements that enable hiding the body of a function at a particular proof location, which allows simplifying the verification of that proof in case the body of the function is not needed for the proof. `Hide` statements make the opaque keyword on functions obsolete. (https://github.com/dafny-lang/dafny/pull/5562)
+
+- Let the command `measure-complexity` output which verification tasks performed the worst in terms of resource count. Output looks like:
+  ...
+  Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources
+  Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources
+  ...
+  (https://github.com/dafny-lang/dafny/pull/5631)
+
+- Enable the option `--enforce-determinism` for the commands `resolve` and `verify` (https://github.com/dafny-lang/dafny/pull/5632)
+
+- Method calls get an optional by-proof that hides the precondtion and its proof (https://github.com/dafny-lang/dafny/pull/5662)
+
+## Bug fixes
+
+- Clarify error location of inlined `is` predicates. (https://github.com/dafny-lang/dafny/pull/5587)
+
+- Optimize the compilation of single-LHS assignment statements to allow the RHS to be a deeply nested expression. This solves a problem in compiling to Java, since `javac` does not deal gracefully with nested lambda expressions. (https://github.com/dafny-lang/dafny/pull/5589)
+
+- Crash when compiling an empty source file while including testing code (https://github.com/dafny-lang/dafny/pull/5638)
+
+- Let the options --print-mode=NoGhostOrIncludes and --print-mode=NoIncludes work (https://github.com/dafny-lang/dafny/pull/5645)
+
+- Verification in the IDE now works correctly when declaring nested module in a different file than their parent. (https://github.com/dafny-lang/dafny/pull/5650)
+
+- Fix NRE that would occur when using --legacy-data-constructors (https://github.com/dafny-lang/dafny/pull/5655)
+
 # 4.7.0
 
 ## New features