Fix documentation and comments (#167)

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).
dafny-lang · Mar 18, 2024 · 38e583e · 38e583e
1 parent be33d9d
commit 38e583e
Show file tree

Hide file tree

Showing 10 changed files with 30 additions and 16 deletions.
diff --git a/audit.log b/audit.log
@@ -1,3 +1,3 @@
 src/DafnyVMC.dfy(35,27): UniformSample32: Declaration has `{:verify false}` attribute. 
-src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(18,26): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
diff --git a/docs/dafny/index.html b/docs/dafny/index.html
@@ -2,4 +2,4 @@
 <br>
 <a href="dafny-doc/index.html">Dafny documentation</a>
 <br>
-<a href="ExamplesRandom.dfy">Example using the foundational uniform sampler</a>
+<a href="ExamplesRandom.dfy">Examples of Sampling</a>
diff --git a/docs/index.html b/docs/index.html
@@ -3,4 +3,6 @@
 <br>
 <a href="dafny/index.html">Using Dafny-VMC from Dafny</a>
 <br>
-<a href="java/index.html">Using Dafny-VMC from Java </a>
+<a href="java/index.html">Using Dafny-VMC from Java</a>
+<br>
+<a href="py/index.html">Using Dafny-VMC from Python</a>
diff --git a/docs/java/index.html b/docs/java/index.html
@@ -1,5 +1,7 @@
 Using the Dafny-VMC library in a Java application.
 <br>
-<a href="java-doc/index.html">Java documentation</a>
+<a href="java-doc/DafnyVMC/package-summary.html">Java documentation</a>
 <br>
-<a href="BuildTest.java">Example</a>
+<a href="TestSamplers.java">Examples of Sampling</a>
+<br>
+<a href="TestShuffling.java">Examples of Shuffling</a>
diff --git a/docs/py/index.html b/docs/py/index.html
@@ -0,0 +1,7 @@
+Using the Dafny-VMC library in a Python application.
+<br>
+<a href="py-doc/DafnyVMC.html">Python documentation</a>
+<br>
+<a href="TestSamplers.py">Examples of Sampling</a>
+<br>
+<a href="TestShuffling.py">Examples of Shuffling</a>
diff --git a/scripts/gendoc.sh b/scripts/gendoc.sh
@@ -18,6 +18,15 @@ echo Generating Dafny documentation...
 $DAFNY doc dfyconfig.toml --output docs/dafny/dafny-doc/
 
 echo Generating Java documentation...
-$DAFNY translate java src/Dafny-VMC.dfy --no-verify
-cp $DAFNYSOURCE/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/*.java src/Dafny-VMC-java/dafny/
-javadoc -d docs/java/java-doc/ -sourcepath src/Dafny-VMC-java -package DafnyVMC
+dafny translate java src/interop/java/Full/CustomRandom.java src/interop/java/Full/Random.java dfyconfig.toml -o src/DafnyVMC --no-verify --include-runtime
+mkdir src/DafnyVMC-java/DafnyVMC
+cp src/interop/java/Full/CustomRandom.java src/DafnyVMC-java/DafnyVMC
+cp src/interop/java/Full/Random.java src/DafnyVMC-java/DafnyVMC
+find src/DafnyVMC-java/ -type f -name "*.java" | xargs javadoc -d docs/java/java-doc/
+
+echo Generating Python documentation...
+export TARGET_LANG=py
+bash scripts/build.sh
+PYTHONPATH=.:build/py/DafnyVMC-py pydoc3 -w build/py/DafnyVMC-py/DafnyVMC.py
+mkdir docs/py/py-doc
+mv DafnyVMC.html docs/py/py-doc
diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
@@ -15,7 +15,6 @@ module Uniform.Model {
    Definitions
   ************/
 
-  // Definition 49
   ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
     requires n > 0
     ensures Independence.IsIndepFunction(h)

diff --git a/src/Math/Analysis/Reals.dfy b/src/Math/Analysis/Reals.dfy
@@ -3,11 +3,6 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-// Fundamental properties of the real numbers.
-// * States the completeness of the reals in terms of a variation of Dedekind cuts.
-//     Dafny should include such an axiom, but doesn't.
-//     See: https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers
-// * Proves existence and uniqueness of infima and suprema
 module Reals {
   import RealArith
 

diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy
@@ -4,6 +4,7 @@
  *******************************************************************************/
 
 module Helper {
+
   /************
    Definitions
   ************/

diff --git a/src/ProbabilisticProgramming/Monad.dfy b/src/ProbabilisticProgramming/Monad.dfy
@@ -16,8 +16,7 @@ module Monad {
   type Hurd<A> = Rand.Bitstream -> Result<A>
 
   // The result of a probabilistic computation on a bitstream.
-  // It either consists of the computed value and the (unconsumed) rest of the bitstream or indicates nontermination.
-  // It differs from Hurd's definition in that the result can be nontermination, which Hurd does not model explicitly.
+  // It consists of the computed value and the (unconsumed) rest of the bitstream.
   datatype Result<A> = Result(value: A, rest: Rand.Bitstream)
   {
     function Map<B>(f: A -> B): Result<B> {