Merge branch 'master' into fix-unary-minus

.github/workflows/check-deep-tests-reusable.yml

@@ -12,7 +12,7 @@ jobs:
       with:
         path: dafny
         submodules: recursive
-    - uses: actions/github-script@v6
+    - uses: actions/github-script@v7
       if: github.repository_owner == 'dafny-lang'
       with:
         # Since nightly-build.yml always targets fixed branches now, rather than being parameterized by

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

@@ -15,15 +15,16 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
   // 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) && run.status !== "in_progress") {
-      if (run.conclusion !== "success") {
-        core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
-      } else {
+    if ((!sha || run.head_sha === sha)) {
+      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.status === "failure" || run.status === "timed_out") {
+        core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
+        return
       }
-      return
     }
   }
-  core.setFailed(`No runs of ${runFilterDesc} found!`)
+  core.setFailed(`No completed runs of ${runFilterDesc} found!`)
 }

.github/workflows/doc-tests.yml

@@ -26,7 +26,7 @@ jobs:
 
     steps:
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: 6.0.x
     - name: Checkout Dafny

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

@@ -64,7 +64,7 @@ jobs:
       if: runner.os == 'Linux'
       run: cert-sync /etc/ssl/certs/ca-certificates.crt
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{ env.dotnet-version }}
     - name: C++ for ubuntu 20.04
@@ -77,18 +77,18 @@ jobs:
         sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
     - name: Set up oldest supported JDK
       if: matrix.target-language-version != 'newest'
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         java-version: 8
         distribution: corretto
     - name: Set up newest supported JDK
       if: matrix.target-language-version == 'newest'
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         java-version: 18
         distribution: corretto
     - name: Set up Python
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with: 
         python-version: '3.11'
     - name: Upgrade outdated pip

.github/workflows/msbuild.yml

@@ -23,7 +23,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{env.dotnet-version}}
     - name: Checkout Dafny
@@ -55,7 +55,7 @@ jobs:
       working-directory: dafny
       run: dotnet build Source/Dafny.sln
     - name: Create NuGet package (just to make sure it works)
-      run: dotnet pack --no-build dafny/Source/Dafny.sln
+      run: dotnet pack dafny/Source/Dafny.sln
     - name: Check uniformity of integration tests that exercise backends
       run: DAFNY_INTEGRATION_TESTS_MODE=uniformity-check dotnet test dafny/Source/IntegrationTests
 
@@ -91,7 +91,7 @@ jobs:
           submodules: recursive
 
       - name: Setup dotnet
-        uses: actions/setup-dotnet@v3
+        uses: actions/setup-dotnet@v4
         with:
           dotnet-version: ${{env.dotnet-version}}
 

.github/workflows/nightly-build.yml

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

.github/workflows/publish-release-reusable.yml

@@ -35,7 +35,7 @@ env:
 jobs:
 
   publish-release:
-    runs-on: ubuntu-20.04
+    runs-on: macos-latest   # Put back 'ubuntu-20.04' if macos-latest fails in any way
     steps:
     - name: Print version
       run: echo ${{ inputs.name }}
@@ -51,7 +51,7 @@ jobs:
         git push origin ${{ inputs.tag_name }} -f
       working-directory: dafny
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{env.dotnet-version}}
     - name: C++ for ubuntu 20.04
@@ -63,14 +63,14 @@ jobs:
       run: |
         sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
     - name: Set up JDK 18
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         java-version: 18
         distribution: corretto
     - uses: actions/setup-node@v4
     - run: npm install bignumber.js
     - name: Set up Python
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with: 
        python-version: '3.11'
     - name: Build Dafny
