ci-and-releases

majiayu000's avatarfrom majiayu000

A lightweight checklist for CI, toolchain bumps, and version/release hygiene for the ComputationalPaths Lean 4 project (Lake + lean-action CI).

⭐0stars🔀0forks📁View on GitHub🕐Updated Jan 5, 2026
[CI and CD]

When & Why to Use This Skill

This Claude skill provides a structured and repeatable framework for managing Continuous Integration (CI) and release cycles specifically for Lean 4 projects using Lake and lean-action CI. It optimizes repository health by providing standardized checklists for toolchain upgrades, versioning hygiene, and dependency management, ensuring a 'zero-warning' development environment.

Use Cases

  • Automating Release Hygiene: Streamline the process of bumping library versions and verifying executable outputs to maintain consistent release records.
  • Managing Toolchain Upgrades: Safely transition to new Lean 4 toolchain versions by following a step-by-step verification process that includes dependency re-pinning and CI configuration checks.
  • Local CI Verification: Perform pre-flight checks using Lake build commands to ensure code changes are compatible with the environment before pushing to the remote repository.
  • Dependency Synchronization: Efficiently update project manifests and resolve breaking changes in imports or lemmas after updating external dependencies.
nameci-and-releases
descriptionA lightweight checklist for CI, toolchain bumps, and version/release hygiene for the ComputationalPaths Lean 4 project (Lake + lean-action CI).

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