Release 4.8.0

Makefile

@@ -93,6 +93,9 @@ update-go-module:
 update-runtime-dafny:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
 
+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

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

Source/DafnyStandardLibraries/src/Std/TargetSpecific/Makefile

@@ -19,7 +19,7 @@ verify-all: update-binary-all
 
 build-binary:
 	$(DAFNY) build -t:lib --hidden-no-verify=$(NO_VERIFY) dfyconfig.toml \
-		`find . -name '*-${TARGETLANG}*.dfy'` \
+		`find . -name '*-${TARGETLANG}*.dfy' | sort` \
 		--output:${DOO_FILE_SOURCE}
 
 check-binary: build-binary

Source/DafnyStandardLibraries/src/Std/TargetSpecific/README.md

@@ -40,3 +40,8 @@ is shared between concurrent executions
 (see [the `{:concurrent}` attribute](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-concurrent-attribute)).
 It cannot currently offer any other guarantees related to concurrent execution,
 such as freedom from deadlocks.
+
+## Notes about naming
+
+Currently, replacement modules should appear in files before the files containing modules that include them, [issue tracked here](https://github.com/dafny-lang/dafny/issues/5728).
+Therefore, until that issue is fixed, it might be advisable to add a number in your files to make the order deterministic, as the "find" command might have different outputs based on the OS.

Source/Directory.Build.props

@@ -1,7 +1,7 @@
 <Project>
 
   <PropertyGroup>
-    <VersionPrefix>4.7.0</VersionPrefix>
+    <VersionPrefix>4.8.0</VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>
 

Source/IntegrationTests/LitTests.cs

@@ -132,6 +132,12 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
           "%diff", (args, config) => DiffCommand.Parse(args.ToArray())
         }, {
           "%sed", (args, config) => SedCommand.Parse(args.ToArray())
+        }, {
+          "%mv", (args, config) => MvCommand.Parse(args.ToArray())
+        }, {
+          "%rm", (args, config) => RmCommand.Parse(args.ToArray())
+        }, {
+          "%cp", (args, config) => CpCommand.Parse(args.ToArray())
         }, {
           "%OutputCheck", OutputCheckCommand.Parse
         }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect

@@ -4,5 +4,5 @@ CLI: Error: malformed dtr file NoGood.dtr
 Translation was aborted because errors were found
 
 Dafny program verifier finished with 0 verified, 0 errors
-CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.7.0.0
+CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.8.0.0
 Translation was aborted because errors were found

Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DerivedModule.dfy

@@ -1,7 +1,8 @@
 // RUN: %baredafny translate go  --go-module-name=GoModule2 --library="%S/test.doo" --translation-record "%S/test-go.dtr" --output "%S/test3" "%s"
