diff --git a/Makefile b/Makefile index d6d9295fa64..273bd2dad69 100644 --- a/Makefile +++ b/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 diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index a934cb41aa6..2e52b713dfc 100644 --- a/RELEASE_NOTES.md +++ b/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 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index f8a1eafca1c..21538812c88 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index 280c19c8f20..2fb315557b7 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index e769ed9dec9..a86c4511f64 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 2fbac7113ae..0ad15aebf4a 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index 21ecd959efc..048ddffc1cb 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index 4a3d8097175..5df5db0f7e5 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index 4d0fbaefba8..dc3dc21dc2f 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy similarity index 100% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO1InternalExterns-go.dfy diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO2InternalExterns-java-cs-js.dfy similarity index 100% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO2InternalExterns-java-cs-js.dfy diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO3InternalExterns-notarget-java-cs-js-go-py.dfy similarity index 100% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget-java-cs-js-go-py.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO3InternalExterns-notarget-java-cs-js-go-py.dfy diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO4InternalExterns-py.dfy similarity index 100% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-py.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO4InternalExterns-py.dfy diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO5-notarget-java-cs-js-go-py.dfy similarity index 100% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIO5-notarget-java-cs-js-go-py.dfy diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Makefile b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Makefile index 3e6c7bb7ee5..eea7d40b13a 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Makefile +++ b/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 diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/README.md b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/README.md index dc0ec146d7b..b4349bc604a 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/README.md +++ b/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. \ No newline at end of file diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 7a84fbde9b3..df8725f3a0f 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,7 +1,7 @@ - 4.7.0 + 4.8.0 1701;1702;VSTHRD200 diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index f770c2141f2..b91a4b5fa44 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -132,6 +132,12 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable 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 } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect index a576b648061..e6ff8236390 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DerivedModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DerivedModule.dfy index 696c15acf2d..b95ecb1d1b1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DerivedModule.dfy +++ b/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 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/dafnysource/helloworld.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/dafnysource/helloworld.dfy new file mode 100644 index 00000000000..75e0ff227c4 --- /dev/null +++ b/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"; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr index c09c81885fb..d9d364ca0a9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test-go.dtr +++ b/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" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo index 88dc9758460..507fc7e0335 100644 Binary files a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo and b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo differ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/helloworld.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/helloworld.dfy index 3b364b53539..07344c82f78 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/helloworld.dfy +++ b/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 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy index 6c6249d642e..a826a16f675 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr index a5ed5313788..8875c24a626 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr +++ b/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" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo index 273681f03c9..d02fd1ee749 100644 Binary files a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo and b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo differ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/dafnysource/helloworld.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/dafnysource/helloworld.dfy new file mode 100644 index 00000000000..75e0ff227c4 --- /dev/null +++ b/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"; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo index fb96ed004fd..984fce8d142 100644 Binary files a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo and b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo differ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr index e495416f648..b5896b46691 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr +++ b/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" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy index 063cd71c1f0..077d23f3902 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy +++ b/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 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy new file mode 100644 index 00000000000..5f5d4774b84 --- /dev/null +++ b/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"; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy index d437246e530..957ee79b501 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy +++ b/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 { diff --git a/Source/XUnitExtensions/Lit/CpCommand.cs b/Source/XUnitExtensions/Lit/CpCommand.cs new file mode 100644 index 00000000000..add922a2ddf --- /dev/null +++ b/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 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}"; + } + } +} diff --git a/Source/XUnitExtensions/Lit/ExitCommand.cs b/Source/XUnitExtensions/Lit/ExitCommand.cs index ccbd6b8948b..ba119cf6694 100644 --- a/Source/XUnitExtensions/Lit/ExitCommand.cs +++ b/Source/XUnitExtensions/Lit/ExitCommand.cs @@ -1,3 +1,4 @@ +using System.ComponentModel; using System.IO; using System.Threading.Tasks; @@ -5,18 +6,27 @@ 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 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; } diff --git a/Source/XUnitExtensions/Lit/LitRunCommand.cs b/Source/XUnitExtensions/Lit/LitRunCommand.cs index 1281639d27e..7c15266857f 100644 --- a/Source/XUnitExtensions/Lit/LitRunCommand.cs +++ b/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); } diff --git a/Source/XUnitExtensions/Lit/MvCommand.cs b/Source/XUnitExtensions/Lit/MvCommand.cs new file mode 100644 index 00000000000..8ab0a593516 --- /dev/null +++ b/Source/XUnitExtensions/Lit/MvCommand.cs @@ -0,0 +1,57 @@ +using System; +using System.IO; +using System.Text.RegularExpressions; +using System.Threading.Tasks; +using Xunit; +using Xunit.Abstractions; +using Xunit.Sdk; + +namespace XUnitExtensions.Lit { + public class MvCommand : ILitCommand { + + private readonly string fileOrFolder; + private readonly string destination; + + private MvCommand(string fileOrFolder, string destination) { + this.fileOrFolder = fileOrFolder; + this.destination = destination; + } + + public static ILitCommand Parse(string[] args) { + if (args.Length != 2) { + throw new ArgumentException($"Wrong number of arguments for mv, expected 2 but got {args.Length}"); + } + var fileOrFolder = args[0]; + var destination = args[1]; + + return new MvCommand(fileOrFolder, destination); + } + + public async Task Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { + if (File.Exists(fileOrFolder)) { + try { + File.Move(fileOrFolder, destination); + } catch (Exception e) { + await outputWriter.WriteLineAsync(e.ToString()); + return 1; + } + } else if (Directory.Exists(fileOrFolder)) { + try { + Directory.Move(fileOrFolder, destination); + } 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 $"%mv {fileOrFolder} {destination}"; + } + } +} diff --git a/Source/XUnitExtensions/Lit/RmCommand.cs b/Source/XUnitExtensions/Lit/RmCommand.cs new file mode 100644 index 00000000000..6b1cee23842 --- /dev/null +++ b/Source/XUnitExtensions/Lit/RmCommand.cs @@ -0,0 +1,85 @@ +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 RmCommand : ILitCommand { + + private readonly string options; + private readonly string fileOrFolder; + + private RmCommand(string options, string fileOrFolder) { + this.options = options; + this.fileOrFolder = fileOrFolder; + } + + public static ILitCommand Parse(string[] args) { + if (args.Length != 1 && args.Length != 2) { + throw new ArgumentException($"Wrong number of arguments for rm, expected 1 or 2 but got {args.Length}"); + } + + string fileOrFolder; + string options; + if (args.Length == 2) { + options = args[0]; + fileOrFolder = args[1]; + } else { + options = ""; + fileOrFolder = args[0]; + } + + return new RmCommand(options, fileOrFolder); + } + private static void RecursiveDelete(DirectoryInfo baseDir) { + if (!baseDir.Exists) { + return; + } + + foreach (var dir in baseDir.EnumerateDirectories()) { + RecursiveDelete(dir); + } + baseDir.Delete(true); + } + public async Task Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { + if (File.Exists(fileOrFolder)) { + try { + File.Delete(fileOrFolder); + } catch (Exception e) { + await outputWriter.WriteLineAsync(e.ToString()); + return 1; + } + } else if (Directory.Exists(fileOrFolder)) { + if (Directory.EnumerateFiles(fileOrFolder).Any()) { + if (options == "-rf") { + RecursiveDelete(new DirectoryInfo(fileOrFolder)); + } else { + await outputWriter.WriteLineAsync("Directory is not empty. Please supply rm with -rf to force deletion"); + return 1; + } + } else { + try { + Directory.Delete(fileOrFolder); + } catch (Exception e) { + await outputWriter.WriteLineAsync(e.ToString()); + return 1; + } + } + } else { + await outputWriter.WriteLineAsync($"File or folder {fileOrFolder} not found"); + return 1; + } + + return 0; + } + + public override string ToString() { + return $"%rm {(options != "" ? options + " " : "")}{fileOrFolder}"; + } + } +} diff --git a/Source/XUnitExtensions/Lit/SedCommand.cs b/Source/XUnitExtensions/Lit/SedCommand.cs index ecffc218cfd..5cb212cb2c8 100644 --- a/Source/XUnitExtensions/Lit/SedCommand.cs +++ b/Source/XUnitExtensions/Lit/SedCommand.cs @@ -22,7 +22,7 @@ private SedCommand(string regexp, string replaceBy, string file) { public static ILitCommand Parse(string[] args) { if (args.Length != 2) { - throw new ArgumentException($"Wrong number of arguments for sed: {args.Length}"); + throw new ArgumentException($"Wrong number of arguments for sed, expected 2 but got {args.Length}"); } var regexpReplace = args[0]; var delimitCharacter = regexpReplace[1]; diff --git a/Source/XUnitExtensions/Lit/ShellLitCommand.cs b/Source/XUnitExtensions/Lit/ShellLitCommand.cs index 3a3cd052ecc..50bdf1fb2f2 100644 --- a/Source/XUnitExtensions/Lit/ShellLitCommand.cs +++ b/Source/XUnitExtensions/Lit/ShellLitCommand.cs @@ -23,6 +23,12 @@ public async Task Execute(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter) { using var process = new Process(); + if (shellCommand.Contains('/') && Path.GetFileName(shellCommand) is var command and "python3") { + var workingDir = Path.GetDirectoryName(shellCommand); + process.StartInfo.WorkingDirectory = workingDir; + shellCommand = command; + } + process.StartInfo.FileName = shellCommand; foreach (var argument in Arguments) { process.StartInfo.ArgumentList.Add(argument); diff --git a/docs/dev/news/5562.feat b/docs/dev/news/5562.feat deleted file mode 100644 index fc1f5198b4f..00000000000 --- a/docs/dev/news/5562.feat +++ /dev/null @@ -1 +0,0 @@ -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. \ No newline at end of file diff --git a/docs/dev/news/5587.fix b/docs/dev/news/5587.fix deleted file mode 100644 index 4bee448a1c1..00000000000 --- a/docs/dev/news/5587.fix +++ /dev/null @@ -1 +0,0 @@ -Clarify error location of inlined `is` predicates. \ No newline at end of file diff --git a/docs/dev/news/5589.fix b/docs/dev/news/5589.fix deleted file mode 100644 index 1af9c03533a..00000000000 --- a/docs/dev/news/5589.fix +++ /dev/null @@ -1 +0,0 @@ -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. \ No newline at end of file diff --git a/docs/dev/news/5631.feat b/docs/dev/news/5631.feat deleted file mode 100644 index 70a4d27e91a..00000000000 --- a/docs/dev/news/5631.feat +++ /dev/null @@ -1,5 +0,0 @@ -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 -... \ No newline at end of file diff --git a/docs/dev/news/5632.feat b/docs/dev/news/5632.feat deleted file mode 100644 index 344a92fc603..00000000000 --- a/docs/dev/news/5632.feat +++ /dev/null @@ -1 +0,0 @@ -Enable the option `--enforce-determinism` for the commands `resolve` and `verify` \ No newline at end of file diff --git a/docs/dev/news/5638.fix b/docs/dev/news/5638.fix deleted file mode 100644 index a9766728ba7..00000000000 --- a/docs/dev/news/5638.fix +++ /dev/null @@ -1 +0,0 @@ -Crash when compiling an empty source file while including testing code diff --git a/docs/dev/news/5645.fix b/docs/dev/news/5645.fix deleted file mode 100644 index 19b4b1af427..00000000000 --- a/docs/dev/news/5645.fix +++ /dev/null @@ -1 +0,0 @@ -Let the options --print-mode=NoGhostOrIncludes and --print-mode=NoIncludes work \ No newline at end of file diff --git a/docs/dev/news/5650.fix b/docs/dev/news/5650.fix deleted file mode 100644 index 0745e66f118..00000000000 --- a/docs/dev/news/5650.fix +++ /dev/null @@ -1 +0,0 @@ -Verification in the IDE now works correctly when declaring nested module in a different file than their parent. \ No newline at end of file diff --git a/docs/dev/news/5655.fix b/docs/dev/news/5655.fix deleted file mode 100644 index ff4ac95cead..00000000000 --- a/docs/dev/news/5655.fix +++ /dev/null @@ -1 +0,0 @@ -Fix NRE that would occur when using --legacy-data-constructors \ No newline at end of file diff --git a/docs/dev/news/5662.feat b/docs/dev/news/5662.feat deleted file mode 100644 index 15c238b1d5e..00000000000 --- a/docs/dev/news/5662.feat +++ /dev/null @@ -1 +0,0 @@ -Method calls get an optional by-proof that hides the precondtion and its proof