ci-and-releases

Arthur742Ramos's avatarfrom Arthur742Ramos

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 1, 2026⬇️1downloads
[CI and CD]

When & Why to Use This Skill

This Claude skill provides a specialized framework for managing Continuous Integration (CI) and release hygiene specifically for Lean 4 projects. It streamlines the process of toolchain upgrades, versioning, and dependency management using Lake and lean-action CI, ensuring repository stability and maintaining a 'zero-warning' code standard.

Use Cases

  • Automating version bumps: Systematically updating library versions in Lean files and verifying them via executable outputs.
  • Toolchain migration: Managing the transition to new Lean 4 toolchain versions while ensuring CI configuration compatibility.
  • Dependency management: Updating project dependencies using Lake, repinning manifests, and resolving build breakages.
  • Local build verification: Providing standardized procedures for cleaning and rebuilding Lean projects to ensure environment consistency.
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