Skip to content

Commit

Permalink
Remove support for C# and update readme (#115)
Browse files Browse the repository at this point in the history
By submitting this pull request, I confirm that my contribution is made
under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
  • Loading branch information
stefan-aws authored Nov 8, 2023
1 parent ee83a0e commit f627a24
Show file tree
Hide file tree
Showing 11 changed files with 9 additions and 124 deletions.
15 changes: 0 additions & 15 deletions .github/workflows/build_cs.yml

This file was deleted.

14 changes: 0 additions & 14 deletions .github/workflows/test_cs.yml

This file was deleted.

22 changes: 6 additions & 16 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# VMC: a Library for Verified Monte Carlo Algorithms

The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to C# and Java. For the future, we plan to extend both the functionality and the range of supported languages.
The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java. For the future, we plan to extend both the functionality and the range of supported languages.

There are two ways to use the library:
- The trait `DRandomFoundational` only needs fair coin flips as a primitive.
Expand All @@ -9,31 +9,21 @@ There are two ways to use the library:
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
$ 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
# 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

To run the statistical tests in the `tests` diretory, use one of the following commands:

```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
# 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
# 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
```
14 changes: 0 additions & 14 deletions build/cs/cs.csproj

This file was deleted.

5 changes: 0 additions & 5 deletions build/cs/run.sh

This file was deleted.

3 changes: 0 additions & 3 deletions docs/csharp/BuildTest.cs

This file was deleted.

3 changes: 0 additions & 3 deletions docs/csharp/index.html

This file was deleted.

4 changes: 1 addition & 3 deletions docs/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,4 @@
<br>
<a href="dafny/index.html">Using Dafny-VMC from Dafny</a>
<br>
<a href="java/index.html">Using Dafny-VMC from Java </a>
<br>
<a href="csharp/index.html">Using Dafny-VMC from C#</a>
<a href="java/index.html">Using Dafny-VMC from Java </a>
8 changes: 2 additions & 6 deletions scripts/test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -25,19 +25,15 @@ echo Running $TARGET_LANG documentation...
echo "Building docs/dafny/ExamplesFoundational.dfy..."
$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
echo "Executing compiled docs/dafny/ExamplesFoundational.dfy:"
if [ "$TARGET_LANG" = "cs" ]
if [ "$TARGET_LANG" = "java" ]
then
dotnet docs/dafny/ExamplesFoundational.dll
else
java -jar docs/dafny/ExamplesFoundational.jar
fi

echo "Building docs/dafny/ExamplesExternUniformPowerOfTwo.dfy..."
$DAFNY build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
echo "Executing compiled docs/dafny/ExamplesExternUniformPowerOfTwo.dfy:"
if [ "$TARGET_LANG" = "cs" ]
if [ "$TARGET_LANG" = "java" ]
then
dotnet docs/dafny/ExamplesExternUniformPowerOfTwo.dll
else
java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
fi
22 changes: 0 additions & 22 deletions src/interop/cs/DRandomCoin.cs

This file was deleted.

23 changes: 0 additions & 23 deletions src/interop/cs/DRandomUniformPowerOfTwo.cs

This file was deleted.

0 comments on commit f627a24

Please sign in to comment.