Skip to content

Commit

Permalink
Merge pull request #29 from lenianiva/manifests/v4.14.0
Browse files Browse the repository at this point in the history 
feat: Manifest for v4.14.0
  • Loading branch information
@lenianiva
lenianiva authored Dec 6, 2024
2 parents 2f9f764 + f007a92 commit 09894fa
Show file tree
Hide file tree
Showing 7 changed files with 352 additions and 13 deletions.
3 changes: 3 additions & 0 deletions lake.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@
then [(capitalize manifest.name)]
else roots;
deps = deps ++ manifestDeps;

# Fixes some symbol not found errors
groupStaticLibs = true;
};
in {
inherit mkPackage;
Expand Down
1 change: 1 addition & 0 deletions manifests/default.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,5 @@
"v4.11.0" = import ./v4.11.0.nix;
"v4.12.0" = import ./v4.12.0.nix;
"v4.13.0" = import ./v4.13.0.nix;
"v4.14.0" = import ./v4.14.0.nix;
}
335 changes: 335 additions & 0 deletions manifests/v4.14.0.nix
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,335 @@
{
tag = "v4.14.0";
rev = "410fab7284703f41660ca2454218dcca9b2ec896";
bootstrap = {
src,
debug ? false,
stage0debug ? false,
extraCMakeFlags ? [],
stdenv,
lib,
cmake,
gmp,
libuv,
cadical,
git,
gnumake,
bash,
buildLeanPackage,
writeShellScriptBin,
runCommand,
symlinkJoin,
lndir,
perl,
gnused,
darwin,
llvmPackages,
linkFarmFromDrvs,
...
} @ args:
with builtins; rec {
inherit stdenv;
sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
buildCMake = args:
stdenv.mkDerivation ({
nativeBuildInputs = [cmake];
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 = (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"} \
${
if stdenv.isDarwin
then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a ${leancpp}/lib/temp/libleanshell.a -lc++"
else "-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 ${
if stdenv.isDarwin
then "${leancpp}/lib/temp/libleanshell.a"
else ""
} ${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' -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;
};
};
}
20 changes: 10 additions & 10 deletions templates/dependency/lake-manifest.json
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,25 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover-community/batteries",
[{"url": "https://github.com/leanprover-community/aesop.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
"name": "batteries",
"rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"inputRev": "v4.14.0",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/aesop.git",
{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "",
"rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
"name": "aesop",
"rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.13.0",
"inherited": false,
"inputRev": "v4.14.0",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "Example",
"lakeDir": ".lake"}
2 changes: 1 addition & 1 deletion templates/dependency/lakefile.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ import Lake
open Lake DSL

require aesop from git
"https://github.com/leanprover-community/aesop.git" @ "v4.13.0"
"https://github.com/leanprover-community/aesop.git" @ "v4.14.0"

package Example

Expand Down
2 changes: 1 addition & 1 deletion templates/dependency/lean-toolchain
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.13.0
leanprover/lean4:v4.14.0
Loading

0 comments on commit 09894fa

Please sign in to comment.