菜单
A lightweight checklist for CI, toolchain bumps, and version/release hygiene for the ComputationalPaths Lean 4 project (Lake + lean-action CI).
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Review armada/fleet-generated Lean files for ComputationalPaths invariants, duplicate modules, shallow Path usage, and scaffold-heavy theorem stubs.
Design domain-specific Step types and rewrite certificates in ComputationalPaths modules without confusing them with core Path.Step rewrite rules.
Audit and harden scaffold-heavy ComputationalPaths Lean modules by replacing selected True/trivial/rfl placeholders with typed Path/RwEq certificate records while preserving public APIs.
Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence.
Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.
Run Aristotle automated theorem prover on Lean files to fill sorry placeholders. Use when you have a file with sorries that needs automated proof search. Handles API setup, axiom import checks, and result verification.
| name | ci-and-releases |
| description | A lightweight checklist for CI, toolchain bumps, and version/release hygiene for the ComputationalPaths Lean 4 project (Lake + lean-action CI). |
# Build
lake build
# Run executable
lake exe computational_paths
# Clean rebuild
lake clean && lake build
ComputationalPaths/Basic.lean (libraryVersion)lean-toolchainlake update if dependencies need repinningGitHub Actions uses leanprover/lean-action@v1:
# .github/workflows/lean_action_ci.yml
name: Lean Action CI
on: [push, pull_request, workflow_dispatch]
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: leanprover/lean-action@v1