mathesis-images

Builds the container images of Mathesis and publishes them to GitHub Packages under this organization. Mathesis itself only builds its images in CI and never pushes them, and the ChronoAI deployment with chrono-cd needs images on ghcr.io.

Nothing here changes the upstream code. The workflow checks out the upstream repository at a ref you choose and runs its own Dockerfiles from infra/.

Images

Image	Built from	Tag
ghcr.io/chronoaiproject/mathesis-web	infra/web/Dockerfile	upstream short commit, and latest
ghcr.io/chronoaiproject/mathesis-api	infra/api/Dockerfile (also runs as the worker)	upstream short commit, and latest
ghcr.io/chronoaiproject/mathesis-lean	infra/verifier/Lean.Dockerfile	hash of the Lean toolchain and lakefile pins
ghcr.io/chronoaiproject/mathesis-verifier	infra/verifier/Dockerfile	upstream short commit, and latest

Build

Run the build-images workflow from the Actions tab, or:

gh workflow run build-images --repo ChronoAIProject/mathesis-images -f ref=develop

ref is any upstream branch, tag or commit. The Lean base is rebuilt only when the upstream pins change. The verifier build runs the real Lean proof checks and takes up to an hour the first time.

Deploy

The chrono-cd app spec that uses these images lives in the chrono-cd repository under docs/examples/mathesis.yaml.