-// RUN: cp -r "%S/go.*" "%S/test3-go/"
-// RUN: cp -r "%S/../../../../../../../../../DafnyRuntime/DafnyRuntimeGo-gomod" "%S"
-// RUN: cp -r "%S/DafnyModule1" "%S/test3-go/"
+// RUN: %cp -rf "%S/go.mod" "%S/test3-go/go.mod"
+// RUN: %cp -rf "%S/go.sum" "%S/test3-go/go.sum"
+// RUN: %cp -rf "%S/../../../../../../../../../DafnyRuntime/DafnyRuntimeGo-gomod" "%S"
+// RUN: %cp -rf "%S/DafnyModule1" "%S/test3-go/"
 // RUN: go run -C %S/test3-go/ test3.go > %t
 // RUN: %diff "%s.expect" "%t"
 module DafnyModule3 {

Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/dafnysource/helloworld.dfy

@@ -0,0 +1,9 @@
+// This file is used to regenerate PythonModule1.doo
+// RUN: echo 'lit should ignore this file' 
+
+module DafnyModule1 {
+  method HelloWorld()
+  {
+    print "Hello World";
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr

@@ -1,4 +1,4 @@
 file_format_version = "1.0"
-dafny_version = "4.7.0.0"
+dafny_version = "4.8.0.0"
 [options_by_module.DafnyModule1]
 go-module-name = "GoModule1"

Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/helloworld.dfy

@@ -1,6 +1,7 @@
 // RUN: %baredafny translate go  --go-module-name=GoModule1 "%s" --output "%S/test"
-// RUN: cp -r "%S/go.*" "%S/test-go/"
-// RUN: cp -r "%S/../../../../../../../../../../DafnyRuntime/DafnyRuntimeGo-gomod" "%S"
+// RUN: %cp -rf "%S/go.mod" "%S/test-go/go.mod"
+// RUN: %cp -rf "%S/go.sum" "%S/test-go/go.sum"
+// RUN: %cp -rf "%S/../../../../../../../../../../DafnyRuntime/DafnyRuntimeGo-gomod" "%S"
 // RUN: go run -C %S/test-go/ test.go > %t
 // RUN: %diff "%s.expect" "%t"
 module DafnyModule1 {

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy

@@ -1,8 +1,8 @@
-// RUN: %baredafny translate py  --python-module-name=PythonModule2 --library="%S/PythonModule1.doo" --translation-record "%S/PythonModule1-py.dtr" --output "%S/PythonModule2" "%s"
-// RUN: rm -rf "%S/PythonModule2"
-// RUN: mv "%S/PythonModule2-py" "%S/PythonModule2"
+// RUN: %baredafny translate py  --python-module-name=PythonModule2 --library="%S/PythonModule1.doo" --translation-record "%S/PythonModule1-py.dtr" --output "%S/PythonModule2" "%s" --include-runtime
+// RUN: %exits-with -any %rm -rf "%S/PythonModule2"
+// RUN: %mv "%S/PythonModule2-py" "%S/PythonModule2"
 // RUN: pip3 install "%S"
-// RUN: python3 %S/PythonModule2/ > %t
+// RUN: %S/python3 PythonModule2/ > %t
 // RUN: %diff "%s.expect" "%t"
 module DafnyModule3 {
 import DafnyModule1

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr

@@ -1,4 +1,4 @@
 file_format_version = "1.0"
-dafny_version = "4.7.0.0"
+dafny_version = "4.8.0.0"
 [options_by_module.DafnyModule1]
 python-module-name = "PythonModule1"

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/dafnysource/helloworld.dfy

@@ -0,0 +1,9 @@
+// This file is used to regenerate PythonModule1.doo
+// RUN: echo 'lit should ignore this file' 
+
+module DafnyModule1 {
+  method HelloWorld()
+  {
+    print "Hello World";
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr

@@ -1,4 +1,4 @@
 file_format_version = "1.0"
-dafny_version = "4.7.0.0"
+dafny_version = "4.8.0.0"
 [options_by_module."Some.Nested.Module"]
 python-module-name = "SomeNestedModule"

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy

@@ -1,6 +1,6 @@
 // RUN: pip3 install "%S"
-// RUN: %baredafny translate py --output "%S/SomeTestModule" --library="%S/SomeNestedModule.doo" --translation-record "%S/SomeNestedModule/SomeNestedModule-py.dtr" "%s"
-// RUN: python3 %S/SomeTestModule-py/ > %t
+// RUN: %baredafny translate py --output "%S/SomeTestModule" --library="%S/SomeNestedModule.doo" --translation-record "%S/SomeNestedModule/SomeNestedModule-py.dtr" "%s" --include-runtime
+// RUN: %S/python3 SomeTestModule-py/ > %t
 // RUN: %diff "%s.expect" "%t"
 module SomeTestModule {
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy

@@ -0,0 +1,9 @@
+// This file is used to regenerate SomeNestedModule.doo
+// RUN: echo 'lit should ignore this file' 
+
+module Some.Nested.Module {
+  method HelloWorld()
+  {
+    print "Hello World";
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy

@@ -1,8 +1,8 @@
-// RUN: %baredafny translate py  --python-module-name=PythonModule1 "%s" --output "%S/PythonModule1"
-// RUN: rm -rf "%S/PythonModule1"
-// RUN: mv "%S/PythonModule1-py/" "%S/PythonModule1"
+// RUN: %baredafny translate py  --python-module-name=PythonModule1 "%s" --output "%S/PythonModule1" --include-runtime
+// RUN: %exits-with -any %rm -rf "%S/PythonModule1"
+// RUN: %mv "%S/PythonModule1-py/" "%S/PythonModule1"
 // RUN: pip3 install "%S"
-// RUN: python3 %S/PythonModule1/ > %t
+// RUN: %S/python3 PythonModule1/ > %t
 // RUN: %diff "%s.expect" "%t"
 module DafnyModule1 {
 

Source/XUnitExtensions/Lit/CpCommand.cs

@@ -0,0 +1,107 @@
+using System;
+using System.IO;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading.Tasks;
+using Xunit;
+using Xunit.Abstractions;
+using Xunit.Sdk;
+
+namespace XUnitExtensions.Lit {
+  public class CpCommand : ILitCommand {
+
+    private readonly string options;
+    private readonly string fileOrFolder;
+    private readonly string destination;
+
+    private CpCommand(string options, string fileOrFolder, string destination) {
+      this.options = options;
+      this.fileOrFolder = fileOrFolder;
+      this.destination = destination;
+    }
+
+    public static ILitCommand Parse(string[] args) {
+      if (args.Length != 2 && args.Length != 3) {
+        throw new ArgumentException($"Wrong number of arguments for cp, expected 2 or 3 but got {args.Length}: " + string.Join(", ", args));
+      }
+
+      string fileOrFolder;
+      string destination;
+      string options;
+
+      if (args.Length == 2) {
+        options = "";
+        fileOrFolder = args[0];
+        destination = args[1];
+      } else {
+        options = args[0];
+        fileOrFolder = args[1];
+        destination = args[2];
+      }
+      return new CpCommand(options, fileOrFolder, destination);
+    }
+    static void CopyDirectory(string sourceDir, string destinationDir, bool recursive, bool force) {
+      // Get information about the source directory
+      var dir = new DirectoryInfo(sourceDir);
+
+      // Check if the source directory exists
+      if (!dir.Exists)
+        throw new DirectoryNotFoundException($"Source directory not found: {dir.FullName}");
+
+      // Cache directories before we start copying
+      DirectoryInfo[] dirs = dir.GetDirectories();
+
+      // Create the destination directory
+      Directory.CreateDirectory(destinationDir);
+
+      // Get the files in the source directory and copy to the destination directory
+      foreach (FileInfo file in dir.GetFiles()) {
+        string targetFilePath = Path.Combine(destinationDir, file.Name);
+        if (force && File.Exists(targetFilePath)) {
+          File.Delete(targetFilePath);
+        }
+        file.CopyTo(targetFilePath);
+      }
+
+      // If recursive and copying subdirectories, recursively call this method
+      if (recursive) {
+        foreach (DirectoryInfo subDir in dirs) {
+          string newDestinationDir = Path.Combine(destinationDir, subDir.Name);
+          CopyDirectory(subDir.FullName, newDestinationDir, true, force);
+        }
+      }
+    }
+    public async Task<int> Execute(TextReader inputReader,
+      TextWriter outputWriter, TextWriter errorWriter) {
+      if (File.Exists(fileOrFolder)) {
+        try {
+          if (File.Exists(destination) && options.Contains('f')) {
+            File.Delete(destination);
+          }
+          File.Copy(fileOrFolder, destination);
+        } catch (Exception e) {
+          await outputWriter.WriteLineAsync(e.ToString());
+          return 1;
+        }
+      } else if (Directory.Exists(fileOrFolder)) {
+        try {
+          var actualDestination = Directory.Exists(destination)
+            ? Path.Combine(destination, Path.GetFileName(fileOrFolder))
+            : destination;
+          CopyDirectory(fileOrFolder, actualDestination, options.Contains('r'), options.Contains('f'));
+        } catch (Exception e) {
+          await outputWriter.WriteLineAsync(e.ToString());
+          return 1;
+        }
+      } else {
+        throw new ArgumentException("File or folder " + fileOrFolder + " not found");
+      }
+
+      return 0;
+    }
+
+    public override string ToString() {
+      return $"%cp {(options != "" ? options + " " : "")}{fileOrFolder} {destination}";
+    }
+  }
+}

Source/XUnitExtensions/Lit/ExitCommand.cs

@@ -1,22 +1,32 @@
+using System.ComponentModel;
 using System.IO;
 using System.Threading.Tasks;
 
 namespace XUnitExtensions.Lit;
 
 
 public class ExitCommand : ILitCommand {
-  private readonly int expectedExitCode;
+  private readonly string expectedExitCode;
   private readonly ILitCommand operand;
 
-  public ExitCommand(int exitCode, ILitCommand operand) {
+  public ExitCommand(string exitCode, ILitCommand operand) {
     this.expectedExitCode = exitCode;
     this.operand = operand;
   }
 
   public async Task<int> Execute(TextReader inputReader,
     TextWriter outputWriter, TextWriter errorWriter) {
-    var exitCode = await operand.Execute(inputReader, outputWriter, errorWriter);
-    if (exitCode == expectedExitCode) {
+    var exitCode = 1;
+    try {
+      exitCode = await operand.Execute(inputReader, outputWriter, errorWriter);
+    } catch (Win32Exception) {
+      if (expectedExitCode == "-any") {
+      } else {
+        throw;
+      }
+    }
+
+    if (expectedExitCode == "-any" || exitCode.ToString() == expectedExitCode) {
       return 0;
     }
 

Source/XUnitExtensions/Lit/LitRunCommand.cs

@@ -18,7 +18,7 @@ private static ILitCommand ParseArguments(Token[] tokens, LitTestConfiguration c
         return new NotCommand(operand);
       }
       if (tokens[0].Value == "%exits-with") {
-        var ec = Int32.Parse(tokens[1].Value);
+        var ec = tokens[1].Value;
         var operand = ParseArguments(tokens[2..], config);
         return new ExitCommand(ec, operand);
       }