Skip to content

Commit 9bfca43

Browse files
morlutomorluto
committed
feat(containers): publish pinned Lean evaluation images
1 parent 3097458 commit 9bfca43

4 files changed

Lines changed: 237 additions & 0 deletions

File tree

‎.github/workflows/lean-images.yml‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
name: Lean Evaluation Images
2+
3+
on:
4+
pull_request:
5+
branches: [main]
6+
paths:
7+
- "containers/lean-checker/**"
8+
- "containers/lean-repl-agent/**"
9+
- ".github/workflows/lean-images.yml"
10+
push:
11+
branches: [main]
12+
paths:
13+
- "containers/lean-checker/**"
14+
- "containers/lean-repl-agent/**"
15+
- ".github/workflows/lean-images.yml"
16+
workflow_dispatch:
17+
18+
concurrency:
19+
group: lean-images-${{ github.workflow }}-${{ github.ref }}
20+
cancel-in-progress: ${{ github.event_name == 'pull_request' }}
21+
22+
permissions:
23+
contents: read
24+
25+
env:
26+
REGISTRY: ghcr.io
27+
PLATFORM: linux/amd64
28+
29+
jobs:
30+
build-pr:
31+
name: Build ${{ matrix.image }}
32+
if: github.event_name == 'pull_request'
33+
runs-on: ubuntu-latest
34+
timeout-minutes: 30
35+
strategy:
36+
fail-fast: false
37+
matrix:
38+
image: [jacobian-lean-checker, jacobian-lean-repl-agent]
39+
steps:
40+
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
41+
with:
42+
persist-credentials: false
43+
- uses: docker/setup-buildx-action@bb05f3f5519dd87d3ba754cc423b652a5edd6d2c # v4
44+
- name: Build and load image for measurement
45+
uses: docker/build-push-action@53b7df96c91f9c12dcc8a07bcb9ccacbed38856a # v7
46+
with:
47+
context: .
48+
file: containers/${{ matrix.image }}/Dockerfile
49+
platforms: ${{ env.PLATFORM }}
50+
load: true
51+
push: false
52+
tags: local/${{ matrix.image }}:${{ github.sha }}
53+
cache-from: type=gha,scope=${{ matrix.image }}
54+
cache-to: type=gha,mode=max,scope=${{ matrix.image }}
55+
- name: Record unpacked image size
56+
env:
57+
IMAGE: local/${{ matrix.image }}:${{ github.sha }}
58+
run: |
59+
bytes=$(docker image inspect "$IMAGE" --format '{{.Size}}')
60+
jq -n \
61+
--arg image "$IMAGE" \
62+
--arg source_sha "$GITHUB_SHA" \
63+
--arg platform "$PLATFORM" \
64+
--argjson unpacked_size_bytes "$bytes" \
65+
'{image: $image, source_sha: $source_sha, platform: $platform, unpacked_size_bytes: $unpacked_size_bytes}' \
66+
| tee "$RUNNER_TEMP/${{ matrix.image }}-size.json" \
67+
>> "$GITHUB_STEP_SUMMARY"
68+
- name: Upload size evidence
69+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
70+
with:
71+
name: ${{ matrix.image }}-size-${{ github.sha }}
72+
path: ${{ runner.temp }}/${{ matrix.image }}-size.json
73+
if-no-files-found: error
74+
retention-days: 90
75+
76+
publish:
77+
name: Publish ${{ matrix.image }}
78+
if: github.event_name == 'push'
79+
runs-on: ubuntu-latest
80+
timeout-minutes: 30
81+
permissions:
82+
contents: read
83+
packages: write
84+
strategy:
85+
fail-fast: false
86+
matrix:
87+
image: [jacobian-lean-checker, jacobian-lean-repl-agent]
88+
steps:
89+
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
90+
with:
91+
persist-credentials: false
92+
- uses: docker/setup-buildx-action@bb05f3f5519dd87d3ba754cc423b652a5edd6d2c # v4
93+
- name: Log in to GHCR
94+
uses: docker/login-action@dbcb813823bdd20940b903addbd779551569679f # v4
95+
with:
96+
registry: ${{ env.REGISTRY }}
97+
username: ${{ github.actor }}
98+
password: ${{ secrets.GITHUB_TOKEN }}
99+
- id: meta
100+
uses: docker/metadata-action@dc802804100637a589fabce1cb79ff13a1411302 # v6
101+
with:
102+
images: ${{ env.REGISTRY }}/${{ github.repository_owner }}/${{ matrix.image }}
103+
tags: |
104+
type=raw,value=sha-${{ github.sha }}
105+
type=raw,value=main
106+
labels: |
107+
org.opencontainers.image.revision=${{ github.sha }}
108+
io.jacobian.source-dirty=false
109+
- id: build
110+
name: Build and publish
111+
uses: docker/build-push-action@53b7df96c91f9c12dcc8a07bcb9ccacbed38856a # v7
112+
with:
113+
context: .
114+
file: containers/${{ matrix.image }}/Dockerfile
115+
platforms: ${{ env.PLATFORM }}
116+
push: true
117+
tags: ${{ steps.meta.outputs.tags }}
118+
labels: ${{ steps.meta.outputs.labels }}
119+
cache-from: type=gha,scope=${{ matrix.image }}
120+
cache-to: type=gha,mode=max,scope=${{ matrix.image }}
121+
provenance: mode=max
122+
sbom: true
123+
- name: Record digest and unpacked size
124+
env:
125+
IMAGE: ${{ env.REGISTRY }}/${{ github.repository_owner }}/${{ matrix.image }}
126+
DIGEST: ${{ steps.build.outputs.digest }}
127+
run: |
128+
docker pull "$IMAGE@$DIGEST"
129+
size=$(docker image inspect "$IMAGE@$DIGEST" --format '{{.Size}}')
130+
jq -n \
131+
--arg source_sha "$GITHUB_SHA" \
132+
--arg image "$IMAGE@$DIGEST" \
133+
--arg image_digest "$DIGEST" \
134+
--arg platform "$PLATFORM" \
135+
--argjson unpacked_size_bytes "$size" \
136+
'{source_sha: $source_sha, image: $image, image_digest: $image_digest, platform: $platform, unpacked_size_bytes: $unpacked_size_bytes}' \
137+
| tee "$RUNNER_TEMP/${{ matrix.image }}-publication.json" \
138+
>> "$GITHUB_STEP_SUMMARY"
139+
- name: Upload publication evidence
140+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
141+
with:
142+
name: ${{ matrix.image }}-publication-${{ github.sha }}
143+
path: ${{ runner.temp }}/${{ matrix.image }}-publication.json
144+
if-no-files-found: error
145+
retention-days: 90

