Merge branch 'master' into SelfReference

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

@@ -16,7 +16,7 @@ jobs:
  uses: actions/checkout@v3
  with:
  path: dafny
- submodules: true
+ submodules: recursive
  - uses: actions/github-script@v6
  if: github.repository_owner == 'dafny-lang'
  with:

.github/workflows/deep-tests.yml

@@ -32,6 +32,7 @@ jobs:
  uses: actions/checkout@v3
  with:
  ref: ${{ inputs.sha }}
+ submodules: recursive
 
  - name: Get short sha
  run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV

.github/workflows/doc-tests.yml

@@ -55,3 +55,8 @@ jobs:
  cd dafny/docs
  chmod +x ./check-examples
  PATH=../bin:$PATH ./check-examples DafnyRef/*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded
+ - name: Check ProofOptimization examples
+ run: |
+ cd dafny/docs
+ chmod +x ./check-examples
+ PATH=../bin:$PATH ./check-examples ProofOptimization/*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded

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

@@ -98,7 +98,7 @@ jobs:
  uses: actions/checkout@v3
  with:
  path: dafny
- submodules: false # Until the libraries work again
+ submodules: true # Until the libraries work again
 # - 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
@@ -132,6 +132,11 @@ jobs:
  run: |
  cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1.exe
  dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" dafny/Source/IntegrationTests/IntegrationTests.csproj
+ - name: Generate tests (non-Windows)
+ if: runner.os != 'Windows'
+ run: |
+ cd dafny/docs/HowToFAQ
+ ../check-examples -c Errors-Parser.md
  - name: Run integration tests (non-Windows)
  if: runner.os != 'Windows'
  env:

.github/workflows/msbuild.yml

@@ -32,11 +32,13 @@ jobs:
  uses: actions/checkout@v3
  with:
  path: dafny
+ submodules: recursive
  - name: Restore tools
  working-directory: dafny
  run: dotnet tool restore
  - name: Get Boogie Version
  run: |
+ sudo apt-get update
  sudo apt-get install -qq libxml2-utils
  echo "boogieVersion=`xmllint --xpath "//PackageReference[@Include='Boogie.ExecutionEngine']/@Version" dafny/Source/DafnyCore/DafnyCore.csproj | grep -Po 'Version="\K.*?(?=")'`" >> $GITHUB_ENV
  - name: Attempt custom Boogie patch
@@ -85,6 +87,7 @@ jobs:
  uses: actions/checkout@v3
  with:
  path: dafny
+ submodules: recursive
 
  - name: Setup dotnet
  uses: actions/setup-dotnet@v3
@@ -121,7 +124,13 @@ jobs:
  # LSP results
  reportgenerator \
  -reports:"./**/coverage.cobertura.xml" \
- -reporttypes:Cobertura -targetdir:coverage-cobertura
+ -reporttypes:Cobertura -targetdir:coverage-cobertura \
+ -classfilters:-Microsoft.Dafny.*PreType* \
+ -classfilters:-Microsoft.Dafny.ResolverPass \
+ -classfilters:-Microsoft.Dafny.*Underspecification* \
+ -classfilters:-Microsoft.Dafny.DetectUnderspecificationVisitor \
+ -classfilters:-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector \
+ -classfilters:-Microsoft.Dafny.ResolverPass
  # Generate HTML from combined report, leaving out XUnitExtensions
  reportgenerator \
  -reports:"coverage-cobertura/Cobertura.xml" \

.github/workflows/publish-release.yml

@@ -26,7 +26,7 @@ jobs:
  version: ${{ steps.get-version.outputs.version-without-v }}
 
  publish-release:
- needs: [get-version]
+ needs: [check-deep-tests, get-version]
  uses: ./.github/workflows/publish-release-reusable.yml
  with:
  name: ${{ needs.get-version.outputs.version }}

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

@@ -88,11 +88,18 @@ jobs:
  run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]{5}"
  shell: bash
  ## Check that a simple program compiles and runs on each supported platform
+ ## Now that the dotnet tool distribution doesn't include the Scripts,
+ ## so we need to clone the repository to get them.
+ - name: Checkout Dafny
+ uses: actions/checkout@v3
+ with:
+ submodules: recursive
+ path: dafny-repo
  - name: run quicktests
  run: |
  npm install bignumber.js