@@ -79,11 +79,11 @@ jobs:
         rm dafny/Binaries/*.nupkg
     - name: Create release NuGet package (for uploading)
       if: ${{ !inputs.prerelease }}
-      run: dotnet pack --no-build dafny/Source/Dafny.sln
+      run: dotnet pack dafny/Source/Dafny.sln
     - name: Create prerelease NuGet package (for uploading)
       if: ${{ inputs.prerelease }}
       # NuGet will consider any package with a version-suffix as a prerelease
-      run: dotnet pack --version-suffix ${{ inputs.name }} --no-build dafny/Source/Dafny.sln
+      run: dotnet pack --version-suffix ${{ inputs.name }} dafny/Source/Dafny.sln
 
     - name: Make NuGet package available as an artifact
       uses: actions/upload-artifact@v3

.github/workflows/refman.yml

@@ -25,7 +25,7 @@ jobs:
     - name: OS
       run: echo ${{ runner.os }} ${{ matrix.os }}
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: 6.0.x
     - name: Checkout Dafny

.github/workflows/release-brew.yml

@@ -26,7 +26,7 @@ jobs:
         java -version
         python --version
     - name: Set up Python
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with:
         python-version: '3.11'
     ## To be consistent, the download should be tested with the quicktest.sh corresponding to

.github/workflows/release-downloads-nuget.yml

@@ -38,12 +38,12 @@ jobs:
     - name: OS
       run: echo ${{ runner.os }} ${{ matrix.os }}
     - name: Set up JDK 18
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         java-version: 18
         distribution: corretto
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{env.dotnet-version}}
     - name: Load Z3

.github/workflows/release-downloads.yml

@@ -36,7 +36,7 @@ jobs:
     - name: OS
       run: echo ${{ runner.os }} ${{ matrix.os }}
     - name: Set up JDK 18
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         java-version: 18
         distribution: corretto

.github/workflows/runtime-tests.yml

@@ -25,7 +25,7 @@ jobs:
         with:
           submodules: true
       - name: Set up JDK 18
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 18
           distribution: corretto

.github/workflows/standard-libraries.yml

@@ -15,22 +15,22 @@ jobs:
 
   build:
     needs: check-deep-tests
-    runs-on: ubuntu-latest
+    runs-on: macos-latest
 
     steps:
       - name: Checkout Dafny
         uses: actions/checkout@v4
         with:
           submodules: true
       - name: Set up JDK 18
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 18
           distribution: corretto
       - name: Build Dafny
         run: dotnet build Source/Dafny.sln
       - name: Get Z3
-        run: make z3-ubuntu
+        run: make z3-mac
       - run: npm install bignumber.js
       - name: Test DafnyStandardLibraries
         run: make -C Source/DafnyStandardLibraries all

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

@@ -42,7 +42,7 @@ jobs:
         path: dafny
         submodules: recursive
     - name: Setup .NET
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
         dotnet-version: 6.0.x
     - name: Install dependencies

RELEASE_NOTES.md

@@ -2,6 +2,82 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.4.0
+
+## New features
+
+- Reads clauses on method declarations are now supported when the `--reads-clauses-on-methods` option is provided. 
+  The `{:concurrent}` attribute now verifies that the `reads` and `modifies` clauses are empty instead of generating an auditor warning.
+  (https://github.com/dafny-lang/dafny/pull/4440)
+
+- Added two new options, `--warn-contradictory-assumptions` and `--warn-redundant-assumptions`, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (https://github.com/dafny-lang/dafny/pull/4542)
+
+- Verification of the `{:concurrent}` attribute on methods now allows non-empty `reads` and `modifies` clauses with the `{:assume_concurrent}` attribute. (https://github.com/dafny-lang/dafny/pull/4563)
+
+- Implemented support for workspace/symbol request to allow IDE navigation by symbol. (https://github.com/dafny-lang/dafny/pull/4619)
+
+- The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged. (https://github.com/dafny-lang/dafny/pull/4625)
+
+- Built-in types such as the `nat` subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
+  instead of emitted on every call to `dafny translate`, to avoid potential duplicate definitions when translating components separately.
+  (https://github.com/dafny-lang/dafny/pull/4658)
+
+- The new `--only-label` option to `merge-coverage-reports` includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option `--only-label NotCovered` will highlight only the regions not covered by either testing or verification. (https://github.com/dafny-lang/dafny/pull/4673)
+
+- The Dafny distribution now includes standard libraries, available with the `--standard-libraries` option.
+  See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details.
+  (https://github.com/dafny-lang/dafny/pull/4678)
+
+- Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (https://github.com/dafny-lang/dafny/pull/4681)
+
+- The new `--coverage-report` flag to `dafny run` and `dafny test` creates an HTML report highlighting which portions of the program were executed at runtime. (https://github.com/dafny-lang/dafny/pull/4755)
+
+- Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute `{:disable-nonlinear-arithmetic}`, 
+  which optionally takes the value false to enable nonlinear arithmetic.
+  (https://github.com/dafny-lang/dafny/pull/4773)
+
+- Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (https://github.com/dafny-lang/dafny/pull/4855)
+
+## Bug fixes
+
+- Ensures that computing the set of values or items of map can only be done if the type of the range supports equality. (https://github.com/dafny-lang/dafny/pull/1373)
+
+- Subset type decl's witness correctly taken into account (https://github.com/dafny-lang/dafny/pull/3792)
+
+- Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations (https://github.com/dafny-lang/dafny/pull/4406)
+
+- Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program. (https://github.com/dafny-lang/dafny/pull/4530)
+
+- Fix a bug that prevented certain types of lemma to be verified in the IDE (https://github.com/dafny-lang/dafny/pull/4607)
+
+- Dot completion now works on values the type of which is a type synonym. (https://github.com/dafny-lang/dafny/pull/4635)
+
+- Fix a case where the document symbol API would return incorrect data when working on a file with parse errors (https://github.com/dafny-lang/dafny/pull/4675)
+
+- Emit less nested target code in match-case expressions (nice for readability, and necessary for Java) (https://github.com/dafny-lang/dafny/pull/4683)
+
+- Ghost diagnostics are now correctly updated when they become empty (https://github.com/dafny-lang/dafny/pull/4693)
+
+- Enable verification options that are configured in a Dafny project file, to be picked up by the Dafny language server (https://github.com/dafny-lang/dafny/pull/4703)
+
+- Prevent double-counting of covered/uncovered lines in test coverage reports (https://github.com/dafny-lang/dafny/pull/4710)
+
+- fix: correction of type inference for default expressions (https://github.com/dafny-lang/dafny/pull/4724)
+
+- The new type checker now also supports static reveals for instance functions (https://github.com/dafny-lang/dafny/pull/4733)
+
+- Resolve :- expressions with void outcomes in new resolver (https://github.com/dafny-lang/dafny/pull/4734)
+
+- Crash in the resolver on type parameters of opaque functions in refined modules (https://github.com/dafny-lang/dafny/pull/4768)
+
+- Fix error messages being printed after their context snippets (https://github.com/dafny-lang/dafny/pull/4787)
+
+- Override checks no longer crashing when substituting type parameters and equality (https://github.com/dafny-lang/dafny/pull/4812)
+
+- Removed one cause of need for restarting the IDE. (https://github.com/dafny-lang/dafny/pull/4833)
+
+- The Python compiler emits reserved names for datatypes (https://github.com/dafny-lang/dafny/pull/4843)
+
 # 4.3.0
 
 ## New features

Source/Dafny/Dafny.cs

@@ -4,6 +4,6 @@ namespace Dafny;
 
 public class Dafny {
   public static int Main(string[] args) {
-    return DafnyCli.Main(args);
+    return DafnyBackwardsCompatibleCli.Main(args);
   }
 }

Source/DafnyCore/AST/Attributes.cs

@@ -15,6 +15,7 @@ void ObjectInvariant() {
 
   public static string AxiomAttributeName = "axiom";
   public static string ConcurrentAttributeName = "concurrent";
+  public static string AssumeConcurrentAttributeName = "assume_concurrent";
   public static string ExternAttributeName = "extern";
   public static string VerifyAttributeName = "verify";
   public static string AutoGeneratedAttributeName = "auto_generated";

Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs

@@ -63,7 +63,7 @@ public override IEnumerable<Expression> SubExpressions {
   }
 
   public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
-    return LegalSourceConstructors;
+    return (IEnumerable<IDeclarationOrUsage>)LegalSourceConstructors ?? Array.Empty<IDeclarationOrUsage>();
   }
 
   public IToken NameToken => tok;

Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs

@@ -73,8 +73,6 @@ public void FillIn(ModuleResolver resolver, Dictionary<DefaultValueExpression, W
     var s = new DefaultValueSubstituter(resolver, visited, this.receiver, this.substMap, typeMap);
     this.ResolvedExpression = s.Substitute(this.formal.DefaultValue);
     visited[this] = WorkProgress.Done;
-
-    this.ResolvedExpression.Type = this.Type;
   }
 
   class DefaultValueSubstituter : Substituter {

Source/DafnyCore/AST/Formatting.dfy

@@ -31,7 +31,7 @@ module {:extern "Microsoft"} {:options "-functionSyntax:4"}  Microsoft {
         ensures allocated(x) {
       }
 
-      /** Prints the entire program while fixing identation, based on
+      /** Prints the entire program while fixing indentation, based on
           1) indentation information provided by the IIndentationFormatter reindent
           2) Reindentation algorithm provided by the same reindent */
       method ReindentProgramFromFirstToken(firstToken: IToken, reindent: IIndentationFormatter) returns (s: CsString)