feat: Nix: template for custom packages

flake.nix

@@ -38,7 +38,8 @@
         inherit buildLeanPackage;
       };
       buildLeanPackage = callPackage (import ./nix/buildLeanPackage.nix) {
-        inherit (lean) stdenv lean leanc;
+        inherit (lean) stdenv leanc;
+        lean = lean.stage1;
         inherit lean-emacs;
         nix = nix-pinned;
       };
@@ -107,5 +108,13 @@
       defaultPackage = packages.lean;
 
       checks.lean = packages.test;
-    });
+
+    }) // rec {
+      templates.pkg = {
+        path = ./nix/templates/pkg;
+        description = "A custom Lean package";
+      };
+
+      defaultTemplate = templates.pkg;
+    };
 }

nix/bootstrap.nix

@@ -62,9 +62,9 @@ rec {
         leanFlags = [ "-Dinterpreter.prefer_native=false" ];
       };
     in (all: all // all.lean) rec {
-      Init = build { name = "Init"; src = ../src; srcDir = "/src"; deps = {}; };
-      Std  = build { name = "Std";  src = ../src; srcDir = "/src"; deps = { inherit Init; }; };
-      Lean = build { name = "Lean"; src = ../src; srcDir = "/src"; deps = { inherit Init Std; }; };
+      Init = build { name = "Init"; src = ../src; srcDir = "/src"; deps = []; };
+      Std  = build { name = "Std";  src = ../src; srcDir = "/src"; deps = [ Init ]; };
+      Lean = build { name = "Lean"; src = ../src; srcDir = "/src"; deps = [ Init Std ]; };
       inherit (Lean) emacs-dev emacs-package;
       mods = Init.mods // Std.mods // Lean.mods;
       lean = stdenv.mkDerivation {

nix/buildLeanPackage.nix

@@ -1,5 +1,5 @@
 { debug ? false, leanFlags ? [], leancFlags ? [],
-  lean, leanc ? lean, lean-leanDeps ? lean, lean-final ? lean,
+  lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
   stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, nix, substituteAll, symlinkJoin, linkFarmFromDrvs }:
 with builtins; let
   # "Init.Core" ~> "Init/Core"
@@ -40,12 +40,12 @@ with builtins; let
     allowSubstitutes = false;
   };
 in
-  { name, src, srcDir ? "", deps }: let
+  { name, src, srcDir ? name, deps ? [ lean.Lean ] }: let
     srcRoot = src;
     fakeDepRoot = runCommandLocal "${name}-dep-root" {} ''
       mkdir $out
       cd $out
-      mkdir ${lib.concatStringsSep " " ([name] ++ attrNames deps)}
+      mkdir ${lib.concatStringsSep " " ([name] ++ map (dep: dep.name) deps)}
     '';
     # build a file containing the module names of all immediate dependencies of `mod`
     leanDeps = mod: mkDerivation {
@@ -106,7 +106,8 @@ in
       ${lean-emacs}/bin/emacs --eval "(progn (setq lean4-rootdir \"${lean}\") (require 'lean4-mode))" $@
     '';
   in rec {
-    mods      = buildModAndDeps name (lib.foldr (dep: depMap: depMap // dep.mods) {} (attrValues deps));
+    inherit name lean;
+    mods      = buildModAndDeps name (lib.foldr (dep: depMap: depMap // dep.mods) {} deps);
     modRoot   = depRoot name [ mods.${name} ];
     cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (builtins.attrValues mods); };
     objects   = mapAttrs compileMod mods;

nix/lean-dev.in

@@ -30,10 +30,13 @@ while [[ "$root" != / ]]; do
     root="$(realpath "$root/..")"
 done
 if [[ "$root" == / ]]; then
+    # if we're outside of any project, just call Lean without any packages
     call @lean@/bin/lean $@
 elif [[ "$input" != "$root@srcDir@/"* ]]; then
+    # otherwise, if we're inside the package but not its source directory, call Lean with the full package available
     call nix run "$root#lean-package" -- $@
 else
+    # otherwise call Lean with the file's dependencies available
     input="$(realpath --relative-to="$root@srcDir@" "$input")"
     input="${input%.lean}"
     input="${input//\//.}"

nix/templates/pkg/MyPackage.lean

@@ -0,0 +1 @@
+#eval "Hello, world!"

nix/templates/pkg/flake.nix

@@ -0,0 +1,18 @@
+{
+  description = "My Lean package";
+
+  inputs.lean.url = github:leanprover/lean4;
+  inputs.flake-utils.url = github:numtide/flake-utils;
+
+  outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
+    let leanPkgs = lean.packages.${system}; in rec {
+      packages = {
+        inherit (leanPkgs) lean;
+      } // leanPkgs.buildLeanPackage {
+        name = "MyPackage";  # must match the name of the top-level .lean file
+        src = ./.;
+      };
+
+      defaultPackage = packages.modRoot;
+    });
+}