- dafny/quicktest.sh > log.txt
- diff log.txt dafny/quicktest.out
+ dafny-repo/Scripts/quicktest.sh dafny > log.txt
+ diff log.txt dafny-repo/Scripts/quicktest.out
 
  test-dafny-libraries:
 

.github/workflows/runtime-tests.yml

@@ -24,6 +24,8 @@ jobs:
  steps:
  - name: Checkout Dafny
  uses: actions/checkout@v3
+ with:
+ submodules: true
  - name: Set up JDK 18
  uses: actions/setup-java@v3
  with:
@@ -33,6 +35,11 @@ jobs:
  run: dotnet build Source/Dafny.sln
  - name: Get Z3
  run: make z3-ubuntu
+ - name: Test DafnyCore
+ run: |
+ cd ./Source/DafnyCore
+ make test
+ make check-format
  - name: Test DafnyRuntimeDafny
  run: |
  cd ./Source/DafnyRuntime/DafnyRuntimeDafny

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

@@ -63,6 +63,8 @@ jobs:
  chmod +x Binaries/z3/bin/z3*
  - name: Build
  run: dotnet build -warnaserror --no-restore ${{env.solutionPath}}
+ - name: Run DafnyCore Tests
+ run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyCore.Test
  - name: Run DafnyLanguageServer Tests
  run: |
  ## Run twice to catch unstable code (Issue #2673)

RELEASE_NOTES.md