‎containers/README.md‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
# Reusable evaluation runtimes
2+
3+
These images separate an agent/provider's exploratory toolchain from a
4+
verifier's authority to replay a submitted mathematical artifact.
5+
6+
| Image | Purpose | Must not contain |
7+
| --- | --- | --- |
8+
| `jacobian-lean-checker` | Compile and inspect submitted Lean source in a clean verifier. | Task solution, task-specific expected output, or the REPL. |
9+
| `jacobian-lean-repl-agent` | Run the pinned Lean REPL for provider-feasibility and agent environments. | Authority to certify a report as independently verified. |
10+
11+
The release workflow publishes both images to GHCR after a trusted `main` push.
12+
It emits immutable commit tags, an OCI digest, SBOM, provenance, and a size
13+
receipt. A Harbor task must pin the resulting `@sha256:` reference in its
14+
environment profile or task Dockerfile. Tags are discovery conveniences, not
15+
evaluation identity.
16+
17+
The checker image is intentionally Lean-only. A future task that genuinely
18+
requires Mathlib must use a separately measured and published runtime; adding
19+
Mathlib to this base would impose its multi-gigabyte footprint on every Lean
20+
source replay.

‎containers/lean-checker/Dockerfile‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#
2+
# A deliberately small trusted runtime for Harbor verifiers that replay Lean
3+
# source. It contains Lean's kernel/compiler, but neither task material nor an
4+
# agent-facing REPL. Tasks must consume a published digest, never a tag.
5+
FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de
6+
7+
ARG LEAN_VERSION=4.31.0
8+
ARG LEAN_ARCHIVE_SHA256=07a633cc8d9151cbc08825ea4cdda50d4b02a2c9cb852c0131b13046f49cad7f
9+
10+
LABEL org.opencontainers.image.source=https://github.com/morluto/jacobian
11+
LABEL org.opencontainers.image.description="Pinned Lean compiler for independent Jacobian verifier replay"
12+
LABEL io.jacobian.lean.version=${LEAN_VERSION}
13+
LABEL io.jacobian.lean.archive-sha256=${LEAN_ARCHIVE_SHA256}
14+
15+
RUN apt-get update \
16+
&& apt-get install -y --no-install-recommends ca-certificates curl libgmp10 zstd \
17+
&& rm -rf /var/lib/apt/lists/* \
18+
&& mkdir -p /opt/lean \
19+
&& curl -fsSL "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/lean-${LEAN_VERSION}-linux.tar.zst" \
20+
-o /opt/lean/lean.tar.zst \
21+
&& printf '%s %s\n' "$LEAN_ARCHIVE_SHA256" /opt/lean/lean.tar.zst | sha256sum -c - \
22+
&& tar --use-compress-program=unzstd -xf /opt/lean/lean.tar.zst -C /opt/lean \
23+
&& rm /opt/lean/lean.tar.zst \
24+
&& /opt/lean/lean-${LEAN_VERSION}-linux/bin/lean --version \
25+
&& python -m pip install --no-cache-dir \
26+
attrs==26.1.0 \
27+
jsonschema==4.26.0 \
28+
jsonschema-specifications==2025.9.1 \
29+
referencing==0.37.0 \
30+
rpds-py==2026.6.3 \
31+
typing-extensions==4.16.0
32+
33+
ENV PATH=/opt/lean/lean-4.31.0-linux/bin:$PATH
34+
ENV PYTHONDONTWRITEBYTECODE=1
35+
36+
WORKDIR /app

‎containers/lean-repl-agent/Dockerfile‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#
2+
# This is an agent/provider runtime. It intentionally remains distinct from
3+
# lean-checker: REPL telemetry is not independent verification evidence.
4+
FROM ghcr.io/astral-sh/uv:0.8.4-python3.12-bookworm-slim@sha256:dc7e1d08f8ca979826ec0b68b31c783e0b35b568be6a078d4cbedf38c4cc085e
5+
6+
ARG LEAN_VERSION=4.31.0
7+
ARG LEAN_ARCHIVE_SHA256=07a633cc8d9151cbc08825ea4cdda50d4b02a2c9cb852c0131b13046f49cad7f
8+
ARG LEAN_REPL_REVISION=0cc60263319308000bbaa5354427f775fe3dc7d0
9+
10+
LABEL org.opencontainers.image.source=https://github.com/morluto/jacobian
11+
LABEL org.opencontainers.image.description="Pinned Lean REPL runtime for Jacobian provider-feasibility tasks"
12+
LABEL io.jacobian.lean.version=${LEAN_VERSION}
13+
LABEL io.jacobian.lean.archive-sha256=${LEAN_ARCHIVE_SHA256}
14+
LABEL io.jacobian.lean-repl.revision=${LEAN_REPL_REVISION}
15+
16+
RUN apt-get update \
17+
&& apt-get install -y --no-install-recommends ca-certificates curl git libgmp10 zstd \
18+
&& rm -rf /var/lib/apt/lists/* \
19+
&& mkdir -p /opt/provider \
20+
&& curl -fsSL "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/lean-${LEAN_VERSION}-linux.tar.zst" \
21+
-o /opt/provider/lean.tar.zst \
22+
&& printf '%s %s\n' "$LEAN_ARCHIVE_SHA256" /opt/provider/lean.tar.zst | sha256sum -c - \
23+
&& tar --use-compress-program=unzstd -xf /opt/provider/lean.tar.zst -C /opt/provider \
24+
&& rm /opt/provider/lean.tar.zst \
25+
&& git init /opt/provider/repl \
26+
&& git -C /opt/provider/repl remote add origin https://github.com/leanprover-community/repl.git \
27+
&& git -C /opt/provider/repl fetch --depth 1 origin "$LEAN_REPL_REVISION" \
28+
&& git -C /opt/provider/repl checkout --detach FETCH_HEAD \
29+
&& PATH=/opt/provider/lean-${LEAN_VERSION}-linux/bin:$PATH lake -d /opt/provider/repl build \
30+
&& /opt/provider/lean-${LEAN_VERSION}-linux/bin/lean --version
31+
32+
ENV PATH=/opt/provider/lean-4.31.0-linux/bin:$PATH
33+
ENV PYTHONDONTWRITEBYTECODE=1
34+
ENV PYTHONPATH=/opt
35+
36+
WORKDIR /app

0 commit comments

Comments
 (0)