misc/lean: check Lean models attached to design docs

ci/plugins/mzcompose/hooks/command

@@ -444,6 +444,7 @@ cleanup() {
     && [ "$BUILDKITE_LABEL" != "Parallel Benchmark against QA Canary Environment" ] \
     && [ "$BUILDKITE_LABEL" != "Parallel Benchmark against QA Benchmarking Staging Environment" ] \
     && [ "$BUILDKITE_LABEL" != ":rust: Miri test (full)" ] \
+    && [ "$BUILDKITE_LABEL" != "Lean models" ] \
     && [[ ! "$BUILDKITE_LABEL" =~ Terraform\ .* ]] \
     && [[ ! "$BUILDKITE_LABEL" =~ Orchestratord\ .* ]] \
     && [[ ! "$BUILDKITE_LABEL" =~ Cluster\ spec\ sheet.* ]] \

ci/test/lint-main/checks/check-copyright.sh

@@ -32,6 +32,7 @@ copyright_files=$(grep -vE \
     -e '(^|/)Cargo\.lock$' \
     -e '(^|/)types\.lock$' \
     -e '(^|/)\.mzprofile$' \
+    -e '(^|/)lean-toolchain$' \
     -e '^src/mz-deploy/src/cli/scaffold/gitignore$' \
     -e '^test/mz-deploy/projects/multi-profile/v1/models/app/core/ambiguous\.sql$' \
     -e '^about\.toml$' \

ci/test/pipeline.template.yml

@@ -668,6 +668,21 @@ steps:
     agents:
       queue: hetzner-aarch64-4cpu-8gb
 
+  - id: lean
+    label: Lean models
+    depends_on: build-aarch64
+    timeout_in_minutes: 30
+    # Design doc models live outside the composition directory. A git
+    # pathspec `*` also matches `/`, so this covers every subdirectory.
+    inputs: ["doc/developer/design/*.lean"]
+    plugins:
+      - ./ci/plugins/mzcompose:
+          composition: lean
+    agents:
+      queue: hetzner-aarch64-4cpu-8gb
+    coverage: skip
+    sanitizer: skip
+
   - id: mcp
     label: MCP e2e
     depends_on: build-aarch64

doc/developer/design/README.md

@@ -126,6 +126,11 @@ your thinking and inform the writing process.
    of stakeholders. Note that we have a bot that automatically posts
    notifications about new design documents in #rnd-design-docs.
 
+A design document can carry a Lean 4 model that CI checks. Put the document
+in its own date-prefixed directory and the model's `.lean` files next to it.
+See [`misc/lean/README.md`](../../../misc/lean/README.md) for how the models
+are built.
+
 ### Iteration
 
 6. As you begin to get feedback on your document, address the comments

misc/images/lean/.gitignore

@@ -0,0 +1,3 @@
+/lean-toolchain
+/lakefile.lean
+/lake-manifest.json

misc/images/lean/Dockerfile

@@ -0,0 +1,78 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+# Lean 4 toolchain for the Lake project in `misc/lean`. The toolchain comes
+# from that project's `lean-toolchain`, so a local elan install and this image
+# use the same Lean version. The project's dependencies are built into
+# `/mz/misc/lean/.lake` at image build time. The project sits at its
+# repository path because `lakefile.lean` finds design doc models relative to
+# itself, in `/mz/doc/developer/design`.
+
+MZFROM debian-base
+
+ARG ELAN_VERSION=v4.2.4
+
+ENV ELAN_HOME=/opt/elan
+ENV PATH=$ELAN_HOME/bin:$PATH
+
+RUN apt-get update \
+    && TZ=UTC DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \
+        ca-certificates \
+        curl \
+        git \
+        jq \
+    && apt-get clean \
+    && rm -rf /var/lib/apt/lists/*
+
+COPY lean-toolchain /mz/misc/lean/
+
+# NOTE: the toolchain is kept whole although checking proofs needs only part of
+# it. Batteries, a dependency of Aesop and Mathlib, has the `runLinter`
+# executable among its default targets. Linking it needs the toolchain's static
+# libraries and LLVM, so removing them breaks the dependency build below.
+RUN case "$(uname -m)" in \
+        x86_64) triple=x86_64-unknown-linux-gnu; sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 ;; \
+        aarch64) triple=aarch64-unknown-linux-gnu; sha256=05febd124d84ebf994b2e7479922a5650b1e950c17ae3bd1ddd776b65bb72bf9 ;; \
+        *) echo "unsupported architecture $(uname -m)" >&2; exit 1 ;; \
+    esac \
+    && curl -fsSL -o /tmp/elan.tar.gz \
+        "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/elan-$triple.tar.gz" \
+    && echo "$sha256  /tmp/elan.tar.gz" | sha256sum -c - \
+    && tar -C /tmp -xzf /tmp/elan.tar.gz \
+    && /tmp/elan-init -y --no-modify-path --default-toolchain "$(cat /mz/misc/lean/lean-toolchain)" \
+    && rm /tmp/elan.tar.gz /tmp/elan-init \
+    && elan toolchain install "$(cat /mz/misc/lean/lean-toolchain)" \
+    && chmod -R a+rX "$ELAN_HOME" \
+    && lean --version
+
+# Git refuses repositories owned by a different uid than the one running it,
+# and Lake then re-clones the baked dependencies.
+RUN git config --system --add safe.directory '*'
+
+WORKDIR /mz/misc/lean
+
+COPY lakefile.lean lake-manifest.json /mz/misc/lean/
+
+# Builds the dependency closure. Building the placeholder library alone only
+# clones the dependencies, because Lake compiles just the modules a target
+# imports, so each package's default targets are built by name. NOTE: a
+# package that declares no default targets builds nothing here and compiles
+# on every run instead. One `lake build` for all packages fails if any of them
+# fails. With no dependencies it builds the placeholder.
+RUN mkdir Mz \
+    && touch Mz.lean \
+    && targets="$(jq -r '.packages[] | "@" + .name' lake-manifest.json)" \
+    && lake build $targets \
+    && rm -rf Mz Mz.lean .lake/build \
+    && chmod -R a+rwX /mz/misc/lean
+
+COPY mz-lake /usr/local/bin/
+
+ENTRYPOINT ["mz-lake"]
+CMD ["build"]

misc/images/lean/mz-lake

@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# mz-lake: copy the Lake project mounted at /src into /mz/misc/lean and run
+# `lake` there with the given arguments. Design doc models are read from
+# /mz/doc/developer/design, which mirrors the repository layout that
+# `lakefile.lean` expects.
+
+set -euo pipefail
+
+# Mounting the project over /mz/misc/lean would hide its .lake, which holds the
+# dependency closure built into the image. The host's own .lake is skipped for
+# the same reason. The entries are copied one by one because copying `.` itself
+# makes a non-root user try to change the mode and mtime of the root-owned
+# project directory, which fails.
+cd /src
+find . -mindepth 1 -maxdepth 1 ! -name .lake -exec cp -R -t /mz/misc/lean {} +
+
+cd /mz/misc/lean
+# The image build cached a configuration elaborated without any design doc
+# models. `-R` elaborates `lakefile.lean` again so it finds them.
+exec lake -R "$@"

misc/images/lean/mzbuild.yml

@@ -0,0 +1,26 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+name: lean
+description: Lean 4 toolchain and dependency closure for the models in misc/lean.
+# Only the files that pin the toolchain and the dependencies are copied, so
+# editing a model does not change the image fingerprint.
+pre-image:
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lean-toolchain
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lakefile.lean
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lake-manifest.json

misc/lean/.gitignore

@@ -0,0 +1 @@
+/.lake

misc/lean/Mz.lean

@@ -0,0 +1,10 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+
+import Mz.Collection