@@ -2,6 +2,101 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.1.0
+
+## New features
+
+- Added support for `.toml` based Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.
+ The CLI commands that take Dafny files as input, such as build, run, translate, will now also accept Dafny project files.
+ When using an IDE based on `dafny server`, such as the Dafny VSCode extension, the IDE will look for a Dafny project file by traversing up the file tree from the currently opened file, until it finds it `dfyconfig.toml`. The project file will override options specified in the IDE.
+ (https://github.com/dafny-lang/dafny/pull/2907)
+
+- Recognize the `{:only}` attribute on `assert` statements to temporarily transform other assertions into assumptions (https://github.com/dafny-lang/dafny/pull/3095)
+
+- Exposes the --output and --spill-translation options for the dafny test command (https://github.com/dafny-lang/dafny/pull/3612)
+
+- The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. (https://github.com/dafny-lang/dafny/pull/3660)
+
+- Added option --no-verify for language server (https://github.com/dafny-lang/dafny/pull/3732)
+
+- Documenting Dafny Entities
+ * Added `.GetDocstring(DafnyOptions)` to every AST node
+ * Plugin support for custom Docstring formatter, 
+ * Activatable plugin to support a subset of Javadoc through `--javadoclike-docstring-plugin`
+ * Support for displaying docstring in VSCode
+ (https://github.com/dafny-lang/dafny/pull/3756)
+
+- Documentation of the syntax for docstrings added to the reference manual (https://github.com/dafny-lang/dafny/pull/3773)
+
+- Labelled assertions and requires in functions (https://github.com/dafny-lang/dafny/pull/3804)
+
+- API support for obtaining the Dafny expression that is being checked by each assertion (https://github.com/dafny-lang/dafny/pull/3888)
+
+- Added a "Dafny Library" backend, which produces self-contained, pre-verified `.doo` files ideal for distributing shared libraries.
+ `.doo` files are produced with commands of the form `dafny build -t:lib ...`.
+ (https://github.com/dafny-lang/dafny/pull/3913)
+
+- Semantic interpretation of dots in names for `{:extern}` modules when compiling to Python (https://github.com/dafny-lang/dafny/pull/3919)
+
+- Code actions in editor to explicit failing assertions.
+ In VSCode, place the cursor on a failing assertion that support being made explicit and either
+ - Position the caret on a failing assertion, press CTRL+; and then ENTER
+ - Hover over the failing division by zero, click "quick fix", press ENTER
+ Both scenarios will explicit the failing assertion.
+ If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.
+
+ Here is a initial list of assertions that can now be made explicit:
+ - Division by zero
+ - "out of bound" on sequences index, sequence slices, or array index
+ - "Not in domain" on maps
+ - "Could not prove unicity" of `var x :| ...` statement 
+ - "Could not prove existence" of `var x :| ...` statement
+ (https://github.com/dafny-lang/dafny/pull/3940)
+
+## Bug fixes
+
+- dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run (https://github.com/dafny-lang/dafny/pull/3221)
+
+- The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized. (https://github.com/dafny-lang/dafny/pull/3398)
+
+- While using `dafny translate --target=java`, the `--include-runtime` option works as intended, while before it had no affect. (https://github.com/dafny-lang/dafny/pull/3611)
+
+- Tested support for paths with spaces in them (https://github.com/dafny-lang/dafny/pull/3683)
+
+- Crash related to the override check for generic functions (https://github.com/dafny-lang/dafny/pull/3692)
+
+- Opaque functions guaranteed to be opaque until revealed (https://github.com/dafny-lang/dafny/pull/3719)
+
+- Support for Corretto tests (https://github.com/dafny-lang/dafny/pull/3731)
+
+- Right shift on native byte has the same consistent semantics even in Java (https://github.com/dafny-lang/dafny/pull/3734)
+
+- Main and {:test} methods may now be in the same program (https://github.com/dafny-lang/dafny/pull/3744)
+
+- The formatter now produces the same output whether invoked on the command-line or from VSCode (https://github.com/dafny-lang/dafny/pull/3790)
+
+- The --solver-log option is now hidden from help unless --help-internal is used. (https://github.com/dafny-lang/dafny/pull/3798)
+
+- Highlight "inconclusive" as errors in the gutter icons (https://github.com/dafny-lang/dafny/pull/3821)
+
+- Docstring for functions with ensures (https://github.com/dafny-lang/dafny/pull/3840)
+
+- Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name. (https://github.com/dafny-lang/dafny/pull/3860)
+
+- Improved rules for nameonly parameters and parameter default-value expressions (https://github.com/dafny-lang/dafny/pull/3864)
+
+- Fixes several compilation issues, mostly related to subset types defined by one of its type parameter (https://github.com/dafny-lang/dafny/pull/3893)
+
+- Explicitly define inequality of `multiset`s in Python for better backwards compatibility (https://github.com/dafny-lang/dafny/pull/3904)
+
+- Format for comprehension expressions (https://github.com/dafny-lang/dafny/pull/3912)
+
+- Formatting for parameter default values (https://github.com/dafny-lang/dafny/pull/3944)
+
+- Formatting issue in forall statement range (https://github.com/dafny-lang/dafny/pull/3960)
+
+- Select alternative default calc operator only if it doesn't clash with given step operators (https://github.com/dafny-lang/dafny/pull/3963)
+
 # 4.0.0
 
 ## Breaking changes

Scripts/package.py

@@ -236,28 +236,20 @@ def pack(args, releases):
 def check_version_cs(args):
  # Checking Directory.Build.props
  with open(path.join(SOURCE_DIRECTORY, "Directory.Build.props")) as fp:
- match = re.search(r'\<VersionPrefix\>([0-9]+.[0-9]+.[0-9]+).([0-9]+)', fp.read())
+ match = re.search(r'\<VersionPrefix\>([0-9]+.[0-9]+.[0-9]+)', fp.read())
  if match:
- (v1, v2) = match.groups()
+ source_version = match.groups()[0]
  else:
  flush("The AssemblyVersion attribute in Directory.Build.props could not be found.")
  return False
- now = time.localtime()
- year = now[0]
- month = now[1]
- day = now[2]
- v3 = str(year-2018) + str(month).zfill(2) + str(day).zfill(2)
- if v2 != v3:
- flush("The date in Directory.Build.props does not agree with today's date: " + v3 + " vs. " + v2)
  if "-" in args.version:
  hy = args.version[:args.version.index('-')]
  else:
  hy = args.version
- if hy != v1:
- flush("The version number in Directory.Build.props does not agree with the given version: " + hy + " vs. " + v1)
- if (v2 != v3 or hy != v1):
+ if hy != source_version:
+ flush("The version number in Directory.Build.props does not agree with the given version: " + source_version + " vs. " + hy)
  return False
- flush("Creating release files for release \"" + args.version + "\" and internal version information: " + v1 + "." + v2)
+ flush("Creating release files for release \"" + args.version + "\" and internal version information: " + source_version)
  return True
 
 def parse_arguments():

Scripts/prepare_release.py

@@ -166,51 +166,28 @@ def delete(self):
 class Version(NamedTuple):
  """Support functions for version numbers.
 
- >>> v = Version.from_string("3.8.2-xyz", datetime.date(2022, 8, 1))
- >>> v.short
+ >>> v = Version.from_string("3.8.2-xyz")
+ >>> v.string
  '3.8.2-xyz'
- >>> v.full
- '3.8.2.40801-xyz'
- >>> v.comment
- 'Version 3.8.2, year 2018+4, month 8, day 1.'
  """
 
  VERSION_NUMBER_PATTERN = re.compile("^(?P<prefix>[0-9]+[.][0-9]+[.][0-9]+)(?P<identifier>-.+)?$")
 
  main: str # Main version number (1.2.3)
- date: datetime.date # Release date
  identifier: str # Optional marker ("alpha")
 
  @classmethod
- def from_string(cls, vernum: str, date: Optional[datetime.date]=None) -> Optional["Version"]:
+ def from_string(cls, vernum: str) -> Optional["Version"]:
  """Parse a short version string into a `Version` object."""
  if m := cls.VERSION_NUMBER_PATTERN.match(vernum):
  prefix, identifier = m.group("prefix", "identifier")
- date = date or datetime.date.today()
- return Version(prefix, date, identifier or "")
+ return Version(prefix, identifier or "")
  return None
 
  @property
- def year_delta(self):
- return self.date.year - 2018
-
- @property
- def short(self):
+ def string(self):
  return f"{self.main}{self.identifier}"
 
- @property
- def timestamp(self):
- return str((self.year_delta * 100 + self.date.month) * 100 + self.date.day)
-
- @property
- def full(self):
- return f"{self.main}.{self.timestamp}{self.identifier}"
-
- @property
- def comment(self):
- return (f"Version {self.main}, year 2018+{self.year_delta}, " +
- f"month {self.date.month}, day {self.date.day}.")
-
 class Release:
  REMOTE = "origin"
  NEWSFRAGMENTS_PATH = "docs/dev/news"
@@ -316,9 +293,7 @@ def _update_build_props_file(self) -> None:
  tail = version_element.tail
  version_element.clear()
  version_element.tail = tail
- version_element.text = vernum.full
- comment = ElementTree.Comment(vernum.comment)
- version_element.append(comment)
+ version_element.text = vernum.string
  xml.write(self.build_props_path, encoding="utf-8")
 
  def _create_release_branch(self):

Scripts/quicktest.out

@@ -1,4 +1,3 @@
-Using: ../../Scripts/dafny
 Should succeed
 
 Dafny program verifier finished with 1 verified, 0 errors

Scripts/quicktest.sh

@@ -10,7 +10,6 @@ if [ -n "$1" ]; then
 else
  DAFNY=$DIR/dafny
 fi
-echo "Using:" $DAFNY
 
 echo Should succeed
 $DAFNY verify a.dfy

Source/Dafny.sln

@@ -39,6 +39,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExte
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDriver.Test\DafnyDriver.Test.csproj", "{FD18CD43-4D20-42EB-93EF-12125C206D76}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
+EndProject
 EndProject
 Global
  GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -118,6 +120,10 @@ Global
  {FD18CD43-4D20-42EB-93EF-12125C206D76}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {FD18CD43-4D20-42EB-93EF-12125C206D76}.Release|Any CPU.ActiveCfg = Release|Any CPU
  {FD18CD43-4D20-42EB-93EF-12125C206D76}.Release|Any CPU.Build.0 = Release|Any CPU
+ {33C29F26-A27B-474D-B436-83EA615B09FC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {33C29F26-A27B-474D-B436-83EA615B09FC}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {33C29F26-A27B-474D-B436-83EA615B09FC}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {33C29F26-A27B-474D-B436-83EA615B09FC}.Release|Any CPU.Build.0 = Release|Any CPU
  EndGlobalSection
  GlobalSection(SolutionProperties) = preSolution
  HideSolutionNode = FALSE