allow warnings and interop

dafny-lang · Jul 26, 2024 · c9e23a7 · c9e23a7
1 parent d4c7d61
commit c9e23a7
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/scripts/test.sh b/scripts/test.sh
@@ -17,12 +17,12 @@ fi
 echo Running $TARGET_LANG tests...
 
 echo "Running tests/TestsRandom.dfy:"
-time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml  --no-verify
+time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml  --no-verify --allow-warnings
 
 echo Running $TARGET_LANG documentation...
 
 echo "Building docs/dafny/ExamplesRandom.dfy..." 
-time $DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG dfyconfig.toml --no-verify
+time $DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG dfyconfig.toml --no-verify --allow-warnings
 
 echo "Executing compiled docs/dafny/ExamplesRandom.dfy:" 
 if [ "$TARGET_LANG" = "java" ]

diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java
@@ -86,6 +86,10 @@ public java.math.BigInteger DiscreteGaussianSample(java.math.BigInteger num, jav
     return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den, mix);
   }
 
+  public dafny.Tuple2<Boolean, java.math.BigInteger> DiscreteLaplaceSampleLoop_k(java.math.BigInteger num, java.math.BigInteger den) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleLoop_k(this, num, den);
+  }
+
   public java.math.BigInteger DiscreteLaplaceSampleMixed(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger mix) {
     return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleMixed(this, num, den, mix);
   }