added -b to re-check instructions, so that examples image is stored too

docs/index.html

@@ -223,13 +223,14 @@ <h2 id="compiling-and-running-benchmarks">Compiling and running benchmarks</h2>
 ./bench_kmp.sh -r
 cd sorting
 make run</code></pre>
-<p>This will run the binary search, KMP, and parallel sorting benchmarks. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.</p>
+<p>This will run the binary search, KMP, and parallel sorting benchmarks. In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.</p>
 <p>To render the sorting benchmark results as pdf file, type (still in sorting directory):</p>
 <pre><code>make report</code></pre>
+<p>This requires pdflatex with the pgfplots package.</p>
 <h2 id="re-checking-the-proofs">Re-Checking the Proofs</h2>
 <p>To re-check the proofs, run</p>
 <pre><code>  cd thys 
-  isabelle build -D.</code></pre>
+  isabelle build -b -D.</code></pre>
 <p>Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation. This will invoke Isabelle to check all proofs and re-generate the exported code.</p>
 <h3 id="regression-test-script">Regression Test Script</h3>
 <p>To run a quick regression test script</p>

docs/index.md

@@ -112,19 +112,22 @@ The main features are:
     make run
 
   This will run the binary search, KMP, and parallel sorting benchmarks.
+  In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required.
   Warning: We have only tested this on a Linux x86_64 platform so far. 
   We do not (yet) know how LLVM will digest our code on other platforms.
 
   To render the sorting benchmark results as pdf file, type (still in sorting directory):
 
     make report
 
+  This requires pdflatex with the pgfplots package.
+
 
 ## Re-Checking the Proofs
   To re-check the proofs, run
 
       cd thys 
-      isabelle build -D.
+      isabelle build -b -D.
 
   Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation.
   This will invoke Isabelle to check all proofs and re-generate the exported code.

index.in.md

@@ -112,19 +112,22 @@ The main features are:
     make run
 
   This will run the binary search, KMP, and parallel sorting benchmarks.
+  In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required.
   Warning: We have only tested this on a Linux x86_64 platform so far. 
   We do not (yet) know how LLVM will digest our code on other platforms.
 
   To render the sorting benchmark results as pdf file, type (still in sorting directory):
 
     make report
 
+  This requires pdflatex with the pgfplots package.
+
 
 ## Re-Checking the Proofs
   To re-check the proofs, run
 
       cd thys 
-      isabelle build -D.
+      isabelle build -b -D.
 
   Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation.
   This will invoke Isabelle to check all proofs and re-generate the exported code.

index.md

@@ -112,19 +112,22 @@ The main features are:
     make run
 
   This will run the binary search, KMP, and parallel sorting benchmarks.
+  In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required.
   Warning: We have only tested this on a Linux x86_64 platform so far. 
   We do not (yet) know how LLVM will digest our code on other platforms.
 
   To render the sorting benchmark results as pdf file, type (still in sorting directory):
 
     make report
 
+  This requires pdflatex with the pgfplots package.
+
 
 ## Re-Checking the Proofs
   To re-check the proofs, run
 
       cd thys 
-      isabelle build -D.
+      isabelle build -b -D.
 
   Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation.
   This will invoke Isabelle to check all proofs and re-generate the exported code.