Merge pull request #1067 from hacspec/minor-fixes-book

feat(book): allow F* extraction + TC from within the book

book/book.toml

@@ -7,4 +7,9 @@ title = "hax"
 
 [output.html]
 mathjax-support = true
+additional-css = ["static/custom.css"]
+additional-js = ["theme/fstar.js", "theme/lz-string.js", "theme/ansi_up.js"]
 
+[output.html.playground]
+runnable = true
+editable = true

book/default.nix

@@ -9,7 +9,6 @@ stdenv.mkDerivation {
   buildPhase = ''
             mdbook build
             mdbook build archive -d ../book/archive
-            bash ./postprocess.sh
           '';
   installPhase = "mv book $out";
 }

book/src/SUMMARY.md

@@ -1,17 +1,21 @@
 # Summary
 
 - [Introduction](./readme.md)
-- [Examples]()
 - [Quick start](quick_start/intro.md)
 - [Tutorial](tutorial/readme.md)
     - [Panic freedom](tutorial/panic-freedom.md)
     - [Properties on functions](tutorial/properties.md)
     - [Data invariants](tutorial/data-invariants.md)
+- [Examples](examples/intro.md)
+    - [Rust By Example](examples/rust-by-examples/intro.md)
+    - [Using the F* backend](examples/fstar/intro.md)
+    - [Using the Coq backend](examples/coq/intro.md)
+    - [Using the ProVerif backend](examples/coq/intro.md)
 - [Proofs]()
     - [F*]()
     - [Coq]()
     - [`libcore`]()
-- [Troubleshooting/FAQ](faq/into.md)
+- [Troubleshooting/FAQ](faq/intro.md)
     - [Command line usage]()
        - [The include flag: which items should be extracted, and how?](faq/include-flags.md)
 - [Contributing]()

book/src/examples/coq/intro.md

@@ -0,0 +1 @@
+# Using the ProVerif backend

book/src/examples/fstar/intro.md

@@ -0,0 +1 @@
+# Using the F* backend

book/src/examples/intro.md

@@ -0,0 +1,12 @@
+# Examples
+
+This chapter contains various examples that demonstrates how hax can
+be used to prove properties about programs. Each example is
+self-contained. hax being a tool that can extract Rust to various
+backends, this section provides examples for each backend.
+
+The first subsection takes some examples from [Rust by
+Example](https://doc.rust-lang.org/rust-by-example/), and shows how to
+prove properties on them.
+
+The other sections present backend-specific examples.

book/src/examples/rust-by-examples/intro.md

@@ -0,0 +1 @@
+# Rust By Example

book/src/faq/into.md

@@ -1,3 +1 @@
 # Troubleshooting/FAQ
-
-This chapter captures a list of common questions or issues and how to resolve them. If you happen to run into an issue that is not documented here, please consider submitting a pull request!

book/src/faq/intro.md

@@ -0,0 +1,3 @@
+# Troubleshooting/FAQ
+
+This chapter captures a list of common questions or issues and how to resolve them. If you happen to run into an issue that is not documented here, please consider submitting a pull request!

book/src/quick_start/intro.md

@@ -5,9 +5,9 @@ what you are looking for!
 
 ## Setup the tools
 
- - **user-checkable** [Install the hax toolchain](https://github.com/hacspec/hax?tab=readme-ov-file#installation).  
+ - <input type="checkbox" class="user-checkable"/> [Install the hax toolchain](https://github.com/hacspec/hax?tab=readme-ov-file#installation).  
    <span style="margin-right:30px;"></span>🪄 Running `cargo hax --version` should print some version info.
- - **user-checkable** [Install F*](https://github.com/FStarLang/FStar/blob/master/INSTALL.md) *(optional: only if want to run F\*)*
+ - <input type="checkbox" class="user-checkable"/> [Install F*](https://github.com/FStarLang/FStar/blob/master/INSTALL.md) *(optional: only if want to run F\*)*
 
 ## Setup the crate you want to verify
 
@@ -16,11 +16,11 @@ what you are looking for!
 *Note: this part is useful only if you want to run F\*.*
 
 
- - **user-checkable** Create the folder `proofs/fstar/extraction` folder, right next to the `Cargo.toml` of the crate you want to verify.  
+ - <input type="checkbox" class="user-checkable"/> Create the folder `proofs/fstar/extraction` folder, right next to the `Cargo.toml` of the crate you want to verify.  
    <span style="margin-right:30px;"></span>🪄 `mkdir -p proofs/fstar/extraction`
- - **user-checkable** Copy [this makefile](https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3) to `proofs/fstar/extraction/Makefile`.  
+ - <input type="checkbox" class="user-checkable"/> Copy [this makefile](https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3) to `proofs/fstar/extraction/Makefile`.  
    <span style="margin-right:30px;"></span>🪄 `curl -o proofs/fstar/extraction/Makefile https://gist.githubusercontent.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3/raw/Makefile`
- - **user-checkable** Add `hax-lib` as a dependency to your crate, enabled only when using hax.  
+ - <input type="checkbox" class="user-checkable"/> Add `hax-lib` as a dependency to your crate, enabled only when using hax.  
    <span style="margin-right:30px;"></span>🪄 `cargo add --target 'cfg(hax)' --git https://github.com/hacspec/hax hax-lib`  
    <span style="margin-right:30px;"></span><span style="opacity: 0;">🪄</span> *(`hax-lib` is not mandatory, but this guide assumes it is present)*