1DOLLY 72PACKAGE lean3REQUIRES HOST runtime@04REQUIRES HOST stack@05REQUIRES HOST threads@067# Lean 4.35's programs, lean, lake and leanc, linked from the libraries the8# first lean (lean-stage0) compiled: Init and Std (lean-std), Lean9# (lean-meta), and here Lake's and LeanExport's, as upstream links them10# (lean-dolly.mk), with the C++ runtime compiled again from src/. Lake11# compiles a package's C with cc and links it with libuv.12FROM /v0.1.5/demos/lean/Dollyfile-lean-stage0 5aa7a8099be0bdd91b3fba399edfe3cf183dc81fa17e07cee68ad9519911d20213INSTALL /v0.1.5/demos/lean/Dollyfile-lean-std db99fd0597ec7b0b0a19cb76c95acea38f42605ac384e1faa8c3fbc8c69a4f5614INSTALL /v0.1.5/demos/lean/Dollyfile-lean-meta c2800f47b56eb4bb1f1107faee6b44f04eb742eac882a8a81a2874d94ca5a39015INSTALL /v0.1.5/Dollyfile-cc afd89a983721972cb610d1d03ea39d5e6123d50b7b1a2b6922f1265657cc286a16INSTALL /v0.1.5/demos/cmake/Dollyfile-libuv 066e772a7a8c660560af765731d055c77bac33cb8fbcb22b034f5df2d24b65251718REQUIRES HEADER libc19REQUIRES HEADER uv20REQUIRES LIB uv21REQUIRES TOOL ar22REQUIRES TOOL c++23REQUIRES TOOL cc24REQUIRES TOOL cp25REQUIRES TOOL find26REQUIRES TOOL gzip27REQUIRES TOOL make28REQUIRES TOOL patch29REQUIRES TOOL rm30REQUIRES TOOL sed31REQUIRES TOOL stack-wrap32REQUIRES TOOL tar33REQUIRES TOOL tr34REQUIRES TOOL xargs3536SOURCE /v0.1.5/dist/static/lean/lean.tar.gz ef83239912f7c218c5f0e937de704b7da807b9802b05216414b59b9dec42e0da /tmp/lean.tar.gz37SOURCE /v0.1.5/dist/static/lean/port.tar 1716710f88ccdd478709b75533ef1686ff39e381ad7d66ff65caff992e2dd1a6 /tmp/lean-port.tar38# Stage 1 reads only src/.39SLOP gzip -dc /tmp/lean.tar.gz | tar -xf - -C / && rm -r /tmp/lean.tar.gz /tmp/lean/stage040SLOP tar -xf /tmp/lean-port.tar -C /41SLOP CWD /tmp/lean patch -p1 < dolly/lean-dolly.patch42# One job: the kernel holds Lean's libraries, 2.4 GB, and at four jobs the43# lean processes that import them exceeded a 9 GB build.44SLOP CWD /tmp/lean make -f dolly/lean-dolly.mk STAGE=1 LIBRARIES='LeanExport Lake Leanc' \45  LEAN=/usr/lib/lean-stage0/lean GITHASH=eb6cafb7290e8bd5f2937522d8d804f58f02bafc libraries install4647# lean runs a program and checks a proof; lake makes a package and builds48# its program with cc.49FILE /tmp/lean-check/squares.lean50    def main : IO Unit := IO.println s!"{((List.range 10).map (· ^ 2)).foldl (· + ·) 0}"51FILE /tmp/lean-check/proof.lean52    theorem byOmega (x y : Nat) (h : x < y) : x + 1 ≤ y := by omega53SLOP CWD /tmp/lean-check test "$(lean --run squares.lean)" = 28554SLOP CWD /tmp/lean-check lean proof.lean55SLOP CWD /tmp/lean-check lake new greeting && cd greeting && lake build && test "$(.lake/build/bin/greeting)" = 'Hello, world!'56# Lean has no manual pages: lean's and lake's help are theirs.57SLOP mkdir -p /usr/share/man/cat1 && lean --help > /usr/share/man/cat1/lean.1 && lake --help > /usr/share/man/cat1/lake.15859EXPORTS TOOL lean60EXPORTS TOOL lake61EXPORTS TOOL leanc62FOLDER /usr/lib/lean/Lake63FOLDER /usr/lib/lean/LeanExport64FILE /usr/lib/lean/Lake.olean65FILE /usr/lib/lean/Lake.olean.server66FILE /usr/lib/lean/Lake.olean.private67FILE /usr/lib/lean/Lake.ir68FILE /usr/lib/lean/Lake.ir.sig69FILE /usr/lib/lean/Lake.ilean70FILE /usr/lib/lean/LakeMain.olean71FILE /usr/lib/lean/LakeMain.olean.server72FILE /usr/lib/lean/LakeMain.olean.private73FILE /usr/lib/lean/LakeMain.ir74FILE /usr/lib/lean/LakeMain.ir.sig75FILE /usr/lib/lean/LakeMain.ilean76FILE /usr/lib/lean/LeanExport.olean77FILE /usr/lib/lean/LeanExport.ilean78FILE /usr/lib/lean/Leanc.olean79FILE /usr/lib/lean/Leanc.ilean80FILE /usr/lib/lean/libLake.a81FILE /usr/lib/lean/libLeanExport.a82FILE /usr/lib/lean/libLeanc.a83FILE /usr/lib/lean/libleancpp.a84FILE /usr/lib/lean/libleanrt.a85FOLDER /usr/include/lean86FILE /usr/share/licenses/lean/LICENSE87FILE /usr/share/man/cat1/lean.188FILE /usr/share/man/cat1/lake.189