CI & Releases

This skill provides a repeatable checklist for keeping the repo green on CI and preparing small “release-like” changes (toolchain bump, version bump, dependency updates).

CI mental model

CI is essentially “clean checkout + lake build”. Keep changes compatible with:

• current toolchain in lean-toolchain
• dependencies pinned by lake-manifest.json
• the project’s “zero-warning” expectations (treat warnings as failures to fix immediately)

Local verification (Windows)

From the Lean project root (computational_paths/):

.\lake.cmd build
.\lake.cmd exe computational_paths

If you suspect stale artifacts:

.\lake.cmd clean
.\lake.cmd build

Version bump checklist

This repo exposes a version string:

• ComputationalPaths/Basic.lean defines libraryVersion
• Main.lean prints it via the executable

When bumping version:

1. Update ComputationalPaths/Basic.lean (libraryVersion)
2. Run .\lake.cmd build
3. Run .\lake.cmd exe computational_paths and confirm the output
4. If the bump is user-visible, update README.md (or add a short changelog note)

Toolchain bump checklist

When updating lean-toolchain:

1. Edit lean-toolchain
2. Run .\lake.cmd build
3. If dependencies need repinning, run lake update and re-build
4. Ensure CI config still matches expectations (.github/workflows/*)

Dependency update checklist

If updating deps (manifest changes):

1. Run lake update
2. Build (.\lake.cmd build)
3. Fix any breakage by updating imports/lemmas or pinning versions back as needed