chore: Nix: overhaul nix-dev, lift technical restrictions

doc/make/nix.md

@@ -82,10 +82,6 @@ there is no mutable directory incrementally filled by the build that we could po
 Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary.
 However, it will only ever load changes saved to disk, not ones opened in other buffers.
 
-Because of technical limitations, there are currently two further restrictions for files in `src/`:
-* They must be reachable from `src/Lean.lean` to be editable. Note that they have to be so anyway to be included in the full stage compilation, but it might initially be confusing when creating a new file.
-* New imports, even when already compiled, will only be accessible after saving the file.
-
 # Other Fun Stuff to Do with Nix
 
 Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough):

nix/bootstrap.nix

@@ -64,9 +64,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 = [ Init ]; };
-      Lean = build { name = "Lean"; src = ../src; srcDir = "/src"; deps = [ Init Std ]; };
+      Init = build { name = "Init"; src = ../src; deps = []; };
+      Std  = build { name = "Std";  src = ../src; deps = [ Init ]; };
+      Lean = build { name = "Lean"; src = ../src; deps = [ Init Std ]; };
       inherit (Lean) emacs-dev emacs-package;
       mods = Init.mods // Std.mods // Lean.mods;
       lean = stdenv.mkDerivation {

nix/buildLeanPackage.nix

@@ -41,7 +41,7 @@ with builtins; let
     allowSubstitutes = false;
   };
 in
-  { name, src, srcDir ? name, deps ? [ lean.Std ] }: let
+  { name, src, deps ? [ lean.Lean ] }: let
     srcRoot = src;
     allDeps = lib.foldr (dep: allDeps: allDeps // { ${dep.name} = dep; } // dep.allDeps) {} deps;
     fakeDepRoot = runCommandLocal "${name}-dep-root" {} ''
@@ -49,14 +49,17 @@ in
       cd $out
       mkdir ${lib.concatStringsSep " " ([name] ++ attrNames allDeps)}
     '';
+    print-lean-deps = writeShellScriptBin "print-lean-deps" ''
+      export LEAN_PATH=${fakeDepRoot}
+      ${lean-leanDeps}/bin/lean --deps --stdin | ${gnused}/bin/sed "s!$LEAN_PATH/!!;s!/!.!g;s!.olean!!"
+    '';
     # build a file containing the module names of all immediate dependencies of `mod`
     leanDeps = mod: mkDerivation {
       name ="${mod}-deps";
       src = src + ("/" + modToLean mod);
-      buildInputs = [ lean-leanDeps gnused ];
+      buildInputs = [ print-lean-deps ];
       buildCommand = ''
-        export LEAN_PATH=${fakeDepRoot};
-        lean --deps $src | sed "s!$LEAN_PATH/!!;s!/!.!g;s!.olean!!" > $out
+        print-lean-deps < $src > $out
       '';
       preferLocalBuild = true;
       allowSubstitutes = false;
@@ -107,8 +110,12 @@ in
     makeEmacsWrapper = name: lean: writeShellScriptBin name ''
       ${lean-emacs}/bin/emacs --eval "(progn (setq lean4-rootdir \"${lean}\") (require 'lean4-mode))" $@
     '';
+    checkMod = deps: writeShellScriptBin "check-mod" ''
+      LEAN_PATH=${depRoot "check-mod" deps} ${lean}/bin/lean "$@"
+    '';
+    makeCheckModFor = deps: mods: checkMod deps // mapAttrs (_: mod: makeCheckModFor (deps ++ [mod]) mods) mods;
   in rec {
-    inherit name lean deps allDeps;
+    inherit name lean deps allDeps print-lean-deps;
     mods      = buildModAndDeps name (lib.foldr (dep: depMap: depMap // dep.mods) {} (attrValues allDeps));
     modRoot   = depRoot name [ mods.${name} ];
     cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
@@ -124,12 +131,13 @@ in
     '';
     emacs-package = makeEmacsWrapper "emacs-package" lean-package;
 
+    check-mod = makeCheckModFor [] mods;
     lean-dev = substituteAll {
       name = "lean";
       dir = "bin";
       src = ./lean-dev.in;
       isExecutable = true;
-      inherit lean bash nix srcDir;
+      inherit lean bash nix srcRoot;
     };
     emacs-dev = makeEmacsWrapper "emacs-dev" lean-dev;
   }

nix/lean-dev.in

@@ -19,26 +19,30 @@ call() {
 
 json=0
 input=
+inputFile=
 for p in "$@"; do
-    [[ "$p" == --json ]] && json=1
-    [[ "$p" != -* ]] && input="$(realpath "$p")"
+    case "$p" in
+        --json) json=1;;
+        --stdin) input="$(< /dev/stdin)";;
+        -*) ;;
+        *) inputFile="$p";;
+    esac
 done
+if [[ -z "$input" && -f "$inputFile" ]]; then
+    input="$(< "$inputFile")"
+fi
 
-root="$(dirname "${input:-/}")"
+# find package root of input file
+root="$(dirname "${inputFile:-/}")"
 while [[ "$root" != / ]]; do
     [ -f "$root/flake.nix" ] && break
     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//\//.}"
-    call nix develop "$root#mods.\"$input\"" -c lean $@
-fi
+# fall back to current package
+[[ "$root" == / ]] && root="@srcRoot@"
+deps="$(echo -n "$input" | nix run "$root#print-lean-deps" 2> /dev/null)"
+attrPath="check-mod"
+for dep in $deps; do
+    attrPath="$attrPath.\"$dep\""
+done
+echo -n "$input" | call nix run "$root#$attrPath" -- "$@"