diff --git a/.github/workflows/gh_pages.yml b/.github/workflows/gh_pages.yml new file mode 100644 index 000000000..bdce044da --- /dev/null +++ b/.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 + 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 diff --git a/cli/default.nix b/cli/default.nix index e28dd1a98..b03b15cd4 100644 --- a/cli/default.nix +++ b/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 "" + echo "

Hax docs

" + echo "

Hax is written both in Rust and OCaml. Documentation for each is available below:

" + echo "" + ) > $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; }; } diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index 80f6ca674..1ddce8a29 100644 --- a/cli/options/src/lib.rs +++ b/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 can be either: + /// The value of `` 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. /// - /// - [] or [file:]: outputs the different AST as JSON - /// to . can be either [-] or a path. + /// - `` or `file:`: outputs the different AST as JSON + /// to ``. `` can be either [-] or a path. #[arg(short, long = "debug-engine")] pub debug_engine: Option, @@ -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 [/proofs//extraction], where - /// is the translated cargo package name and the - /// name of the backend. + /// under the directory `/proofs//extraction`, where + /// `` is the translated cargo package name and `` + /// 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, /// 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, #[command(subcommand)] pub command: Option, - /// [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 ;]). + /// options like `-C -p ;`). #[arg(long = "deps")] pub deps: bool, } diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index 0cb5e6200..3ad2c7511 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/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 { 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 { } /// 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 { diff --git a/engine/default.nix b/engine/default.nix index 9bb289c39..3c3c82aaa 100644 --- a/engine/default.nix +++ b/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]; diff --git a/engine/doc/dune b/engine/doc/dune new file mode 100644 index 000000000..b86828151 --- /dev/null +++ b/engine/doc/dune @@ -0,0 +1,3 @@ +(documentation + (package hax-engine) + (mld_files index)) diff --git a/engine/doc/index.mld b/engine/doc/index.mld new file mode 100644 index 000000000..1ba5ca3a7 --- /dev/null +++ b/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}} + } + } +} + diff --git a/frontend/diagnostics/src/lib.rs b/frontend/diagnostics/src/lib.rs index f64d6ba51..43e2967ce 100644 --- a/frontend/diagnostics/src/lib.rs +++ b/frontend/diagnostics/src/lib.rs @@ -120,7 +120,7 @@ impl std::fmt::Display for Diagnostics { "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, } = 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 diff --git a/frontend/exporter/adt-into/src/lib.rs b/frontend/exporter/adt-into/src/lib.rs index c46a37644..28628646f 100644 --- a/frontend/exporter/adt-into/src/lib.rs +++ b/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( diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index b12fc8d27..aced51bcb 100644 --- a/frontend/exporter/src/traits.rs +++ b/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 ). #[tracing::instrument(level = "trace", skip(s))] pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>( s: &S, diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 355ca5c59..43013e1b3 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/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, }