Nadja Yang
03752ca7ca
Lake 4.30.0 uses libtool -static on macOS for static library targets instead of ar. https://github.com/leanprover/lean4/blob/d024af099ca4bf2c86f649261ebf59565dc8c622/src/lake/Lake/Build/Library.lean#L87-L95 See Hydra Build No. 330752454, lean4.aarch64-darwin (June 4, 2026), https://hydra.nixos.org/build/330752454; Hydra Build No. 330752481, leanPackages.lean4.aarch64-darwin (June 4, 2026), https://hydra.nixos.org/build/330752481. Breakage introduced in https://github.com/NixOS/nixpkgs/pull/526718/commits/a26b66330f6fa572e7005ee2a1eb031093456e6e
121 lines
2.8 KiB
Nix
121 lines
2.8 KiB
Nix
{
|
|
lib,
|
|
stdenv,
|
|
cmake,
|
|
cctools,
|
|
fetchFromGitHub,
|
|
git,
|
|
gmp,
|
|
cadical,
|
|
leangz,
|
|
makeWrapper,
|
|
pkg-config,
|
|
libuv,
|
|
enableMimalloc ? true,
|
|
perl,
|
|
testers,
|
|
}:
|
|
let
|
|
cadical' = cadical.override { version = "2.1.3"; };
|
|
in
|
|
stdenv.mkDerivation (finalAttrs: {
|
|
pname = "lean4";
|
|
version = "4.30.0";
|
|
|
|
# Using a vendored version rather than nixpkgs' version to match the exact version required by
|
|
# Lean. Apparently, even a slight version change can impact greatly the final performance.
|
|
mimalloc-src = fetchFromGitHub {
|
|
owner = "microsoft";
|
|
repo = "mimalloc";
|
|
tag = "v2.2.3";
|
|
hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
|
|
};
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "leanprover";
|
|
repo = "lean4";
|
|
tag = "v${finalAttrs.version}";
|
|
hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
|
|
};
|
|
|
|
postPatch =
|
|
let
|
|
pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc";
|
|
in
|
|
''
|
|
substituteInPlace src/CMakeLists.txt \
|
|
--replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
|
|
|
|
# Remove tests that fails in sandbox.
|
|
# It expects `sourceRoot` to be a git repository.
|
|
rm -rf src/lake/examples/git/
|
|
''
|
|
+ (lib.optionalString enableMimalloc ''
|
|
substituteInPlace CMakeLists.txt \
|
|
--replace-fail 'MIMALLOC-SRC' '${finalAttrs.mimalloc-src}'
|
|
for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do
|
|
substituteInPlace "$file" \
|
|
--replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
|
|
done
|
|
'');
|
|
|
|
preConfigure = ''
|
|
patchShebangs stage0/src/bin/ src/bin/
|
|
'';
|
|
|
|
nativeBuildInputs = [
|
|
cmake
|
|
pkg-config
|
|
makeWrapper
|
|
leangz # Provides leantar
|
|
]
|
|
++ lib.optionals stdenv.hostPlatform.isDarwin [ cctools.libtool ];
|
|
|
|
buildInputs = [
|
|
gmp
|
|
libuv
|
|
cadical'
|
|
];
|
|
|
|
postInstall = ''
|
|
wrapProgram $out/bin/lean \
|
|
--prefix PATH : ${cadical'}/bin
|
|
'';
|
|
|
|
nativeCheckInputs = [
|
|
git
|
|
perl
|
|
];
|
|
|
|
patches = [ ./mimalloc.patch ];
|
|
|
|
cmakeFlags = [
|
|
"-DUSE_GITHASH=OFF"
|
|
"-DINSTALL_LICENSE=OFF"
|
|
"-DINSTALL_CADICAL=OFF"
|
|
"-DUSE_MIMALLOC=${if enableMimalloc then "ON" else "OFF"}"
|
|
];
|
|
|
|
passthru.tests = {
|
|
version = testers.testVersion {
|
|
package = finalAttrs.finalPackage;
|
|
version = "v${finalAttrs.version}";
|
|
};
|
|
};
|
|
|
|
meta = {
|
|
description = "Automatic and interactive theorem prover";
|
|
homepage = "https://leanprover.github.io/";
|
|
changelog = "https://github.com/leanprover/lean4/blob/${finalAttrs.src.tag}/RELEASES.md";
|
|
license = lib.licenses.asl20;
|
|
platforms = lib.platforms.all;
|
|
maintainers = with lib.maintainers; [
|
|
danielbritten
|
|
jthulhu
|
|
nadja-y
|
|
niklashh
|
|
];
|
|
mainProgram = "lean";
|
|
};
|
|
})
|