max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: Nix: preserve module directory structure in .c and .o outputs

Browse source 
This simplifies update-stage0 and makes linker errors from static libraries less confusing
This commit is contained in:
Sebastian Ullrich 2020-11-22 13:39:27 +01:00
parent b3165709d2
commit b02413120f
1 changed files with 17 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
nix/buildLeanPackage.nix
View file

@ -1,7 +1,8 @@
{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeShellScriptBin, bash, lean-emacs, nix, substituteAll }:
with builtins; let
# "Init.Core" ~> "Init/Core.lean"
modToLean = mod: replaceStrings ["."] ["/"] mod + ".lean";
# "Init.Core" ~> "Init/Core"
modToPath = mod: replaceStrings ["."] ["/"] mod;
modToLean = mod: modToPath mod + ".lean";
mkDerivation = args@{ buildCommand, ... }: derivation (args // {
inherit stdenv;
inherit (stdenv) system;
@ -38,6 +39,7 @@ with builtins; let
};
in
{ name, src, srcDir ? "", deps }: let
srcRoot = src;
fakeDepRoot = runCommandLocal "${name}-dep-root" {} ''
mkdir $out
cd $out
@ -55,19 +57,21 @@ in
preferLocalBuild = true;
allowSubstitutes = false;
};
#${lean}/bin/lean --deps ${src}/${modToLean mod} | sed -n "s!$LEAN_PATH/!!;\!^${name}/!{s!/!.!g;s!.olean!!;p}" > $out
# build module (.olean and .c) given derivations of all (transitive) dependencies
buildMod = mod: deps: let relpath = modToLean mod; in mkDerivation {
buildMod = mod: deps: mkDerivation rec {
name = "${mod}";
LEAN_PATH = depRoot mod deps;
inherit relpath;
relpath = modToPath mod;
buildInputs = [ lean ];
leanPath = relpath + ".lean";
src = srcRoot + ("/" + leanPath);
outputs = [ "out" "c" ];
src = src + ("/" + relpath);
oleanPath = relpath + ".olean";
cPath = relpath + ".c";
buildCommand = ''
mkdir -p $(dirname $relpath) $out/$(dirname $relpath) $c
cp $src $relpath
lean -o $out/''${relpath%.lean}.olean -c $c/out.c $relpath
mkdir -p $(dirname $relpath) $out/$(dirname $relpath) $c/$(dirname $relpath)
cp $src $leanPath
lean -o $out/$oleanPath -c $c/$cPath $leanPath
'';
} // {
inherit deps;
@ -75,12 +79,11 @@ in
compileMod = mod: drv: mkDerivation {
name = "${mod}-cc";
buildInputs = [ leanc ];
src = "${drv.c}/out.c";
hardeningDisable = [ "all" ];
oPath = drv.relpath + ".o";
buildCommand = ''
mkdir -p $out
ln -s $src out.c
leanc -c -o $out/out.o out.c ${if debug then "-g" else "-O3 -DNDEBUG"}
mkdir -p $out/$(dirname ${drv.relpath})
leanc -c -o $out/$oPath ${drv.c}/${drv.cPath} ${if debug then "-g" else "-O3 -DNDEBUG"}
'';
};
singleton = name: value: listToAttrs [ { inherit name value; } ];
@ -102,7 +105,7 @@ in
objects = mapAttrs compileMod mods;
staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
mkdir $out
ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/out.o") (attrValues objects))}
ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))}
'';
lean-package = writeShellScriptBin "lean" ''