chore: remove broken Nix build (#9910)
This commit is contained in:
Sebastian Ullrich
GitHub
parent
93e35dc3da
commit
535435955b
9 changed files with 3 additions and 615 deletions
12
flake.nix
12
flake.nix
|
|
@ -18,14 +18,14 @@
|
|||
# An old nixpkgs for creating releases with an old glibc
|
||||
pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
|
||||
|
||||
lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
|
||||
llvmPackages = pkgs.llvmPackages_15;
|
||||
|
||||
devShellWithDist = pkgsDist: pkgs.mkShell.override {
|
||||
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
|
||||
stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
|
||||
} ({
|
||||
buildInputs = with pkgs; [
|
||||
cmake gmp libuv ccache pkg-config
|
||||
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
|
||||
llvmPackages.llvm # llvm-symbolizer for asan/lsan
|
||||
gdb
|
||||
tree # for CI
|
||||
];
|
||||
|
|
@ -60,12 +60,6 @@
|
|||
GDB = pkgsDist.gdb;
|
||||
});
|
||||
in {
|
||||
packages.${system} = {
|
||||
# to be removed when Nix CI is not needed anymore
|
||||
inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
|
||||
deprecated = lean-packages;
|
||||
};
|
||||
|
||||
devShells.${system} = {
|
||||
# The default development shell for working on lean itself
|
||||
default = devShellWithDist pkgs;
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
set -eo pipefail
|
||||
|
||||
for pkg in $buildInputs; do
|
||||
export PATH=$PATH:$pkg/bin
|
||||
done
|
||||
|
||||
: ${outputs:=out}
|
||||
|
|
@ -1,208 +0,0 @@
|
|||
{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
|
||||
stdenv, lib, cmake, pkg-config, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
|
||||
... } @ args:
|
||||
with builtins;
|
||||
lib.warn "The Nix-based build is deprecated" rec {
|
||||
inherit stdenv;
|
||||
sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
|
||||
buildCMake = args: stdenv.mkDerivation ({
|
||||
nativeBuildInputs = [ cmake pkg-config ];
|
||||
buildInputs = [ gmp libuv llvmPackages.llvm ];
|
||||
# https://github.com/NixOS/nixpkgs/issues/60919
|
||||
hardeningDisable = [ "all" ];
|
||||
dontStrip = (args.debug or debug);
|
||||
|
||||
postConfigure = ''
|
||||
patchShebangs .
|
||||
'';
|
||||
} // args // {
|
||||
src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
|
||||
cmakeFlags = ["-DSMALL_ALLOCATOR=ON" "-DUSE_MIMALLOC=OFF"] ++ (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
|
||||
preConfigure = args.preConfigure or "" + ''
|
||||
# ignore absence of submodule
|
||||
sed -i 's!lake/Lake.lean!!' CMakeLists.txt
|
||||
'';
|
||||
});
|
||||
lean-bin-tools-unwrapped = buildCMake {
|
||||
name = "lean-bin-tools";
|
||||
outputs = [ "out" "leanc_src" ];
|
||||
realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
|
||||
dontBuild = true;
|
||||
installPhase = ''
|
||||
mkdir $out $leanc_src
|
||||
mv bin/ include/ share/ $out/
|
||||
mv leanc.sh $out/bin/leanc
|
||||
mv leanc/Leanc.lean $leanc_src/
|
||||
substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed "
|
||||
substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make"
|
||||
substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash"
|
||||
'';
|
||||
};
|
||||
leancpp = buildCMake {
|
||||
name = "leancpp";
|
||||
src = src + "/src";
|
||||
buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
|
||||
installPhase = ''
|
||||
mkdir -p $out
|
||||
mv lib/ $out/
|
||||
mv runtime/libleanrt_initial-exec.a $out/lib
|
||||
'';
|
||||
};
|
||||
stage0 = args.stage0 or (buildCMake {
|
||||
name = "lean-stage0";
|
||||
realSrc = src + "/stage0/src";
|
||||
debug = stage0debug;
|
||||
cmakeFlags = [ "-DSTAGE=0" ];
|
||||
extraCMakeFlags = [];
|
||||
preConfigure = ''
|
||||
ln -s ${src + "/stage0/stdlib"} ../stdlib
|
||||
'';
|
||||
installPhase = ''
|
||||
mkdir -p $out/bin $out/lib/lean
|
||||
mv bin/lean $out/bin/
|
||||
mv lib/lean/*.{so,dylib} $out/lib/lean
|
||||
'';
|
||||
meta.mainProgram = "lean";
|
||||
});
|
||||
stage = { stage, prevStage, self }:
|
||||
let
|
||||
desc = "stage${toString stage}";
|
||||
build = args: buildLeanPackage.override {
|
||||
lean = prevStage;
|
||||
leanc = lean-bin-tools-unwrapped;
|
||||
# use same stage for retrieving dependencies
|
||||
lean-leanDeps = stage0;
|
||||
lean-final = self;
|
||||
} ({
|
||||
src = src + "/src";
|
||||
roots = [ { mod = args.name; glob = "andSubmodules"; } ];
|
||||
fullSrc = src;
|
||||
srcPath = "$PWD/src:$PWD/src/lake";
|
||||
inherit debug;
|
||||
leanFlags = [ "-DwarningAsError=true" ];
|
||||
} // args);
|
||||
Init' = build { name = "Init"; deps = []; };
|
||||
Std' = build { name = "Std"; deps = [ Init' ]; };
|
||||
Lean' = build { name = "Lean"; deps = [ Std' ]; };
|
||||
attachSharedLib = sharedLib: pkg: pkg // {
|
||||
inherit sharedLib;
|
||||
mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
|
||||
};
|
||||
in (all: all // all.lean) rec {
|
||||
inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
|
||||
Init = attachSharedLib leanshared Init';
|
||||
Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
|
||||
Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
|
||||
Lake = build {
|
||||
name = "Lake";
|
||||
sharedLibName = "Lake_shared";
|
||||
src = src + "/src/lake";
|
||||
deps = [ Init Lean ];
|
||||
};
|
||||
Lake-Main = build {
|
||||
name = "LakeMain";
|
||||
roots = [{ glob = "one"; mod = "LakeMain"; }];
|
||||
executableName = "lake";
|
||||
deps = [ Lake ];
|
||||
linkFlags = lib.optional stdenv.isLinux "-rdynamic";
|
||||
src = src + "/src/lake";
|
||||
};
|
||||
stdlib = [ Init Std Lean Lake ];
|
||||
modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
|
||||
depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
|
||||
iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
|
||||
Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
|
||||
stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
|
||||
libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
|
||||
mkdir $out
|
||||
touch empty.c
|
||||
${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
|
||||
'';
|
||||
leanshared_1 = runCommand "leanshared_1" { buildInputs = [ stdenv.cc ]; libName = "leanshared_1${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
|
||||
mkdir $out
|
||||
touch empty.c
|
||||
${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
|
||||
'';
|
||||
leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
|
||||
mkdir $out
|
||||
LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
|
||||
-Wl,--whole-archive ${leancpp}/lib/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ \
|
||||
-lm ${stdlibLinkFlags} \
|
||||
$(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
|
||||
-o $out/$libName
|
||||
'';
|
||||
mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
|
||||
print-paths = Lean.makePrintPathsFor [] mods;
|
||||
leanc = writeShellScriptBin "leanc" ''
|
||||
LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
|
||||
'';
|
||||
lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
|
||||
mkdir -p $out/bin
|
||||
${leanc}/bin/leanc ${leancpp}/lib/temp/libleanmain.a ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* -o $out/bin/lean
|
||||
'';
|
||||
# derivation following the directory layout of the "basic" setup, mostly useful for running tests
|
||||
lean-all = stdenv.mkDerivation {
|
||||
name = "lean-${desc}";
|
||||
buildCommand = ''
|
||||
mkdir -p $out/bin $out/lib/lean
|
||||
ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
|
||||
# put everything in a single final derivation so `IO.appDir` references work
|
||||
cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
|
||||
# NOTE: `lndir` will not override existing `bin/leanc`
|
||||
${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
|
||||
'';
|
||||
meta.mainProgram = "lean";
|
||||
};
|
||||
cacheRoots = linkFarmFromDrvs "cacheRoots" ([
|
||||
stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
|
||||
] ++ map (lib: lib.oTree) stdlib);
|
||||
test = buildCMake {
|
||||
name = "lean-test-${desc}";
|
||||
realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
|
||||
buildInputs = [ gmp libuv perl git cadical ];
|
||||
preConfigure = ''
|
||||
cd src
|
||||
'';
|
||||
extraCMakeFlags = [ "-DLLVM=OFF" ];
|
||||
postConfigure = ''
|
||||
patchShebangs ../../tests ../lake
|
||||
rm -r bin lib include share
|
||||
ln -sf ${lean-all}/* .
|
||||
'';
|
||||
buildPhase = ''
|
||||
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
|
||||
'';
|
||||
installPhase = ''
|
||||
mkdir $out
|
||||
mv test-results.xml $out
|
||||
'';
|
||||
};
|
||||
update-stage0 =
|
||||
let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
|
||||
writeShellScriptBin "update-stage0" ''
|
||||
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
|
||||
'';
|
||||
update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
|
||||
set -euo pipefail
|
||||
${update-stage0}/bin/update-stage0
|
||||
git commit -m "chore: update stage0"
|
||||
'';
|
||||
link-ilean = writeShellScriptBin "link-ilean" ''
|
||||
dest=''${1:-src}
|
||||
rm -rf $dest/build/lib || true
|
||||
mkdir -p $dest/build/lib
|
||||
ln -s ${iTree}/* $dest/build/lib
|
||||
'';
|
||||
benchmarks =
|
||||
let
|
||||
entries = attrNames (readDir (src + "/tests/bench"));
|
||||
leanFiles = map (n: elemAt n 0) (filter (n: n != null) (map (match "(.*)\.lean") entries));
|
||||
in lib.genAttrs leanFiles (n: (buildLeanPackage {
|
||||
name = n;
|
||||
src = filterSource (e: _: baseNameOf e == "${n}.lean") (src + "/tests/bench");
|
||||
}).executable);
|
||||
};
|
||||
stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
|
||||
stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
|
||||
stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
|
||||
}
|
||||
|
|
@ -1,247 +0,0 @@
|
|||
{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
|
||||
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
|
||||
runCommand, darwin, mkShell, ... }:
|
||||
let lean-final' = lean-final; in
|
||||
lib.makeOverridable (
|
||||
{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
|
||||
# Lean dependencies. Each entry should be an output of buildLeanPackage.
|
||||
deps ? [ lean.Init lean.Std lean.Lean ],
|
||||
# Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
|
||||
staticLibDeps ? [],
|
||||
# Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
|
||||
groupStaticLibs ? false,
|
||||
# Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
|
||||
# shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
|
||||
# These libs are also linked to in packages that depend on this one.
|
||||
nativeSharedLibs ? [],
|
||||
# Lean modules to include.
|
||||
# A set of Lean modules names as strings (`"Foo.Bar"`) or attrsets (`{ name = "Foo.Bar"; glob = "one" | "submodules" | "andSubmodules"; }`);
|
||||
# see Lake README for glob meanings. Dependencies of selected modules are always included.
|
||||
roots ? [ name ],
|
||||
# Output from `lean --deps-json` on package source files. Persist the corresponding output attribute to a file and pass it back in here to avoid IFD.
|
||||
# Must be refreshed on any change in `import`s or set of source file names.
|
||||
modDepsFile ? null,
|
||||
# Whether to compile each module into a native shared library that is loaded whenever the module is imported in order to accelerate evaluation
|
||||
precompileModules ? false,
|
||||
# Whether to compile the package into a native shared library that is loaded whenever *any* of the package's modules is imported into another package.
|
||||
# If `precompileModules` is also `true`, the latter only affects imports within the current package.
|
||||
precompilePackage ? precompileModules,
|
||||
# Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
|
||||
pluginDeps ? [],
|
||||
# `overrideAttrs` for `buildMod`
|
||||
overrideBuildModAttrs ? null,
|
||||
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
|
||||
srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
|
||||
with builtins; let
|
||||
# "Init.Core" ~> "Init/Core"
|
||||
modToPath = mod: replaceStrings ["."] ["/"] mod;
|
||||
modToAbsPath = mod: "${src}/${modToPath mod}";
|
||||
# sanitize file name before copying to store, except when already in store
|
||||
copyToStoreSafe = base: suffix: if lib.isDerivation base then base + suffix else
|
||||
builtins.path { name = lib.strings.sanitizeDerivationName (baseNameOf suffix); path = base + suffix; };
|
||||
modToLean = mod: copyToStoreSafe src "/${modToPath mod}.lean";
|
||||
bareStdenv = ./bareStdenv;
|
||||
mkBareDerivation = args: derivation (args // {
|
||||
name = lib.strings.sanitizeDerivationName args.name;
|
||||
stdenv = bareStdenv;
|
||||
inherit (stdenv) system;
|
||||
buildInputs = (args.buildInputs or []) ++ [ coreutils ];
|
||||
builder = stdenv.shell;
|
||||
args = [ "-c" ''
|
||||
source $stdenv/setup
|
||||
set -u
|
||||
${args.buildCommand}
|
||||
'' ];
|
||||
}) // { overrideAttrs = f: mkBareDerivation (lib.fix (lib.extends f (_: args))); };
|
||||
runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
|
||||
runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
|
||||
preferLocalBuild = true;
|
||||
allowSubstitutes = false;
|
||||
}) buildCommand;
|
||||
mkSharedLib = name: args: runBareCommand "${name}-dynlib" {
|
||||
buildInputs = [ stdenv.cc ] ++ lib.optional stdenv.isDarwin darwin.cctools;
|
||||
libName = "${name}${stdenv.hostPlatform.extensions.sharedLibrary}";
|
||||
} ''
|
||||
mkdir -p $out
|
||||
${leanc}/bin/leanc -shared ${args} -o $out/$libName
|
||||
'';
|
||||
depRoot = name: deps: mkBareDerivation {
|
||||
name = "${name}-depRoot";
|
||||
inherit deps;
|
||||
depRoots = map (drv: drv.LEAN_PATH) deps;
|
||||
|
||||
passAsFile = [ "deps" "depRoots" ];
|
||||
buildCommand = ''
|
||||
mkdir -p $out
|
||||
for i in $(cat $depRootsPath); do
|
||||
cp -dru --no-preserve=mode $i/. $out
|
||||
done
|
||||
for i in $(cat $depsPath); do
|
||||
cp -drsu --no-preserve=mode $i/. $out
|
||||
done
|
||||
'';
|
||||
};
|
||||
srcRoot = src;
|
||||
|
||||
# A flattened list of Lean-module dependencies (`deps`)
|
||||
allExternalDeps = lib.unique (lib.foldr (dep: allExternalDeps: allExternalDeps ++ [ dep ] ++ dep.allExternalDeps) [] deps);
|
||||
allNativeSharedLibs =
|
||||
lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
|
||||
|
||||
# A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
|
||||
# plus every dep module itself: `dep.staticLib`
|
||||
allStaticLibDeps =
|
||||
lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
|
||||
|
||||
pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
|
||||
|
||||
leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
|
||||
loadDynlibsOfDeps = deps: lib.unique (concatMap (d: d.propagatedLoadDynlibs) deps);
|
||||
|
||||
# submodules "Init" = ["Init.List.Basic", "Init.Core", ...]
|
||||
submodules = mod: let
|
||||
dir = readDir (modToAbsPath mod);
|
||||
f = p: t:
|
||||
if t == "directory" then
|
||||
submodules "${mod}.${p}"
|
||||
else
|
||||
let m = builtins.match "(.*)\.lean" p;
|
||||
in lib.optional (m != null) "${mod}.${head m}";
|
||||
in concatLists (lib.mapAttrsToList f dir);
|
||||
|
||||
# conservatively approximate list of source files matched by glob
|
||||
expandGlobAllApprox = g:
|
||||
if typeOf g == "string" then
|
||||
# we can't know the required files without parsing dependencies (which is what we want this
|
||||
# function for), so we approximate to the entire package.
|
||||
let root = (head (split "\\." g));
|
||||
in lib.optional (pathExists (src + "/${modToPath root}.lean")) root ++ lib.optionals (pathExists (modToAbsPath root)) (submodules root)
|
||||
else if g.glob == "one" then expandGlobAllApprox g.mod
|
||||
else if g.glob == "submodules" then submodules g.mod
|
||||
else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
|
||||
else throw "unknown glob kind '${g}'";
|
||||
# list of modules that could potentially be involved in the build
|
||||
candidateMods = lib.unique (concatMap expandGlobAllApprox roots);
|
||||
candidateFiles = map modToLean candidateMods;
|
||||
modDepsFile = args.modDepsFile or mkBareDerivation {
|
||||
name = "${name}-deps.json";
|
||||
candidateFiles = lib.concatStringsSep " " candidateFiles;
|
||||
passAsFile = [ "candidateFiles" ];
|
||||
buildCommand = ''
|
||||
mkdir $out
|
||||
${lean-leanDeps}/bin/lean --deps-json --stdin < $candidateFilesPath > $out/$name
|
||||
'';
|
||||
};
|
||||
modDeps = fromJSON (
|
||||
# the only possible references to store paths in the JSON should be inside errors, so no chance of missed dependencies from this
|
||||
unsafeDiscardStringContext (readFile "${modDepsFile}/${modDepsFile.name}"));
|
||||
# map from module name to list of imports
|
||||
modDepsMap = listToAttrs (lib.zipListsWith lib.nameValuePair candidateMods modDeps.imports);
|
||||
maybeOverrideAttrs = f: x: if f != null then x.overrideAttrs f else x;
|
||||
# build module (.olean and .c) given derivations of all (immediate) dependencies
|
||||
# TODO: make `rec` parts override-compatible?
|
||||
buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
|
||||
name = "${mod}";
|
||||
LEAN_PATH = depRoot mod deps;
|
||||
LEAN_ABORT_ON_PANIC = "1";
|
||||
relpath = modToPath mod;
|
||||
buildInputs = [ lean ];
|
||||
leanPath = relpath + ".lean";
|
||||
# should be either single .lean file or directory directly containing .lean file plus dependencies
|
||||
src = copyToStoreSafe srcRoot ("/" + leanPath);
|
||||
outputs = [ "out" "ilean" "c" ];
|
||||
oleanPath = relpath + ".olean";
|
||||
ileanPath = relpath + ".ilean";
|
||||
cPath = relpath + ".c";
|
||||
inherit leanFlags leanPluginFlags;
|
||||
leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
|
||||
buildCommand = ''
|
||||
dir=$(dirname $relpath)
|
||||
mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
|
||||
if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
|
||||
lean -o $out/$oleanPath -i $out/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
|
||||
'';
|
||||
}) // {
|
||||
inherit deps;
|
||||
propagatedLoadDynlibs = loadDynlibsOfDeps deps;
|
||||
};
|
||||
compileMod = mod: drv: mkBareDerivation {
|
||||
name = "${mod}-cc";
|
||||
buildInputs = [ leanc stdenv.cc ];
|
||||
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
|
||||
# on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
|
||||
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
|
||||
'';
|
||||
};
|
||||
mkMod = mod: deps:
|
||||
let drv = buildMod mod deps;
|
||||
obj = compileMod mod drv;
|
||||
# this attribute will only be used if any dependent module is precompiled
|
||||
sharedLib = mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: pathOfSharedLib d.sharedLib) deps)}";
|
||||
in drv // {
|
||||
inherit obj sharedLib;
|
||||
} // lib.optionalAttrs precompileModules {
|
||||
propagatedLoadDynlibs = [sharedLib];
|
||||
};
|
||||
externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} allExternalDeps;
|
||||
# map from module name to derivation
|
||||
modCandidates = mapAttrs (mod: header:
|
||||
let
|
||||
deps = if header.errors == []
|
||||
then map (m: m.module) header.result.imports
|
||||
else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
|
||||
in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
|
||||
expandGlob = g:
|
||||
if typeOf g == "string" then [g]
|
||||
else if g.glob == "one" then [g.mod]
|
||||
else if g.glob == "submodules" then submodules g.mod
|
||||
else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
|
||||
else throw "unknown glob kind '${g}'";
|
||||
# subset of `modCandidates` that is transitively reachable from `roots`
|
||||
mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
|
||||
startSet = map (m: { key = m; }) (concatMap expandGlob roots);
|
||||
operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
|
||||
}));
|
||||
allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
|
||||
|
||||
objects = mapAttrs (_: m: m.obj) mods';
|
||||
bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
|
||||
staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
|
||||
mkdir -p $out
|
||||
ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
|
||||
'';
|
||||
|
||||
staticLibLinkWrapper = libs: if groupStaticLibs && !stdenv.isDarwin
|
||||
then "-Wl,--start-group ${libs} -Wl,--end-group"
|
||||
else "${libs}";
|
||||
in rec {
|
||||
inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps src objects staticLib modDepsFile;
|
||||
mods = mapAttrs (_: m:
|
||||
m //
|
||||
# if neither precompilation option was set but a dependent module wants to be precompiled, default to precompiling this package whole
|
||||
lib.optionalAttrs (precompilePackage || !precompileModules) { inherit sharedLib; } //
|
||||
lib.optionalAttrs precompilePackage { propagatedLoadDynlibs = [sharedLib]; })
|
||||
mods';
|
||||
modRoot = depRoot name (attrValues mods);
|
||||
depRoots = linkFarmFromDrvs "depRoots" (map (m: m.LEAN_PATH) (attrValues mods));
|
||||
cTree = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
|
||||
oTree = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
|
||||
iTree = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
|
||||
sharedLib = mkSharedLib "lib${sharedLibName}" ''
|
||||
${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
|
||||
${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
|
||||
executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
|
||||
objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
|
||||
in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
|
||||
mkdir -p $out/bin
|
||||
leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \
|
||||
-o $out/bin/${executableName} \
|
||||
${lib.concatStringsSep " " allLinkFlags}
|
||||
'') {};
|
||||
})
|
||||
|
|
@ -1,42 +0,0 @@
|
|||
#!@bash@/bin/bash
|
||||
|
||||
set -euo pipefail
|
||||
|
||||
function pebkac() {
|
||||
echo 'This is just a simple Nix adapter for `lake print-paths|serve`.'
|
||||
exit 1
|
||||
}
|
||||
|
||||
[[ $# -gt 0 ]] || pebkac
|
||||
case $1 in
|
||||
--version)
|
||||
# minimum version for `lake serve` with fallback
|
||||
echo 3.1.0
|
||||
;;
|
||||
print-paths)
|
||||
shift
|
||||
deps="$@"
|
||||
root=.
|
||||
# fall back to initial package if not in package
|
||||
[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
|
||||
target="$root#print-paths"
|
||||
args=()
|
||||
# HACK: use stage 0 instead of 1 inside Lean's own `src/`
|
||||
[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@
|
||||
for dep in $deps; do
|
||||
target="$target.\"$dep\""
|
||||
done
|
||||
echo "Building dependencies..." >&2
|
||||
# -v only has "built ...", but "-vv" is a bit too verbose
|
||||
exec @nix@/bin/nix run "$target" ${args[*]} -v
|
||||
;;
|
||||
serve)
|
||||
shift
|
||||
[[ ${1:-} == "--" ]] && shift
|
||||
# `link-ilean` puts them there
|
||||
LEAN_PATH=${LEAN_PATH:+$LEAN_PATH:}$PWD/build/lib exec $(dirname $0)/lean --server "$@"
|
||||
;;
|
||||
*)
|
||||
pebkac
|
||||
;;
|
||||
esac
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
#!@bash@/bin/bash
|
||||
|
||||
set -euo pipefail
|
||||
|
||||
root="."
|
||||
# find package root
|
||||
while [[ "$root" != / ]]; do
|
||||
[ -f "$root/flake.nix" ] && break
|
||||
root="$(realpath "$root/..")"
|
||||
done
|
||||
# fall back to initial package if not in package
|
||||
[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
|
||||
|
||||
# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic)
|
||||
target="$root#lean-package"
|
||||
for arg in "$@"; do
|
||||
case $arg in
|
||||
--server | --worker | -v | --version)
|
||||
target="$root#lean"
|
||||
;;
|
||||
esac
|
||||
done
|
||||
|
||||
args=(-- "$@")
|
||||
# HACK: use stage 0 instead of 1 inside Lean's own `src/`
|
||||
[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
|
||||
|
||||
LEAN_SYSROOT="$(dirname "$0")/.." exec @nix@/bin/nix ${LEAN_NIX_ARGS:-} run "$target" ${args[*]}
|
||||
|
|
@ -1,52 +0,0 @@
|
|||
{ src, pkgs, ... } @ args:
|
||||
with pkgs;
|
||||
let
|
||||
# https://github.com/NixOS/nixpkgs/issues/130963
|
||||
llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
|
||||
cc = (ccacheWrapper.override rec {
|
||||
cc = llvmPackages.clang;
|
||||
extraConfig = ''
|
||||
export CCACHE_DIR=/nix/var/cache/ccache
|
||||
export CCACHE_UMASK=007
|
||||
export CCACHE_BASE_DIR=$NIX_BUILD_TOP
|
||||
# https://github.com/NixOS/nixpkgs/issues/109033
|
||||
args=("$@")
|
||||
for ((i=0; i<"''${#args[@]}"; i++)); do
|
||||
case ''${args[i]} in
|
||||
-frandom-seed=*) unset args[i]; break;;
|
||||
esac
|
||||
done
|
||||
set -- "''${args[@]}"
|
||||
[ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@"
|
||||
'';
|
||||
}).overrideAttrs (old: {
|
||||
# https://github.com/NixOS/nixpkgs/issues/119779
|
||||
installPhase = builtins.replaceStrings ["use_response_file_by_default=1"] ["use_response_file_by_default=0"] old.installPhase;
|
||||
});
|
||||
stdenv' = if stdenv.isLinux then useGoldLinker stdenv else stdenv;
|
||||
lean = callPackage (import ./bootstrap.nix) (args // {
|
||||
stdenv = overrideCC stdenv' cc;
|
||||
inherit src buildLeanPackage llvmPackages;
|
||||
});
|
||||
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;
|
||||
lean = lean.stage1;
|
||||
inherit (lean.stage1) leanc;
|
||||
}));
|
||||
in {
|
||||
inherit cc buildLeanPackage llvmPackages;
|
||||
nixpkgs = pkgs;
|
||||
ciShell = writeShellScriptBin "ciShell" ''
|
||||
set -o pipefail
|
||||
export PATH=${moreutils}/bin:$PATH
|
||||
# prefix lines with cumulative and individual execution time
|
||||
"$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
|
||||
'';
|
||||
} // lean.stage1
|
||||
|
|
@ -1 +0,0 @@
|
|||
#eval "Hello, world!"
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
{
|
||||
description = "My Lean package";
|
||||
|
||||
inputs.lean.url = "github:leanprover/lean4";
|
||||
inputs.flake-utils.url = "github:numtide/flake-utils";
|
||||
|
||||
outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
|
||||
let
|
||||
leanPkgs = lean.packages.${system};
|
||||
pkg = leanPkgs.buildLeanPackage {
|
||||
name = "MyPackage"; # must match the name of the top-level .lean file
|
||||
src = ./.;
|
||||
};
|
||||
in {
|
||||
packages = pkg // {
|
||||
inherit (leanPkgs) lean;
|
||||
};
|
||||
|
||||
defaultPackage = pkg.modRoot;
|
||||
});
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue