菜单
Use when CI fails on a PR, when debugging GitHub Actions failures, or when a PR is blocked by failing checks. Also use when planning work to fix broken PRs.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Use when deciding whether a formalized proof should delegate to Mathlib, when refactoring standalone proofs into Mathlib wrappers, or when reviewing delegation refactors for correctness.
Use when running Stage 3.4 (Proof Polishing) to bring sorry-free proofs to Mathlib quality. Use when assessing whether a proof needs cleanup, when working through proof-polish GitHub issues, or when deciding which tactic to prefer for a given goal.
Use when a Lean proof has failed 2-3 attempts and needs to be sent to Aristotle for automated proving, or when checking the status of a previously submitted Aristotle job.
Quantitative insights on formalization speed by item type and proof strategy. Use when estimating difficulty from textbook statements, planning batches, or predicting project timelines.
Use when filling sorry placeholders in Lean 4 proof files, when choosing between proof approaches for a FormalFrontier item, or when a proof attempt fails and you need an alternative strategy.
Use when searching for Mathlib declarations to fill a proof, when imports fail, when you need to find the right Mathlib module for a concept, or when exact? or apply? don't find what you need.
| name | ci-troubleshooting |
| description | Use when CI fails on a PR, when debugging GitHub Actions failures, or when a PR is blocked by failing checks. Also use when planning work to fix broken PRs. |
| allowed-tools | Bash, Read, Grep, Glob |
This project uses leanprover/lean-action@v1 for CI. The workflow is at
.github/workflows/lean_action.yml.
Required files in repo root (missing any of these causes CI failure):
lakefile.toml or lakefile.leanlean-toolchainlake-manifest.json (generated by lake update)If lake-manifest.json is missing, CI fails with:
No lake-manifest.json found. Run lake update to generate manifest
Fix: run lake update locally, commit lake-manifest.json.
# Get the latest CI run for a PR
gh pr checks <PR-number>
# Get detailed run info
gh run view <run-id> --log-failed
| Symptom | Cause | Fix |
|---|---|---|
| 0 steps executed, fails in <10s | GitHub Actions infrastructure issue | Rerun: gh run rerun <run-id> |
lake-manifest.json not found | Missing manifest | lake update, commit manifest |
lake build timeout | Mathlib cache miss | Ensure lake exe cache get runs before build |
| Lean compilation error | Code issue in PR | Fix the Lean code |
| Merge conflict marker | PR has conflicts | Rebase or merge main into branch |
GitHub Actions sometimes has runner issues where jobs complete with 0 steps. This is transient. Rerun with:
gh run rerun <run-id>
If it fails again after rerun, investigate the workflow file itself.
gh pr checks <PR-number>)When coordination orient shows PRs with [CONFLICTS]:
progress/ files, items.json):
gh pr view <N> --json mergeable,mergeStateStatus
git fetch origin main
git rebase origin/main
# resolve conflicts
git push --force-with-lease
lake exe cache get: Without Mathlib cache, CI builds
take 30+ minutes and often timeout.