mirror of
https://github.com/NixOS/nixpkgs.git
synced 2026-06-05 21:03:40 +00:00
102 lines
2.6 KiB
Nix
102 lines
2.6 KiB
Nix
{
|
|
lib,
|
|
buildLakePackage,
|
|
runCommand,
|
|
leangz,
|
|
fetchFromGitHub,
|
|
batteries,
|
|
aesop,
|
|
Qq,
|
|
proofwidgets,
|
|
plausible,
|
|
LeanSearchClient,
|
|
importGraph,
|
|
tests,
|
|
}:
|
|
|
|
let
|
|
# build leangz without zstd support, to improve Hydra's xz compression ratio
|
|
leangz-raw = leangz.overrideAttrs { cargoBuildNoDefaultFeatures = true; };
|
|
|
|
mathlib__archive = buildLakePackage (finalAttrs: {
|
|
pname = "lean4-mathlib";
|
|
# nixpkgs-update: no auto update
|
|
version = "4.30.0";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "leanprover-community";
|
|
repo = "mathlib4";
|
|
tag = "v${finalAttrs.version}";
|
|
hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
|
|
};
|
|
|
|
leanPackageName = "mathlib";
|
|
leanDeps = [
|
|
batteries
|
|
aesop
|
|
Qq
|
|
proofwidgets
|
|
plausible
|
|
LeanSearchClient
|
|
importGraph
|
|
];
|
|
|
|
nativeBuildInputs = [ leangz-raw ];
|
|
|
|
# Per-module lgz preprocessing strips olean structural overhead,
|
|
# providing significant compression benefit over a raw xz invocation.
|
|
# This also brings the output under Hydra's max_output_size. The
|
|
# user-facing mathlib derivation unpacks transparently.
|
|
postInstall = ''
|
|
local lib="$out/.lake/build/lib/lean"
|
|
local ir="$out/.lake/build/ir"
|
|
find "$lib" -name '*.trace' -print0 \
|
|
| xargs -0 -P"$NIX_BUILD_CORES" -I{} bash -c '
|
|
base="''${1%.trace}"; rel="''${base#'"$lib"'/}"
|
|
leantar -C "'"$lib"'" -C "'"$ir"'" "$base.ltar" \
|
|
"$rel.trace" "$rel.olean" "$rel.olean.server" "$rel.olean.private" \
|
|
"$rel.ilean" -i 1 "$rel.c"
|
|
rm "$base".{trace,olean,olean.server,olean.private,ilean} "'"$ir"'/$rel.c"
|
|
' _ {}
|
|
'';
|
|
|
|
meta = {
|
|
description = "Mathematical library for Lean 4";
|
|
homepage = "https://github.com/leanprover-community/mathlib4";
|
|
license = lib.licenses.asl20;
|
|
maintainers = with lib.maintainers; [ nadja-y ];
|
|
};
|
|
});
|
|
in
|
|
|
|
runCommand mathlib__archive.name
|
|
{
|
|
nativeBuildInputs = [ leangz-raw ];
|
|
passthru = {
|
|
inherit mathlib__archive;
|
|
inherit (mathlib__archive)
|
|
src
|
|
version
|
|
lakePackageName
|
|
lean4
|
|
allLeanDeps
|
|
computedLakeDeps
|
|
overrideLakeDepsAttrs
|
|
;
|
|
tests = {
|
|
inherit (tests.lake) weak-minimax;
|
|
};
|
|
};
|
|
meta = mathlib__archive.meta // {
|
|
hydraPlatforms = [ ];
|
|
};
|
|
}
|
|
''
|
|
mkdir -p $out
|
|
cp -rT ${mathlib__archive} $out
|
|
chmod -R u+w $out
|
|
find $out/.lake/build/lib -name '*.ltar' \
|
|
-exec leantar -C $out/.lake/build/lib/lean -C $out/.lake/build/ir -x {} +
|
|
find $out/.lake/build/lib -name '*.ltar' -delete
|
|
''
|