1DOLLY 72PACKAGE lean-std3REQUIRES HOST runtime@045# Lean's Init and Std libraries, which the first lean (lean-stage0) compiles6# from the release's sources: each module's .olean files and its C, which cc7# compiles into libInit.a and libStd.a (lean-dolly.mk). Every Lean file8# imports Init.9FROM /v0.1.5/demos/lean/Dollyfile-lean-stage0 5aa7a8099be0bdd91b3fba399edfe3cf183dc81fa17e07cee68ad9519911d20210REQUIRES TOOL ar11REQUIRES TOOL cc12REQUIRES TOOL find13REQUIRES TOOL gzip14REQUIRES TOOL make15REQUIRES TOOL rm16REQUIRES TOOL sed17REQUIRES TOOL tar18REQUIRES TOOL tr19REQUIRES TOOL xargs2021SOURCE /v0.1.5/dist/static/lean/lean.tar.gz ef83239912f7c218c5f0e937de704b7da807b9802b05216414b59b9dec42e0da /tmp/lean.tar.gz22SOURCE /v0.1.5/dist/static/lean/port.tar 1716710f88ccdd478709b75533ef1686ff39e381ad7d66ff65caff992e2dd1a6 /tmp/lean-port.tar23# Stage 1 reads only src/.24SLOP gzip -dc /tmp/lean.tar.gz | tar -xf - -C / && rm -r /tmp/lean.tar.gz /tmp/lean/stage025SLOP tar -xf /tmp/lean-port.tar -C /26SLOP CWD /tmp/lean make -f dolly/lean-dolly.mk -j4 STAGE=1 LIBRARIES='Init Std' LEAN=/usr/lib/lean-stage0/lean2728FOLDER /usr/lib/lean/Init29FILE /usr/lib/lean/Init.olean30FILE /usr/lib/lean/Init.olean.server31FILE /usr/lib/lean/Init.olean.private32FILE /usr/lib/lean/Init.ir33FILE /usr/lib/lean/Init.ir.sig34FILE /usr/lib/lean/Init.ilean35FOLDER /usr/lib/lean/Std36FILE /usr/lib/lean/Std.olean37FILE /usr/lib/lean/Std.olean.server38FILE /usr/lib/lean/Std.olean.private39FILE /usr/lib/lean/Std.ir40FILE /usr/lib/lean/Std.ir.sig41FILE /usr/lib/lean/Std.ilean42FILE /usr/lib/lean/libInit.a43FILE /usr/lib/lean/libStd.a44