From 2978bcca29bf1d422b3d43a7f2219d8dd644e5c4 Mon Sep 17 00:00:00 2001
From: Ryan Lahfa <ryan.lahfa@inria.fr>
Date: Mon, 26 Aug 2024 14:19:16 +0200
Subject: [PATCH] chore(docs/user): vendor various lean-nix code

As upstream is moving to a non-user-facing Nix library,
we are vendoring some of the useful code such as `buildLeanPackage`.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
---
 docs/user/flake.nix       | 33 +++------------------------------
 docs/user/nix/default.nix | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+), 30 deletions(-)
 create mode 100644 docs/user/nix/default.nix

diff --git a/docs/user/flake.nix b/docs/user/flake.nix
index a9431a594..4563f66bd 100644
--- a/docs/user/flake.nix
+++ b/docs/user/flake.nix
@@ -21,6 +21,7 @@
     with inputs.lean.packages.${system}; with nixpkgs;
     let
       doc-src = ./.; # lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
+      leanLib = callPackage ./nix { };
     in {
     packages = rec {
       lean-mdbook = mdbook.overrideAttrs (drv: rec {
@@ -87,36 +88,8 @@
       aeneas-base = 
       let
         manifest = builtins.fromJSON (builtins.readFile ./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 {};
+        fetchFromLakeManifest = leanLib.fetchFromLakeManifest manifest;
+        inherit (leanLib) addFakeFiles;
 
         batteries = buildLeanPackage {
           name = "Batteries";
diff --git a/docs/user/nix/default.nix b/docs/user/nix/default.nix
new file mode 100644
index 000000000..b90dda26b
--- /dev/null
+++ b/docs/user/nix/default.nix
@@ -0,0 +1,37 @@
+{ emptyFile, runCommandCC, lib, callPackage, ... }: {
+  /* Given a parsed Lake manifest in Nix,
+    this will fetch a specific Lake dependency of the manifest.
+
+    This currently only supports Git inputs.
+  */
+  fetchFromLakeManifest = manifest: { 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 = 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
+      '' + lib.concatMapStringsSep "\n" (p : ''
+        install -D -m 644 ${emptyFile} $out/${p}
+      '') paths);
+    }
+    else {};
+}