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/.
| 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 |
Run the build-images workflow from the Actions tab, or:
gh workflow run build-images --repo ChronoAIProject/mathesis-images -f ref=developref 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.
The chrono-cd app spec that uses these images lives in the chrono-cd repository under
docs/examples/mathesis.yaml.