Claude-skill-registry ci-and-releases

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

install

source · Clone the upstream repo

git clone https://github.com/majiayu000/claude-skill-registry

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/majiayu000/claude-skill-registry "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/data/ci-and-releases" ~/.claude/skills/majiayu000-claude-skill-registry-ci-and-releases && rm -rf "$T"

manifest: skills/data/ci-and-releases/SKILL.md

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:

Update

ComputationalPaths/Basic.lean

(

libraryVersion

)

Run
```
.\lake.cmd build
```
Run
```
.\lake.cmd exe computational_paths
```
and confirm the output
If the bump is user-visible, update
```
README.md
```
(or add a short changelog note)

Toolchain bump checklist

When updating

lean-toolchain

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

Dependency update checklist

If updating deps (manifest changes):

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