Merge pull request #361 from hacspec/doc

Docs (`rustdoc`, `odoc`): build and publish to gh-pages (via CI)

.github/workflows/gh_pages.yml

@@ -0,0 +1,41 @@
+name: Deploy documentation to GH Pages
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [main]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - uses: DeterminateSystems/nix-installer-action@main
+    - uses: DeterminateSystems/magic-nix-cache-action@main
+    - name: Build docs
+      run: nix build .#hax.docs --out-link ./_site
+    - name: Upload Pages artifact
+      uses: actions/upload-pages-artifact@v2
+
+  # deploys the result of `build`
+  # this job is a copy paste from <https://github.com/actions/deploy-pages>
+  deploy:
+    # Add a dependency to the build job
+    needs: build
+
+    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+    permissions:
+      pages: write      # to deploy to Pages
+      id-token: write   # to verify the deployment originates from an appropriate source
+
+    # Deploy to the github-pages environment
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+
+    # Specify runner + deployment step
+    runs-on: ubuntu-latest
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v2 # or the latest "vX.X.X" version tag for this action

cli/default.nix

@@ -44,6 +44,32 @@
     // {
       inherit cargoArtifacts pname;
     });
+  frontend-docs = craneLib.cargoDoc (commonArgs // {inherit cargoArtifacts pname;});
+  docs = stdenv.mkDerivation {
+    name = "hax-docs";
+    unpackPhase = "true";
+    buildPhase = "true";
+    installPhase = ''
+      mkdir $out
+      cp -r ${frontend-docs}/share/doc $out/frontend
+      cp -r ${hax-engine.docs}         $out/engine
+      cd $out
+      INDEX=$(mktemp)
+      (
+        echo "<style>"
+        echo "body {font-family: Sans-Serif; margin: 0px; padding: 20px;}"
+        echo "h1 {font-size: 140%;  font-weight: inherit;}"
+        echo "</style>"
+        echo "<h1>Hax docs</h1>"
+        echo "<p>Hax is written both in Rust and OCaml. Documentation for each is available below:</p>"
+        echo "<ul>"
+        echo "<li><a href=\"frontend/hax_frontend_exporter/index.html\">Frontend documentation</a> (Rust)</li>"
+        echo "<li><a href=\"engine/hax-engine/index.html\">Engine documentation</a> (OCaml)</li>"
+        echo "</ul>"
+      ) > $INDEX
+      mv $INDEX index.html
+    '';
+  };
   binaries = [hax hax-engine rustc gcc];
   tests = craneLib.buildPackage (commonArgs
     // {
@@ -77,6 +103,7 @@ in
     meta.mainProgram = "cargo-hax";
     passthru = {
       unwrapped = hax;
-      inherit tests;
+      engine-docs = hax-engine.docs;
+      inherit tests docs frontend-docs;
     };
   }

cli/options/src/lib.rs

@@ -215,23 +215,23 @@ pub struct BackendOptions {
     #[arg(long = "dry-run")]
     pub dry_run: bool,
 
-    /// Verbose mode for the Hax engine. Set [-vv] for maximal verbosity.
+    /// Verbose mode for the Hax engine. Set `-vv` for maximal verbosity.
     #[arg(short, long, action = clap::ArgAction::Count)]
     pub verbose: u8,
 
     /// Enable engine debugging: dumps the AST at each phase.
     ///
-    /// The value of <DEBUG_ENGINE> can be either:
+    /// The value of `<DEBUG_ENGINE>` can be either:
     ///
-    ///  - [interactive] (or [i]): enables debugging of the engine, and
-    /// visualize interactively in a webapp how a crate was
+    ///  - `interactive` (or `i`): enables debugging of the engine,
+    /// and visualize interactively in a webapp how a crate was
     /// transformed by each phase, both in Rust-like syntax and
     /// browsing directly the internal AST. By default, the webapp is
-    /// hosted on http://localhost:8000, the port can be override by
+    /// hosted on `http://localhost:8000`, the port can be override by
     /// setting the `HAX_DEBUGGER_PORT` environment variable.
     ///
-    /// - [<FILE>] or [file:<FILE>]: outputs the different AST as JSON
-    /// to <FILE>. <FILE> can be either [-] or a path.
+    /// - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
+    /// to `<FILE>`. `<FILE>` can be either [-] or a path.
     #[arg(short, long = "debug-engine")]
     pub debug_engine: Option<DebugEngineMode>,
 
@@ -242,9 +242,9 @@ pub struct BackendOptions {
 #[derive(JsonSchema, Subcommand, Debug, Clone, Serialize, Deserialize)]
 pub enum ExporterCommand {
     /// Translate to a backend. The translated modules will be written
-    /// under the directory [<PKG>/proofs/<BACKEND>/extraction], where
-    /// <PKG> is the translated cargo package name and <BACKEND> the
-    /// name of the backend.
+    /// under the directory `<PKG>/proofs/<BACKEND>/extraction`, where
+    /// `<PKG>` is the translated cargo package name and `<BACKEND>`
+    /// the name of the backend.
     #[clap(name = "into")]
     Backend(BackendOptions),
 
@@ -259,7 +259,7 @@ pub enum ExporterCommand {
         output_file: PathOrDash,
         /// Whether the bodies are exported as THIR, built MIR, const
         /// MIR, or a combination. Repeat this option to extract a
-        /// combination (e.g. [-k thir -k mir-built]).
+        /// combination (e.g. `-k thir -k mir-built`).
         #[arg(
             value_enum,
             short,
@@ -304,11 +304,11 @@ pub enum Command {
 #[command(author, version = concat!("commit=", env!("HAX_GIT_COMMIT_HASH"), " ", "describe=", env!("HAX_GIT_DESCRIBE")), name = "hax", about, long_about = None)]
 pub struct Options {
     /// Replace the expansion of each macro matching PATTERN by their
-    /// invocation. PATTERN denotes a rust path (i.e. [A::B::c]) in
+    /// invocation. PATTERN denotes a rust path (i.e. `A::B::c`) in
     /// which glob patterns are allowed. The glob pattern * matches
     /// any name, the glob pattern ** matches zero, one or more
-    /// names. For instance, [A::B::C::D::X] and [A::E::F::D::Y]
-    /// matches [A::**::D::*].
+    /// names. For instance, `A::B::C::D::X` and `A::E::F::D::Y`
+    /// matches `A::**::D::*`.
     #[arg(
         short = 'i',
         long = "inline-macro-call",
@@ -323,23 +323,23 @@ pub struct Options {
     pub inline_macro_calls: Vec<Namespace>,
 
     /// Semi-colon terminated list of arguments to pass to the
-    /// [cargo build] invocation. For example, to apply this
-    /// program on a package [foo], use [-C -p foo ;]. (make sure
-    /// to escape [;] correctly in your shell)
+    /// `cargo build` invocation. For example, to apply this
+    /// program on a package `foo`, use `-C -p foo ;`. (make sure
+    /// to escape `;` correctly in your shell)
     #[arg(default_values = Vec::<&str>::new(), short='C', allow_hyphen_values=true, num_args=1.., long="cargo-args", value_terminator=";")]
     pub cargo_flags: Vec<String>,
 
     #[command(subcommand)]
     pub command: Option<Command>,
 
-    /// [cargo] caching is disabled by default, this flag enables it back.
+    /// `cargo` caching is disabled by default, this flag enables it back.
     #[arg(long="enable-cargo-cache", action=clap::builder::ArgAction::SetTrue)]
     pub force_cargo_build: ForceCargoBuild,
 
     /// Apply the command to every local package of the dependency closure. By
     /// default, the command is only applied to the primary packages (i.e. the
     /// package(s) of the current directory, or the ones selected with cargo
-    /// options like [-C -p <PKG> ;]).
+    /// options like `-C -p <PKG> ;`).
     #[arg(long = "deps")]
     pub deps: bool,
 }

cli/subcommands/src/cargo_hax.rs

@@ -4,8 +4,8 @@ use hax_cli_options::NormalizePaths;
 use hax_cli_options::Options;
 use std::process::Command;
 
-/// Return a toolchain argument to pass to [cargo]: when the correct nightly is
-/// already present, this is None, otherwise we (1) ensure [rustup] is available
+/// Return a toolchain argument to pass to `cargo`: when the correct nightly is
+/// already present, this is None, otherwise we (1) ensure `rustup` is available
 /// (2) install the nightly (3) return the toolchain
 fn toolchain() -> Option<&'static str> {
     let current_rustc_version = version_check::triple()
@@ -27,9 +27,9 @@ fn toolchain() -> Option<&'static str> {
     }
 }
 
-/// [get_args] is a wrapper of `std::env::args` that strips a possible
-/// cargo subcommand. This allows for a binary [BINARY] to be called
-/// both with [cargo BINARY args...] and [cargo-BINARY args...].
+/// [`get_args`] is a wrapper of `std::env::args` that strips a possible
+/// cargo subcommand. This allows for a binary `BINARY` to be called
+/// both with `cargo BINARY args...` and `cargo-BINARY args...`.
 pub fn get_args(subcommand: &str) -> Vec<String> {
     let mut args: Vec<_> = std::env::args().collect();
     if args.get(1) == Some(&subcommand.to_string()) {
@@ -40,11 +40,11 @@ pub fn get_args(subcommand: &str) -> Vec<String> {
 }
 
 /// Our custom rustc driver will *not* be run in an proper terminal,
-/// thus logs would appear uncolored. When no RUST_LOG_STYLE env. var.
-/// is set, [rust_log_style] checks wether the [cargo hax] command was
+/// thus logs would appear uncolored. When no `RUST_LOG_STYLE` env. var.
+/// is set, [`rust_log_style`] checks wether the `cargo hax` command was
 /// run inside a terminal. If it was inside a terminal,
-/// [rust_log_style] returns ["always"], which is the usual default
-/// behavior. Otherwise we return ["never"]. When [RUST_LOG_STYLE] is
+/// [`rust_log_style`] returns `"always"`, which is the usual default
+/// behavior. Otherwise we return `"never"`. When [`RUST_LOG_STYLE`] is
 /// set, we just return its value.
 const RUST_LOG_STYLE: &str = "RUST_LOG_STYLE";
 fn rust_log_style() -> String {

engine/default.nix

@@ -41,7 +41,7 @@
     pname = "hax-engine";
     version = "0.0.1";
     duneVersion = "3";
-    src = lib.sourceFilesBySuffices ./. [".ml" ".mli" ".js" "dune" "dune-project" "sh" "rs"];
+    src = lib.sourceFilesBySuffices ./. [".ml" ".mli" ".js" "dune" "dune-project" "sh" "rs" "mld"];
     buildInputs = with ocamlPackages;
       [
         zarith_stubs_js
@@ -87,6 +87,14 @@
     ];
     strictDeps = true;
     passthru = {
+      docs = hax-engine.overrideAttrs (old: {
+        name = "hax-engine-docs";
+        nativeBuildInputs = old.nativeBuildInputs ++ [
+          ocamlPackages.odoc
+        ];
+        buildPhase = ''dune build @doc'';
+        installPhase = "cp -rf _build/default/_doc/_html $out";
+      });
       js = hax-engine.overrideAttrs (old: {
         name = "hax-engine.js";
         nativeBuildInputs = old.nativeBuildInputs ++ [closurecompiler gnused];

engine/doc/dune

@@ -0,0 +1,3 @@
+(documentation
+  (package hax-engine)
+  (mld_files index))

engine/doc/index.mld

@@ -0,0 +1,20 @@
+{0 Hax Engine}
+
+The engine of hax is written in OCaml, and has the following structure:
+{ul {- the {!module-Hax_engine} library (located in `/engine/lib`)}
+    {- the {!module-Native_driver} binary (located in `/engine/bin`)}
+    {- the backends (located in `/engine/backends`):
+       {ul {- {!module-Fstar_backend}}
+           {- {!module-Coq_ast}}
+           {- {!module-Easycrypt_ast}}
+       }
+    }
+    {- utilities and PPXs:
+       {ul {- {!module-Hacspeclib_macro_parser}}
+           {- {!module-Ppx_functor_application}}
+           {- {!module-Ppx_generate_features}}
+           {- {!module-Ppx_inline}}
+        }
+    }
+}
+

frontend/diagnostics/src/lib.rs

@@ -120,7 +120,7 @@ impl<S> std::fmt::Display for Diagnostics<S> {
                 "The bindings {:?} cannot be mutated here: they don't belong to the closure scope, and this is not allowed.",
                 bindings
             ),
-            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported. [lhs = e] is fine only when [lhs] is a combination of local identifiers, field accessors and index accessors."),
+            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported. `lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
             _ => write!(f, "{:?}", self.kind),
         }
     }
@@ -165,7 +165,7 @@ pub enum Kind {
         bindings: Vec<String>,
     } = 6,
 
-    /// Assignation of an arbitrary left-hand side is not supported. [lhs = e] is fine only when [lhs] is a combination of local identifiers, field accessors and index accessors.
+    /// Assignation of an arbitrary left-hand side is not supported. `lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors.
     ArbitraryLHS = 7,
 
     /// A phase explicitely rejected this chunk of code

frontend/exporter/adt-into/src/lib.rs

@@ -256,9 +256,10 @@ fn variant_to_arm(
     }
 }
 
-/// [`AdtInto`] derives a [`SInto`] instance. This helps at
-/// transporting a algebraic data type `A` to another ADT `B` when `A`
-/// and `B` shares a lot of structure.
+/// [`AdtInto`] derives a
+/// [`SInto`](../hax_frontend_exporter/trait.SInto.html)
+/// instance. This helps at transporting a algebraic data type `A` to
+/// another ADT `B` when `A` and `B` shares a lot of structure.
 #[proc_macro_derive(
     AdtInto,
     attributes(

frontend/exporter/src/traits.rs

@@ -312,7 +312,7 @@ pub fn clause_id_of_predicate(predicate: rustc_middle::ty::Predicate) -> u64 {
 /// for `Wrapper` (in this case: `u64 : ToU64`) and resolve it.
 ///
 /// TODO: returns an Option for now, `None` means we hit the indexing
-/// bug (see https://github.com/rust-lang/rust/issues/112242).
+/// bug (see <https://github.com/rust-lang/rust/issues/112242>).
 #[tracing::instrument(level = "trace", skip(s))]
 pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,

frontend/exporter/src/types/mir.rs

@@ -439,7 +439,7 @@ pub enum StatementKind {
 
 #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
 pub struct Place {
-    /// The type of the element on which we apply the projection given by [kind]
+    /// The type of the element on which we apply the projection given by `kind`
     pub ty: Ty,
     pub kind: PlaceKind,
 }