1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
# Lean 4 toolchain for the leanPackages set (independent of pkgs.lean4).
{
lib,
stdenv,
symlinkJoin,
cmake,
cctools,
fetchFromGitHub,
git,
gmp,
cadical,
cadical' ? cadical.override { version = "2.1.3"; },
leangz,
pkg-config,
libuv,
perl,
runCommand,
writeText,
testers,
}:
let
lean4 = stdenv.mkDerivation (finalAttrs: {
pname = "lean4";
version = "4.30.0";
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=";
};
# Vendor mimalloc. Upstream has since partially adopted FetchContent:
# https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2
#
# Dynamically adjust the source tree to maintain a healthy boundary
# with Nix and avoid overstepping on its jurisdiction over cache coherence.
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}")'
rm -rf src/lake/examples/git/
substituteInPlace CMakeLists.txt \
--replace-fail 'GIT_REPOSITORY https://github.com/microsoft/mimalloc' \
'SOURCE_DIR "${finalAttrs.mimalloc-src}"' \
--replace-fail 'GIT_TAG ${finalAttrs.mimalloc-src.tag}' ""
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
substituteInPlace src/lake/Lake/Load/Lean/Elab.lean \
--replace-fail \
'let upToDate := (← olean.pathExists) ∧' \
'let upToDate := cfg.pkgDir.toString.startsWith "/nix/store/" ∨ (← olean.pathExists) ∧'
'';
preConfigure = ''
patchShebangs stage0/src/bin/ src/bin/
'';
nativeBuildInputs = [
cmake
leangz
pkg-config
]
++ lib.optionals stdenv.hostPlatform.isDarwin [ cctools.libtool ];
buildInputs = [
gmp
libuv
cadical'
];
nativeCheckInputs = [
git
perl
];
cmakeFlags = [
"-DUSE_GITHASH=OFF"
"-DINSTALL_LICENSE=OFF"
"-DINSTALL_CADICAL=OFF"
"-DINSTALL_LEANTAR=OFF"
"-DUSE_MIMALLOC=ON"
];
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; [ nadja-y ];
mainProgram = "lean";
};
});
oldStorePath = builtins.substring 0 43 (toString lean4);
# Binary-patched for correct runtime discovery in wrapped environments.
wrapped = symlinkJoin {
inherit (lean4) name pname;
paths = [
lean4
cadical'
leangz
];
nativeBuildInputs = [ perl ];
postBuild = ''
newStorePath=$(echo "$out" | head -c 43)
for bin in ${lean4}/bin/*; do
test -f "$bin" || continue
install -m755 "$bin" "$out/bin/"
perl -pi -e "s|\Q${oldStorePath}\E|$newStorePath|g" "$out/bin/$(basename "$bin")"
done
'';
inherit (lean4) version src meta;
passthru = {
inherit (lean4) version src;
tests =
let
src = writeText "smoke.lean" ''
import Std
example : 1 + 1 = 2 := by decide
example : ∀ (x y : BitVec 8), x &&& y = y &&& x := by bv_decide
'';
in
{
version = testers.testVersion {
package = wrapped;
version = "v${lean4.version}";
};
smoke = runCommand "lean4-test-smoke" { } ''
${wrapped}/bin/lean ${src}
touch $out
'';
};
};
};
in
wrapped
|
