Fixed doo files

dafny-lang · Aug 28, 2024 · 80e7fc3 · 80e7fc3
1 parent 2d8f49a
commit 80e7fc3
Show file tree

Hide file tree

Showing 16 changed files with 6 additions and 1 deletion.
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
diff --git a/...rgetSpecific/FileIOInternalExterns-go.dfy → ...getSpecific/FileIO1InternalExterns-go.dfy b/...rgetSpecific/FileIOInternalExterns-go.dfy → ...getSpecific/FileIO1InternalExterns-go.dfy
diff --git a/...ific/FileIOInternalExterns-java-cs-js.dfy → ...fic/FileIO1InternalExterns-java-cs-js.dfy b/...ific/FileIOInternalExterns-java-cs-js.dfy → ...fic/FileIO1InternalExterns-java-cs-js.dfy
diff --git a/...rnalExterns-notarget-java-cs-js-go-py.dfy → ...rnalExterns-notarget-java-cs-js-go-py.dfy b/...rnalExterns-notarget-java-cs-js-go-py.dfy → ...rnalExterns-notarget-java-cs-js-go-py.dfy
diff --git a/...rgetSpecific/FileIOInternalExterns-py.dfy → ...getSpecific/FileIO1InternalExterns-py.dfy b/...rgetSpecific/FileIOInternalExterns-py.dfy → ...getSpecific/FileIO1InternalExterns-py.dfy
diff --git a/...ific/FileIO-notarget-java-cs-js-go-py.dfy → ...fic/FileIO2-notarget-java-cs-js-go-py.dfy b/...ific/FileIO-notarget-java-cs-js-go-py.dfy → ...fic/FileIO2-notarget-java-cs-js-go-py.dfy
diff --git 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.
diff --git a/...s/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect b/...s/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/test.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/test.doo
diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo