diff --git a/doc/make/nix.md b/doc/make/nix.md index 8611580351..2909607528 100644 --- 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 diff --git a/flake.lock b/flake.lock index f844c63ad1..3dd1edd48a 100644 --- 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", diff --git a/flake.nix b/flake.nix index 454090b891..8256573e21 100644 --- 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; diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 6f9f53cc36..d585ee1073 100644 --- 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; }; } diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index bc93ea1e53..9989750ee2 100644 --- 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; +} diff --git a/nix/lean-dev.in b/nix/lean-dev.in index be8e76b338..5defccfe50 100644 --- 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[*]} diff --git a/nix/packages.nix b/nix/packages.nix index ee88f08e32..96d5c9c56e 100644 --- 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;