feat: Nix: Emacs PoC
This commit is contained in:
Sebastian Ullrich
parent
50abe8352b
commit
b2c83a37d8
4 changed files with 106 additions and 40 deletions
65
flake.nix
65
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;
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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\": \"<stdin>\", \"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}")' $@
|
||||
'';
|
||||
}
|
||||
|
|
|
|||
9
nix/lean-stage0/bin/lean
Executable file
9
nix/lean-stage0/bin/lean
Executable file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue