feat(doc): init rustdoc and odoc

cryspen · Nov 15, 2023 · 98cb20d · 98cb20d
1 parent af47d07
commit 98cb20d
Show file tree

Hide file tree

Showing 4 changed files with 61 additions and 2 deletions.
diff --git 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 "<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;
     };
   }
diff --git 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
@@ -0,0 +1,3 @@
+(documentation
+  (package hax-engine)
+  (mld_files index))
diff --git a/engine/doc/index.mld b/engine/doc/index.mld
@@ -0,0 +1,21 @@
+{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}}
+        }
+    }
+}
+
+