shell and readme

dafny-lang · Nov 8, 2023 · eb568d8 · eb568d8
1 parent 74012cc
commit eb568d8
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 17 deletions.
diff --git a/README.md b/README.md
@@ -10,17 +10,17 @@ To run the examples in the `docs` directory, use one of the following commands:
 
 ```bash
 # C# ExamplesFoundational
-$ dafny build docs/dafny/ExamplesFoundational.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs dfyconfig.toml --no-verify
+$ dafny build docs/dafny/ExamplesFoundational.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniformPowerOfTwo.cs dfyconfig.toml --no-verify
 $ dotnet docs/dafny/ExamplesFoundational.dll
 # C# ExamplesExternUniform
-$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs dfyconfig.toml --no-verify
-$ dotnet docs/dafny/ExamplesExternUniform.dll
+$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniformPowerOfTwo.cs dfyconfig.toml --no-verify
+$ dotnet docs/dafny/ExamplesExternUniformPowerOfTwo.dll
 # Java ExamplesFoundational
-$ dafny build docs/dafny/ExamplesFoundational.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java dfyconfig.toml --no-verify
+$ dafny build docs/dafny/ExamplesFoundational.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java dfyconfig.toml --no-verify
 $ java -jar docs/dafny/ExamplesFoundational.jar
 # Java ExamplesExternUniform
-$ dafny build docs/dafny/ExamplesExternUniform.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java dfyconfig.toml --no-verify
-$ java -jar docs/dafny/ExamplesExternUniform.jar
+$ dafny build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java dfyconfig.toml --no-verify
+$ java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
 ```
 
 # Testing
@@ -29,11 +29,11 @@ To run the statistical tests in the `tests` diretory, use one of the following c
 
 ```bash
 # C# TestsFoundational
-$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniformPowerOfTwo.cs tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 # C# TestsExternUniform
-$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniform.cs tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:cs src/interop/cs/DRandomCoin.cs src/interop/cs/DRandomUniformPowerOfTwo.cs tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 # Java TestsFoundational
-$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java tests/TestsFoundationalPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 # Java TestsExternUniform
-$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniform.java tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java tests/TestsExternUniformPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
diff --git a/scripts/prep.sh b/scripts/prep.sh
@@ -3,4 +3,8 @@
 VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.3.0/dafny-4.3.0-x64-ubuntu-20.04.zip
 
 wget $VERSION
-unzip `basename $VERSION` 
+unzip `basename $VERSION` 
+
+cd dafny
+dotnet add package System.Security.Cryptography.Algorithms --version 4.3.1
+cd ..
diff --git a/scripts/test.sh b/scripts/test.sh
@@ -14,12 +14,6 @@ then
   exit 1
 fi
 
-if [ "$TARGET_LANG" = "cs" ]
-then 
-  dotnet new console
-  dotnet add package System.Security.Cryptography.Algorithms --version 4.3.1
-fi
-
 echo Running $TARGET_LANG tests...
 echo "Running tests/TestsFoundational.dfy:"
 time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify