ci-troubleshooting

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

CI Troubleshooting for FormalFrontier Book Repos

Prerequisites

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.lean
• lean-toolchain
• lake-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.

Diagnosing CI Failures

Step 1: Check the failure type

# Get the latest CI run for a PR
gh pr checks <PR-number>

# Get detailed run info
gh run view <run-id> --log-failed

Step 2: Classify the failure

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

Step 3: Infrastructure failures

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.

Step 4: After fixing

• Push the fix to the PR branch
• Wait for CI to run (check with gh pr checks <PR-number>)
• If auto-merge was enabled, it will merge once CI passes

Merge Conflicts on PRs

When coordination orient shows PRs with [CONFLICTS]:

1. Check if the conflict is trivial (e.g., progress/ files, items.json):

   gh pr view <N> --json mergeable,mergeStateStatus
   

2. If you're the PR author, rebase onto main:

   git fetch origin main
   git rebase origin/main
   # resolve conflicts
   git push --force-with-lease
   

3. If you're NOT the PR author, create a fix issue rather than force-pushing to someone else's branch.

Common Pitfalls

• Don't skip lake exe cache get: Without Mathlib cache, CI builds take 30+ minutes and often timeout.
• Don't assume CI failures are your fault: Check for infrastructure issues first (0-step runs, runner provisioning failures).
• Don't merge PRs with conflicts: Even if CI passed before conflicts appeared, the merged result may not compile.