feat: Nix: use HEAD as stage0

2026-03-17 18:34:06 +00:00 · 2020-12-16 15:18:47 +01:00
parent 4812f2aa64
commit 4e3025fe81
7 changed files with 165 additions and 111 deletions
--- a/doc/make/nix.md
+++ b/doc/make/nix.md
@@ -101,6 +101,20 @@ Not sure what you just broke? Run Lean from (e.g.) the previous commit on a file
 nix run .\?rev=$(git rev-parse @^) scratch.lean
 ```

+Work on two adjacent stages at the same time without the need for repeatedly updating and reverting `stage0/`:
+```bash
+# open an editor that will use only committed changes (so first commit them when changing files)
+nix run .#HEAD-as-stage1.emacs-dev&
+# open a second editor that will use those commited changes as stage 0
+# (so don't commit changes done here until you are done and ran a final `update-stage0-commit`)
+nix run .#HEAD-as-stage0.emacs-dev&
+```
+To run `nix build` on the second stage outside of the second editor, use
+```bash
+nix build .#stage0-from-input
+```
+This setup will inadvertently change your `flake.lock` file, which you can revert when you are done.
+
 ...more surely to come...

 # Debugging
--- a/flake.lock
+++ b/flake.lock
@@ -15,6 +15,21 @@
        "type": "github"
      }
    },
+    "lean-stage0": {
+      "locked": {
+        "lastModified": 0,
+        "narHash": "sha256-3K/43lSW4WIHNG+HHVKCD1odS63mHuaQ4ueHyTIkcls=",
+        "owner": "leanprover",
+        "repo": "lean4",
+        "rev": "0000000000000000000000000000000000000000",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "lean4",
+        "type": "github"
+      }
+    },
    "lowdown-src": {
      "flake": false,
      "locked": {
@@ -100,6 +115,7 @@
    "root": {
      "inputs": {
        "flake-utils": "flake-utils",
+        "lean-stage0": "lean-stage0",
        "mdBook": "mdBook",
        "nix": "nix",
        "nixpkgs": "nixpkgs_2",
--- a/flake.nix
+++ b/flake.nix
@@ -12,8 +12,17 @@
    url = github:leanprover/mdBook;
    flake = false;
  };
+  # used *only* by `stage0-from-input` below
+  inputs.lean-stage0 = {
+    url = github:leanprover/lean4;
+    inputs.nixpkgs.follows = "nixpkgs";
+    inputs.flake-utils.follows = "flake-utils";
+    inputs.temci.follows = "temci";
+    inputs.nix.follows = "nix";
+    inputs.mdBook.follows = "mdBook";
+  };

-  outputs = { self, nixpkgs, flake-utils, temci, nix, mdBook }: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, flake-utils, temci, nix, mdBook, lean-stage0 }: flake-utils.lib.eachDefaultSystem (system:
    let
      packages = nixpkgs.legacyPackages.${system}.callPackage (./nix/packages.nix) { inherit nix temci mdBook; };
    in {
@@ -30,6 +39,10 @@
          }).stage1;
        };
        tsandebug = tsan.override { debug = true; };
+        stage0-from-input = packages.override {
+          stage0 = lean-stage0.packages.${system}.lean;
+        };
+        inherit self;
      };

      defaultPackage = packages.lean;
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -39,7 +39,7 @@ rec {
      mv lib/ $out/
    '';
  };
-  stage0 = buildCMake {
+  stage0 = args.stage0 or (buildCMake {
    name = "lean-stage0";
    src = ../stage0/src;
    debug = false;
@@ -51,18 +51,19 @@ rec {
      mkdir -p $out/bin
      mv bin/lean $out/bin/
    '';
-  };
+  });
  stage = { stage, prevStage, self }:
    let
      desc = "stage${toString stage}";
-      build = buildLeanPackage.override {
+      build = args: buildLeanPackage.override {
        lean = prevStage;
        # use same stage for retrieving dependencies
        lean-leanDeps = stage0;
        lean-final = self;
+      } (args // {
        inherit debug;
        leanFlags = [ "-Dinterpreter.prefer_native=false" ];
-      };
+      });
    in (all: all // all.lean) rec {
      Init = build { name = "Init"; src = ../src; deps = []; };
      Std  = build { name = "Std";  src = ../src; deps = [ Init ]; };
@@ -116,7 +117,7 @@ rec {
        git commit -m "chore: update stage0"
      '';
    };
-  stage1 = stage { stage = 1; prevStage = args.stage0 or stage0; self = stage1; };
+  stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
  stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
  stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
 }
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -1,7 +1,9 @@
-{ debug ? false, leanFlags ? [], leancFlags ? [],
-  lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
+{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, nix, substituteAll, symlinkJoin, linkFarmFromDrvs,
  ... }:
+let lean-final' = lean-final; in
+{ name, src, deps ? [ lean.Lean ],
+  debug ? false, leanFlags ? [], leancFlags ? [], srcCheckTarget ? "$root#stage0check-mod", srcCheckArgs ? "(\${args[*]})", lean-final ? lean-final' }:
 with builtins; let
  # "Init.Core" ~> "Init/Core"
  modToPath = mod: replaceStrings ["."] ["/"] mod;
@@ -40,104 +42,102 @@ with builtins; let
    preferLocalBuild = true;
    allowSubstitutes = false;
  };
-in
-  { 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" {} ''
-      mkdir $out
-      cd $out
-      mkdir ${lib.concatStringsSep " " ([name] ++ attrNames allDeps)}
+  srcRoot = src;
+  allDeps = lib.foldr (dep: allDeps: allDeps // { ${dep.name} = dep; } // dep.allDeps) {} deps;
+  fakeDepRoot = runCommandLocal "${name}-dep-root" {} ''
+    mkdir $out
+    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 = [ print-lean-deps ];
+    buildCommand = ''
+      print-lean-deps < $src > $out
    '';
-    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!!"
+    preferLocalBuild = true;
+    allowSubstitutes = false;
+  };
+  # build module (.olean and .c) given derivations of all (transitive) dependencies
+  buildMod = mod: deps: mkDerivation rec {
+    name = "${mod}";
+    LEAN_PATH = depRoot mod deps;
+    relpath = modToPath mod;
+    buildInputs = [ lean ];
+    leanPath = relpath + ".lean";
+    src = srcRoot + ("/" + leanPath);
+    outputs = [ "out" "c" ];
+    oleanPath = relpath + ".olean";
+    cPath = relpath + ".c";
+    inherit leanFlags;
+    buildCommand = ''
+      mkdir -p $(dirname $relpath) $out/$(dirname $relpath) $c/$(dirname $relpath)
+      cp $src $leanPath
+      lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags
    '';
-    # build a file containing the module names of all immediate dependencies of `mod`
-    leanDeps = mod: mkDerivation {
-      name ="${mod}-deps";
-      src = src + ("/" + modToLean mod);
-      buildInputs = [ print-lean-deps ];
-      buildCommand = ''
-        print-lean-deps < $src > $out
-      '';
-      preferLocalBuild = true;
-      allowSubstitutes = false;
-    };
-    # build module (.olean and .c) given derivations of all (transitive) dependencies
-    buildMod = mod: deps: mkDerivation rec {
-      name = "${mod}";
-      LEAN_PATH = depRoot mod deps;
-      relpath = modToPath mod;
-      buildInputs = [ lean ];
-      leanPath = relpath + ".lean";
-      src = srcRoot + ("/" + leanPath);
-      outputs = [ "out" "c" ];
-      oleanPath = relpath + ".olean";
-      cPath = relpath + ".c";
-      inherit leanFlags;
-      buildCommand = ''
-        mkdir -p $(dirname $relpath) $out/$(dirname $relpath) $c/$(dirname $relpath)
-        cp $src $leanPath
-        lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags
-      '';
-    } // {
-      inherit deps;
-    };
-    compileMod = mod: drv: mkDerivation {
-      name = "${mod}-cc";
-      buildInputs = [ leanc ];
-      hardeningDisable = [ "all" ];
-      oPath = drv.relpath + ".o";
-      inherit leancFlags;
-      buildCommand = ''
-        mkdir -p $out/$(dirname ${drv.relpath})
-        # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
-        ln -s ${drv.c}/${drv.cPath} src.c
-        leanc -c -o $out/$oPath src.c $leancFlags ${if debug then "-g" else "-O3 -DNDEBUG"}
-      '';
-    };
-    singleton = name: value: listToAttrs [ { inherit name value; } ];
-    # Recursively build `mod` and its dependencies. `modMap` maps module names to
-    # `{ deps, drv }` pairs of a derivation and its transitive dependencies (as a nested
-    # mapping from module names to derivations). It is passed linearly through the
-    # recursion to memoize common dependencies.
-    buildModAndDeps = mod: modMap: if modMap ? ${mod} then modMap else
-      let
-        deps = filter (p: p != "") (lib.splitString "\n" (readFile (leanDeps mod)));
-        modMap' = lib.foldr buildModAndDeps modMap deps;
-      in modMap' // { ${mod} = buildMod mod (map (dep: modMap'.${dep}) deps); };
-    makeEmacsWrapper = name: lean: writeShellScriptBin name ''
-      ${lean-emacs}/bin/emacs --eval "(progn (setq lean4-rootdir \"${lean}\") (require 'lean4-mode))" $@
-    '';
-    checkMod = lean: deps: writeShellScriptBin "check-mod" ''
-      LEAN_PATH=${depRoot "check-mod" deps} ${lean}/bin/lean "$@"
-    '';
-    makeCheckModFor = lean: deps: mods: checkMod lean deps // mapAttrs (_: mod: makeCheckModFor lean (deps ++ [mod]) mods) mods;
-  in rec {
-    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); };
-    objects   = mapAttrs compileMod mods;
-    oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
-    staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
-      mkdir $out
-      ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))}
+  } // {
+    inherit deps;
+  };
+  compileMod = mod: drv: mkDerivation {
+    name = "${mod}-cc";
+    buildInputs = [ leanc ];
+    hardeningDisable = [ "all" ];
+    oPath = drv.relpath + ".o";
+    inherit leancFlags;
+    buildCommand = ''
+      mkdir -p $out/$(dirname ${drv.relpath})
+      # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
+      ln -s ${drv.c}/${drv.cPath} src.c
+      leanc -c -o $out/$oPath src.c $leancFlags ${if debug then "-g" else "-O3 -DNDEBUG"}
    '';
+  };
+  singleton = name: value: listToAttrs [ { inherit name value; } ];
+  # Recursively build `mod` and its dependencies. `modMap` maps module names to
+  # `{ deps, drv }` pairs of a derivation and its transitive dependencies (as a nested
+  # mapping from module names to derivations). It is passed linearly through the
+  # recursion to memoize common dependencies.
+  buildModAndDeps = mod: modMap: if modMap ? ${mod} then modMap else
+    let
+      deps = filter (p: p != "") (lib.splitString "\n" (readFile (leanDeps mod)));
+      modMap' = lib.foldr buildModAndDeps modMap deps;
+    in modMap' // { ${mod} = buildMod mod (map (dep: modMap'.${dep}) deps); };
+  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-final}/bin/lean "$@"
+  '';
+  makeCheckModFor = deps: mods: checkMod deps // mapAttrs (_: mod: makeCheckModFor (deps ++ [mod]) mods) mods;
+in rec {
+  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); };
+  objects   = mapAttrs compileMod mods;
+  oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
+  staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
+    mkdir $out
+    ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))}
+  '';

-    lean-package = writeShellScriptBin "lean" ''
-      LEAN_PATH=${modRoot}:$LEAN_PATH ${lean-final}/bin/lean $@
-    '';
-    emacs-package = makeEmacsWrapper "emacs-package" lean-package;
+  lean-package = writeShellScriptBin "lean" ''
+    LEAN_PATH=${modRoot}:$LEAN_PATH ${lean-final}/bin/lean $@
+  '';
+  emacs-package = makeEmacsWrapper "emacs-package" lean-package;

-    check-mod = lib.makeOverridable (lean: makeCheckModFor lean [] mods) lean-final;
-    lean-dev = substituteAll {
-      name = "lean";
-      dir = "bin";
-      src = ./lean-dev.in;
-      isExecutable = true;
-      inherit lean bash nix srcRoot;
-    };
-    emacs-dev = makeEmacsWrapper "emacs-dev" lean-dev;
-  }
+  check-mod = makeCheckModFor [] mods;
+  lean-dev = substituteAll {
+    name = "lean";
+    dir = "bin";
+    src = ./lean-dev.in;
+    isExecutable = true;
+    inherit lean bash nix srcRoot srcCheckTarget srcCheckArgs;
+  };
+  emacs-dev = makeEmacsWrapper "emacs-dev" lean-dev;
+}
--- a/nix/lean-dev.in
+++ b/nix/lean-dev.in
@@ -41,10 +41,11 @@ done
 # fall back to current package
 [[ "$root" == / ]] && root="@srcRoot@"
 deps="$(echo -n "$input" | nix run "$root#print-lean-deps" 2> /dev/null)"
-attrPath="check-mod"
+target="$root#check-mod"
+args=(-- "$@")
 # HACK: use stage 0 instead of 1 inside Lean's own `src/`
-[[ -d "$root/src/Lean" && "$(realpath "$inputFile")" == "$root/src/"* ]] && attrPath="stage0check-mod"
+[[ -d "$root/src/Lean" && "$(realpath "$inputFile")" == "$root/src/"* ]] && target="@srcCheckTarget@" && args=@srcCheckArgs@
 for dep in $deps; do
-    attrPath="$attrPath.\"$dep\""
+    target="$target.\"$dep\""
 done
-echo -n "$input" | call nix run "$root#$attrPath" -- "$@"
+echo -n "$input" | call nix run "$target" ${args[*]}
--- a/nix/packages.nix
+++ b/nix/packages.nix
@@ -22,12 +22,19 @@ let
    stdenv = overrideCC llvmPackages.stdenv cc;
    inherit buildLeanPackage;
  });
-  buildLeanPackage = callPackage (import ./buildLeanPackage.nix) (args // {
+  makeOverridableLeanPackage = f:
+    let newF = origArgs: f origArgs // {
+      overrideArgs = newArgs: makeOverridableLeanPackage f (origArgs // newArgs);
+    };
+    in lib.setFunctionArgs newF (lib.getFunctionArgs f) // {
+      override = args: makeOverridableLeanPackage (f.override args);
+    };
+  buildLeanPackage = makeOverridableLeanPackage (callPackage (import ./buildLeanPackage.nix) (args // {
    inherit (lean) stdenv leanc;
    lean = lean.stage1;
    inherit lean-emacs;
    nix = nix-pinned;
-  });
+  }));
  lean4-mode = emacsPackages.melpaBuild {
    pname = "lean4-mode";
    version = "1";
@@ -75,7 +82,9 @@ let
 in {
  inherit cc lean4-mode buildLeanPackage llvmPackages;
  lean = lean.stage1;
-  stage0check-mod = lean.stage1.Lean.check-mod.override lean.stage0;
+  stage0check-mod = (lean.stage1.Lean.overrideArgs { lean-final = lean.stage0; }).check-mod;
+  HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcCheckTarget = "$root#stage0-from-input.stage0check-mod"; srcCheckArgs = "(--override-input lean-stage0 $root\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
+  HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcCheckTarget = "$root\?rev=$(git rev-parse HEAD)#stage0check-mod"; });
  temci = (import temci {}).override { doCheck = false; };
  nix = nix-pinned;
  nixpkgs = pkgs;