# CI And Releases

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

- Skill: `majiayu000/ci-and-releases` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds add majiayu000/ci-and-releases`
- Raw SKILL.md: https://api.skillmd.com/api/skills/majiayu000/ci-and-releases/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: majiayu000 (https://skillmd.com/u/majiayu000)
- Updated: 2026-09-09
- Page: https://skillmd.com/skills/majiayu000/ci-and-releases

---


# 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/`):

```powershell
.\lake.cmd build
.\lake.cmd exe computational_paths
```

If you suspect stale artifacts:

```powershell
.\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