1DOLLY 72PACKAGE lean-meta3REQUIRES HOST runtime@045# Lean's Lean library, the compiler and elaborator that a Lean program6# imports to work with Lean itself, compiled by the first lean (lean-stage0)7# as lean-std is: its .olean files and libLean.a, which every Lean program8# links, as upstream's flags name it.9FROM /v0.1.5/demos/lean/Dollyfile-lean-stage0 5aa7a8099be0bdd91b3fba399edfe3cf183dc81fa17e07cee68ad9519911d20210INSTALL /v0.1.5/demos/lean/Dollyfile-lean-std db99fd0597ec7b0b0a19cb76c95acea38f42605ac384e1faa8c3fbc8c69a4f5611REQUIRES TOOL ar12REQUIRES TOOL cc13REQUIRES TOOL find14REQUIRES TOOL gzip15REQUIRES TOOL make16REQUIRES TOOL rm17REQUIRES TOOL sed18REQUIRES TOOL tar19REQUIRES TOOL tr20REQUIRES TOOL xargs2122SOURCE /v0.1.5/dist/static/lean/lean.tar.gz ef83239912f7c218c5f0e937de704b7da807b9802b05216414b59b9dec42e0da /tmp/lean.tar.gz23SOURCE /v0.1.5/dist/static/lean/port.tar 1716710f88ccdd478709b75533ef1686ff39e381ad7d66ff65caff992e2dd1a6 /tmp/lean-port.tar24# Stage 1 reads only src/.25SLOP gzip -dc /tmp/lean.tar.gz | tar -xf - -C / && rm -r /tmp/lean.tar.gz /tmp/lean/stage026SLOP tar -xf /tmp/lean-port.tar -C /27# Three jobs: the last modules import most of Lean, and four of them at once28# exceeded a 9 GB build.29SLOP CWD /tmp/lean make -f dolly/lean-dolly.mk -j3 STAGE=1 LIBRARIES=Lean LEAN=/usr/lib/lean-stage0/lean3031FOLDER /usr/lib/lean/Lean32FILE /usr/lib/lean/Lean.olean33FILE /usr/lib/lean/Lean.olean.server34FILE /usr/lib/lean/Lean.olean.private35FILE /usr/lib/lean/Lean.ir36FILE /usr/lib/lean/Lean.ir.sig37FILE /usr/lib/lean/Lean.ilean38FILE /usr/lib/lean/libLean.a39