Conversation
Add a Lake project in misc/lean for Lean 4 models of Materialize, with a sample model of update collections that proves consolidation preserves multiplicities and leaves no zero diffs. warningAsError makes any sorry fail the build. The lean mzbuild image installs the toolchain pinned in lean-toolchain and builds the project's dependencies into the image. It copies only lean-toolchain, lakefile.toml and lake-manifest.json from misc/lean, so editing a model reuses the published image. The lean composition copies the mounted sources next to the baked dependencies and runs lake, and a new CI step runs it. Fix the mzbuild copy pre-image, which reported its inputs relative to the source directory instead of the repository root, so fingerprinting any image that used it failed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Build every module under Mz/ with globs, so a model that Mz.lean does not import still fails the build on a sorry. Build each dependency's default targets in the image, since building the placeholder library only cloned them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Build all dependency packages in one lake invocation. A for loop only reported the last package's status, so an earlier failure produced a published image without that package's modules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Delete the static libraries, LLVM, .ilean files and sources from the toolchain, which shrinks it from 3.0 GB to 2.3 GB. Install the toolchain explicitly first, since elan otherwise downloads it lazily on first use. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The lean composition runs one short-lived container and no long-running service, so docker compose logs has nothing to collect and the check failed a passing build. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Batteries, which Aesop and Mathlib require, lists the runLinter executable in its default targets. Linking it needs the static libraries and LLVM, so stripping them breaks the dependency build as soon as any common library is added. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
mz-lake copied the project with a tar of `.`, which makes a non-root user change the mode and mtime of the root-owned /workspace and abort. Copy the entries individually instead. Install the toolchain before the chmod so every file it downloads is readable by any uid. Add nodup_consolidate: the existing theorems also hold for a filter that merges nothing. Fix comments and README claims about image inputs, lake env, and the git safe.directory rule. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A design doc can now live in its own directory under doc/developer/design with .lean files next to it. lakefile.lean, which replaces lakefile.toml, lists those directories when Lake reads it and builds each as a module namespace, so adding a model needs no lakefile edit. The image places the project at its repository path so the lakefile finds the docs relative to itself, the composition mounts the design directory read-only, and mz-lake runs lake with -R because the configuration cached at image build time saw no design doc models. The CI step also runs when a .lean file under doc/developer/design changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Builds on #39444, and includes its commits until that merges. Only the last commit is new.
Motivation
Design docs are where protocol and semantics models get argued, so the model should sit next to the doc it supports and be checked by CI like the models in
misc/lean/Mz.Description
A design doc that carries a model lives in its own directory,
doc/developer/design/<date>_<topic>/, with.leanfiles next to the Markdown.lakefile.lean, which replaceslakefile.toml, lists those directories when Lake reads it and builds each one as a module namespace, so adding a model needs no lakefile edit. A TOML lakefile cannot do this, because it cannot list directories and its glob syntax rejects names that start with a digit. A model's module is«<date>_<topic>».<File>.The image now places the project at
/mz/misc/lean, because the lakefile finds the design docs relative to itself. The composition mountsdoc/developer/designread-only at the matching path. Lake caches the evaluated lakefile, and the copy cached at image build time saw no design doc models, somz-lakepasses-Rto make Lake read the lakefile again on every run. The CI step gainsinputs: ["doc/developer/design/*.lean"], so a change to a design doc model triggers it.Verification
With a scratch
doc/developer/design/20261003_probe/directory, the build compiled«20261003_probe».Model, and an added file containingsorryfailed it, both as root and as a non-root uid. Without-R, the same build silently skipped the design doc models. Editing a model underMz/or a design doc, or the README, leavesbin/mzimage fingerprint leanunchanged, and a run after such an edit rebuilt no image. Editinglakefile.leanchanges the fingerprint.Posted by Claude Code.
🤖 Generated with Claude Code