chore(docs/user): package Mathlib4 in Nix

Well, this is required… Following Loogle's steps, we add fake files for ProofWidgets4 and we can produce an .olean from Aeneas' base library without Lake involvement! Free parallelization and caching :). TODOs are to improve the hash handling when lake-manifest.json bumps, but this requires extending Lake to produce the NAR hash serializations. Signed-off-by: Ryan Lahfa <[email protected]>
AeneasVerif · Aug 20, 2024 · 746b6d9 · 746b6d9
1 parent be5fd85
commit 746b6d9
Show file tree

Hide file tree

Showing 6 changed files with 210 additions and 6 deletions.
diff --git a/.gitignore b/.gitignore
@@ -69,6 +69,9 @@ tests/fstar/misc/obj/
 *.uo
 *Theory.sml
 
+# Lean
+.lake
+
 # Misc
 /fstar-tests
 *~

diff --git a/docs/user/flake.lock b/docs/user/flake.lock
diff --git a/docs/user/flake.nix b/docs/user/flake.nix
@@ -2,7 +2,7 @@
 {
   description = "Aeneas documentation";
 
-  inputs.lean.url = "github:leanprover/lean4";
+  inputs.lean.url = "github:leanprover/lean4/v4.10.0";
   inputs.flake-utils.follows = "lean/flake-utils";
   inputs.mdBook = {
     url = "github:leanprover/mdBook";
@@ -40,6 +40,7 @@
           mkdir $out
           # necessary for `additional-css`...?
           cp -vr --no-preserve=mode $src/* .
+          cp -vr --no-preserve=mode ${inked}/* .
           mdbook build -d $out
         '';
       };
@@ -88,7 +89,7 @@
           dir=$(dirname $relpath)
           mkdir -p $dir out/$dir
           if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi
-          alectryon --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md
+          alectryon --lake $src/lakefile.lean --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md
         '';
       });
 
@@ -97,14 +98,123 @@
         paths = map renderLeanMod (lib.attrValues pkg.mods);
       };
 
+      aeneas-base = 
+      let
+        manifest = builtins.fromJSON (builtins.readFile ../../backends/lean/lake-manifest.json);
+        fetchFromLakeManifest = { name, hash, ... }:
+        let 
+          dep = lib.findFirst (pkg: pkg.name == name) null manifest.packages;
+        in 
+        assert dep != null;
+        assert dep.type == "git"; fetchGit {
+          inherit (dep) url rev;
+          narHash = hash;
+        } // (if dep.inputRev != null then { ref = dep.inputRev; } else {});
+
+        # Inspired from Loogle scaffolding.
+        # addFakeFile can plug into buildLeanPackage’s overrideBuildModAttrs
+        # it takes a lean module name and a filename, and makes that file available
+        # (as an empty file) in the build tree, e.g. for include_str.
+        addFakeFiles = m: self: super:
+          if m ? ${super.name}
+          then let
+            paths = m.${super.name};
+          in {
+            src = pkgs.runCommandCC "${super.name}-patched" {
+              inherit (super) leanPath src relpath;
+            } (''
+              dir=$(dirname $relpath)
+              mkdir -p $out/$dir
+              if [ -d $src ]; then cp -r $src/. $out/$dir/; else cp $src $out/$leanPath; fi
+            '' + pkgs.lib.concatMapStringsSep "\n" (p : ''
+              install -D -m 644 ${pkgs.emptyFile} $out/${p}
+            '') paths);
+          }
+          else {};
+
+        batteries = buildLeanPackage {
+          name = "Batteries";
+          src = fetchFromLakeManifest {
+            name = "batteries";
+            hash = "sha256-JbOOKsUiYedNj3oiCNfwgkWyEIXsb1bAUm3uSEWsWPs=";
+          };
+        };
+        qq = buildLeanPackage {
+          name = "Qq";
+          src = fetchFromLakeManifest {
+            name = "Qq";
+            hash = "sha256-//sZE32XzebePy81HEwNhIH8YW8iHgk+O8A0y/qNJrg=";
+          };
+        };
+        aesop = buildLeanPackage {
+          name = "Aesop";
+          deps = [ batteries ];
+          src = fetchFromLakeManifest {
+            name = "aesop";
+            hash = "sha256-LzooSD6NaSQyqKkBcxbSbjIZHrnDBx/lp/s4UdWeHpU=";
+          };
+        };
+        import-graph = buildLeanPackage {
+          name = "ImportGraph";
+          deps = [ batteries ];
+          src = fetchFromLakeManifest {
+            name = "importGraph";
+            hash = "sha256-3bWWnklUHuY/dA1Y3SK78SSDE+J8syEsMPJ67LnRI3M=";
+          };
+        };
+        proof-widgets = buildLeanPackage {
+          name = "ProofWidgets";
+          deps = [ batteries ];
+          src = fetchFromLakeManifest {
+            name = "proofwidgets";
+            hash = "sha256-6PzWhCNxxcuh0vEV0JhV0G30NVkYGEDup1j3KvG2VzA=";
+          };
+
+          overrideBuildModAttrs = addFakeFiles {
+            "ProofWidgets.Compat" = [ ".lake/build/js/compat.js" ];
+            "ProofWidgets.Component.Basic" = [ ".lake/build/js/interactiveExpr.js" ];
+            "ProofWidgets.Component.GoalTypePanel" = [ ".lake/build/js/goalTypePanel.js" ];
+            "ProofWidgets.Component.Recharts" = [ ".lake/build/js/recharts.js" ];
+            "ProofWidgets.Component.PenroseDiagram" = [ ".lake/build/js/penroseDisplay.js" ];
+            "ProofWidgets.Component.Panel.SelectionPanel" = [ ".lake/build/js/presentSelection.js" ];
+            "ProofWidgets.Component.Panel.GoalTypePanel" = [ ".lake/build/js/goalTypePanel.js" ];
+            "ProofWidgets.Component.MakeEditLink" = [ ".lake/build/js/makeEditLink.js" ];
+            "ProofWidgets.Component.OfRpcMethod" = [ ".lake/build/js/ofRpcMethod.js" ];
+            "ProofWidgets.Component.FilterDetails" = [ ".lake/build/js/filterDetails.js" ];
+            "ProofWidgets.Component.HtmlDisplay" =
+              [ ".lake/build/js/htmlDisplay.js" ".lake/build/js/htmlDisplayPanel.js"];
+              "ProofWidgets.Presentation.Expr" = [ ".lake/build/js/exprPresentation.js" ];
+          };
+        };
+        mathlib = buildLeanPackage {
+          deps = [ qq aesop batteries import-graph proof-widgets ];
+          name = "Mathlib";
+          src = fetchFromLakeManifest {
+            name = "mathlib";
+            hash = "sha256-gJYmaNDVus3vgUE3aNQfyMCcQJxw/lq5aYtLjs4OI7I=";
+          };
+        };
+      in
+      buildLeanPackage {
+        name = "Base";
+        deps = [ mathlib ];
+        src = ../../backends/lean;
+      };
+
       literate = buildLeanPackage {
         name = "literate";
+        deps = [ aeneas-base ];
         src = ./.;
-        roots = [ ];
       };
       inked = renderPackage literate;
       doc = book;
     };
     defaultPackage = self.packages.${system}.doc;
+    devShells.default = mkShell {
+      packages = [
+        self.packages.${system}.alectryon
+        self.packages.${system}.leanInk
+      ];
+    };
   });
 }
diff --git a/docs/user/lake-manifest.json b/docs/user/lake-manifest.json
@@ -0,0 +1,82 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.39",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e242f1edcacf917f40fae9b81f57f4bd0a4e45ac",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "base",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../../backends/lean",
+   "configFile": "lakefile.lean"}],
+ "name": "Manual",
+ "lakeDir": ".lake"}
diff --git a/docs/user/lakefile.lean b/docs/user/lakefile.lean
@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+require base from "../../backends/lean"
+
+package «Manual» where
+  -- add package configuration options here
diff --git a/docs/user/lean-toolchain b/docs/user/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.10.0-rc2