diff --git a/flake.nix b/flake.nix index 39535119a3..2d32b33a16 100644 --- a/flake.nix +++ b/flake.nix @@ -3,35 +3,50 @@ inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable; - outputs = { self, nixpkgs }: { - - packages.x86_64-linux.lean = - with import nixpkgs { system = "x86_64-linux"; }; - let - cc = ccacheWrapper.override rec { - cc = llvmPackages_10.clang.override { - # linker go brrr - bintools = llvmPackages_10.lldClang.bintools; - }; - extraConfig = '' -export CCACHE_DIR=/var/cache/ccache -export CCACHE_UMASK=007 -export CCACHE_BASE_DIR=$NIX_BUILD_TOP -[ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@" - ''; + outputs = { self, nixpkgs }: + with import nixpkgs { system = "x86_64-linux"; }; + let + cc = ccacheWrapper.override rec { + cc = llvmPackages_10.clang.override { + # linker go brrr + bintools = llvmPackages_10.lldClang.bintools; }; - lean = callPackage (import ./nix/bootstrap.nix) { - stdenv = overrideCC stdenv cc; - inherit buildLeanPackage; - }; - buildLeanPackage = callPackage (import ./nix/buildLeanPackage.nix) { - inherit (lean) stdenv lean leanc; - }; - in lean.lean // lean // { inherit buildLeanPackage; }; + extraConfig = '' + export CCACHE_DIR=/var/cache/ccache + export CCACHE_UMASK=007 + export CCACHE_BASE_DIR=$NIX_BUILD_TOP + [ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@" + ''; + }; + lean = callPackage (import ./nix/bootstrap.nix) { + stdenv = overrideCC stdenv cc; + inherit buildLeanPackage; + }; + buildLeanPackage = callPackage (import ./nix/buildLeanPackage.nix) { + inherit (lean) stdenv lean leanc; + inherit lean-emacs; + }; + lean4-mode = emacsPackages.melpaBuild { + pname = "lean4-mode"; + version = "1"; + src = ./lean4-mode; + packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash dash-functional f flycheck s ]; + recipe = pkgs.writeText "recipe" '' + (lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el")) + ''; + fileSpecs = [ "*.el" ]; + }; + lean-emacs = emacsWithPackages (epkgs: + # can't use `epkgs`??? + with emacsPackages.melpaPackages; [ dash dash-functional f flycheck s ] ++ [ lean4-mode ]); + in { + packages.x86_64-linux = { + inherit (lean.stage1.Lean) mods leanInteractive emacs; + lean = lean.stage1 // lean // { inherit buildLeanPackage; }; + }; defaultPackage.x86_64-linux = self.packages.x86_64-linux.lean; checks.x86_64-linux.lean = self.packages.x86_64-linux.lean.test; - }; } diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index a2bc9d65c9..22b007b384 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -47,9 +47,12 @@ rec { desc = "stage${toString stage}"; build = buildLeanPackage.override { lean = prevStage; }; in (all: all // all.lean) rec { - Init = build { name = "Init"; src = ../src; deps = {}; }; - Std = build { name = "Std"; src = ../src; deps = { inherit Init; }; }; - Lean = build { name = "Lean"; src = ../src; deps = { inherit Init Std; }; }; + 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; }; }; + stdlib = { + mods = Init.mods // Std.mods // Lean.mods; + }; lean = stdenv.mkDerivation { name = "lean-${desc}"; buildCommand = '' @@ -79,5 +82,4 @@ rec { stage1 = stage { stage = 1; prevStage = stage0; }; stage2 = stage { stage = 2; prevStage = stage1; }; stage3 = stage { stage = 3; prevStage = stage2; }; - lean = stage1; } diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index 26d6a53c21..e7b3376c36 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -1,4 +1,4 @@ -{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean }: +{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, writeScriptBin, bash, lean-emacs }: with builtins; let # "Init.Core" ~> "Init/Core.lean" modToLean = mod: replaceStrings ["."] ["/"] mod + ".lean"; @@ -35,8 +35,7 @@ with builtins; let ''; }; in - { name, src, deps }: - let + { name, src, srcDir ? "", deps }: let fakeDepRoot = runCommandLocal "${name}-dep-root" {} '' mkdir $out cd $out @@ -92,12 +91,53 @@ in 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); }; - in rec { - mods = buildModAndDeps name (lib.foldr (dep: depMap: depMap // dep.mods) {} (attrValues deps)); - modRoot = depRoot name [ mods.${name} ]; - objects = mapAttrs compileMod mods; - staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } '' - mkdir $out - ar rcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/out.o") (attrValues objects))} - ''; + in rec { + mods = buildModAndDeps name (lib.foldr (dep: depMap: depMap // dep.mods) {} (attrValues deps)); + modRoot = depRoot name [ mods.${name} ]; + objects = mapAttrs compileMod mods; + staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } '' + mkdir $out + ar rcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/out.o") (attrValues objects))} + ''; + leanPackage = writeScriptBin "lean" '' + #!${bash}/bin/bash + set -euo pipefail + LEAN_PATH=${modRoot} ${lean}/bin/lean $@ + ''; + leanInteractive = writeScriptBin "lean" '' + #!${bash}/bin/bash + set -euo pipefail + call() { + if [[ -n $json ]]; then + nix develop $@ 2>&1 | awk '/{/ { print $0; next } { gsub(/"/, "\\\"", $0); gsub(/\n/, "\\n", $0); printf "{\"severity\": \"warning\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"\", \"text\": \"%s\"}\n", $0 }' + else + nix develop $@ + fi + } + + json=0 + input= + for p in "$@"; do + [[ "$p" == --json ]] && json=1 + [[ "$p" != -* ]] && input="$(realpath "$p")" + done + + root=. + while [[ "$root" != / ]]; do + [ -f "$root/flake.nix" ] && break + root="$(realpath "$root/..")" + done + if [[ "$root" == / || "$input" != "$root${srcDir}/"* ]]; then + ${leanPackage}/bin/lean $@ + else + input="$(realpath --relative-to="$root${srcDir}" "$input")" + input="''${input%.lean}" + input="''${input//\//.}" + call "$root#mods.\"$input\"" -c lean $@ + fi + ''; + emacs = writeScriptBin "run-emacs" '' + #!${bash}/bin/bash + ${lean-emacs}/bin/emacs --eval '(setq lean4-rootdir "${leanInteractive}")' $@ + ''; } diff --git a/nix/lean-stage0/bin/lean b/nix/lean-stage0/bin/lean new file mode 100755 index 0000000000..0c2dc28fdf --- /dev/null +++ b/nix/lean-stage0/bin/lean @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +set -euo pipefail + +root="$(realpath "$(dirname "$0")")/../../.." +input="${@: -1}" +input="$(realpath --relative-to="$root/src" "$input")" +input="${input%.lean}" +input="${input//\//.}" +nix develop "$root#lean.stdlib.mods.\"$input\"" -c lean $@ 2> /dev/null