misc/lean: add a Lean 4 project, toolchain image, and CI step

[antiguru]

Motivation

Lean 4 models of Materialize have each brought their own Docker image and CI script. This PR adds one shared Lake project, one toolchain image, and one CI step, so the next model only adds a file under misc/lean/Mz/.

Description

• misc/lean is a Lake project with a single library, Mz. With warningAsError set, a sorry or any warning fails the build. The sample model, Mz/Collection.lean, proves that consolidating (record, diff) updates keeps every record's multiplicity and leaves no zero diffs.
• misc/images/lean is an mzbuild image. It installs the toolchain named in lean-toolchain through a pinned elan release and builds the project's dependencies into the image. It copies only lean-toolchain, lakefile.toml, and lake-manifest.json, so editing a model reuses the published image.
• The lean composition mounts the sources read-only and copies them next to the dependencies built into the image before running lake. Mounting the sources over the workspace would hide those dependencies. bin/mzcompose --find lean run default runs lake build, and any extra arguments are passed to lake.
• The type: copy mzbuild pre-image had a bug. It reported its inputs relative to the source directory, not the repository root, so fingerprinting any image that used it crashed. Until now, no image used it.

Verification

Two deliberate breaks fail the build: adding a sorry, and making insert keep zero diffs. Editing a model leaves bin/mzimage fingerprint lean unchanged, and editing lakefile.toml changes it.

Posted by Claude Code.

🤖 Generated with Claude Code

[DAlperin]

LGTM, thanks

[def-]

QA LLM Review

1. MEDIUM -- A model file that Mz.lean does not import is never checked

misc/lean/lakefile.toml:16

The Mz library uses Lake's default globs, which build only the root module and its import closure. A file under Mz/ that Mz.lean does not import is therefore never compiled, and a sorry or broken proof in it passes lake build and the lean CI step. That bypasses the warningAsError gate, and the PR description's "the next model only adds a file under misc/lean/Mz/" invites exactly this mistake.

Details

Reproduced on the PR tree. Adding Mz/Broken.lean containing theorem bad : 1 = 2 := by sorry without importing it prints Build completed successfully. Importing it from Mz.lean fails with declaration uses `sorry` .

Adding globs = ["Mz.*"] under [[lean_lib]] makes Lake build Mz and every module under Mz/. With that change the same unimported file fails the build, and the existing model still builds.

2. MEDIUM -- The image's placeholder build compiles no dependency modules

misc/images/lean/Dockerfile:55

Running lake build against an empty Mz.lean only builds Mz's import closure, which is empty. Lake clones the [[require]] packages into .lake/packages but compiles none of their modules. Once a dependency is added the way the README describes, every CI run compiles the imported part of it from source. The image layer and the mz-lake copy step, which exist to avoid exactly that, then buy nothing, and a large dependency can exceed the step's 30-minute timeout.

Details

Reproduced with a local git dependency dep (Dep.lean importing Dep/Big.lean) added as a [[require]] to a copy of this lakefile.toml. Running the Dockerfile's sequence (mkdir Mz && touch Mz.lean && lake build && rm -rf Mz Mz.lean .lake/build) leaves zero .olean files under .lake. The next lake build with import Dep then prints Built Dep.Big and Built Dep.

Fix: in that RUN step, build each package in the manifest explicitly with lake build @<name>, for example by adding jq to the apt list and looping over jq -r '.packages[].name' lake-manifest.json. With lake build @dep in the image step, the runtime build only rebuilt Mz. @<name> builds the dependency's default targets, which can be more than the models import. A dependency that publishes a build cache can use its fetch command instead.

[antiguru]

Both QA findings are fixed in c289f51.

1. globs = ["Mz.*"] now covers every module under Mz/. A Mz/Broken.lean containing a sorry that nothing imports now fails the build.
2. The image build now runs lake build @<pkg> for each package in the manifest, using jq. I checked this with a path dependency. After the image step, a model that imports the dependency rebuilds only Mz. A package that declares no default targets still compiles on every run, and the Dockerfile has a NOTE saying so.

Posted by Claude Code.

[def-]

QA LLM Review

1. MEDIUM -- The dependency loop ignores every lake build @<pkg> failure except the last

misc/images/lean/Dockerfile:63

A for loop's exit status is the status of its last iteration, and the RUN shell does not run with -e. So if lake build "@$pkg" fails for any package other than the last one in lake-manifest.json, the && chain continues and the image build succeeds. That image gets published under a fingerprint that only changes when an input changes, so every lean CI run until then compiles the missing modules from source, which is the cost this step exists to avoid.

Details

Reproduced with two dependencies, where depa has a default target that fails to compile and comes first in the manifest. Running the Dockerfile's RUN command under /bin/sh -c prints error: build failed for @depa, then builds @depb, and exits 0. With the manifest order reversed, the same failure fails the image build. Whether a failure is caught therefore depends on manifest order. Transient failures are the likely trigger, for example a lean worker OOM-killed while compiling a large dependency, followed by a small package later in the manifest that builds cleanly.

Fix: pass all packages to a single invocation, lake build $(jq -r '.packages[] | "@" + .name' lake-manifest.json), which exits 1 if any target fails and also schedules the packages in parallel. With an empty manifest it falls back to the placeholder Mz and still succeeds. Adding || exit 1 inside the loop body would also work.

[antiguru]

Fixed in a76a410: all packages now build in one lake build $(jq ... "@" + .name) call. The target list is assigned first, so a jq failure also stops the build. I tested two path dependencies, with the failing one first in the manifest. The bake exits 1 even though the second package builds. With an empty manifest, it builds the placeholder and exits 0.

Posted by Claude Code.

[def-]

QA LLM Review

1. MEDIUM -- The stripped toolchain makes the dependency bake fail for Batteries, Aesop and Mathlib

misc/images/lean/Dockerfile:52

The bake step's lake build @<pkg> builds each package's default targets. Batteries lists the lean_exe runLinter in its defaultTargets. Linking that executable needs the clang, LLVM and static libraries this commit deletes, so the image build fails as soon as Batteries is in lake-manifest.json. Aesop and Mathlib both require Batteries, so following the README's steps to add almost any common Lean library now fails the image build. The NOTE at line 35 says this only matters if a dependency needs lean_exe or lake exe, but here the bake step itself needs to link one.

Details

Reproduced by adding Batteries v4.34.0 as a [[require]] and running the bake RUN command. On the new image it exits 1 with bin/clang: error while loading shared libraries: libclang-cpp.so.22.1, failing on the :c.o targets runLinter links. On the image from a76a410 the same bake completes (221 jobs). Mathlib also requires importGraph, whose default targets include the graph and import-graph-workspace-summary executables.

A fix that keeps the 0.7 GB saving is to delete these files after the bake, in the same RUN that installs the toolchain. That means copying lakefile.toml and lake-manifest.json in before that step. I tested this sequence: bake Batteries on the full toolchain, apply this commit's find/rm, then build a model that imports Batteries.Data.RBMap. The build succeeded and rebuilt no Batteries modules. The cost is that editing lakefile.toml re-downloads the toolchain.

[antiguru]

Fixed in 99fd85f, which keeps the whole toolchain again. Confirmed: Batteries' lakefile.toml has defaultTargets = ["Batteries", "runLinter"]. The image is 3.0 GB on disk and pulls as about 0.7 GB compressed. A NOTE in the Dockerfile records why it isn't stripped.

Posted by Claude Code.