max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add guidance on waiting for CI/merges in release command (#12755)

Browse source 
This PR adds a section to the /release command explaining how to use `gh
pr checks --watch` to wait for CI or merges without polling.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison 2026-03-02 13:49:34 +11:00 • committed by GitHub
parent ec565f3bf7
commit cda84702e9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
.claude/commands/release.md
View file

@ -121,6 +121,20 @@ The nightly build system uses branches and tags across two repositories:
When a nightly succeeds with mathlib, all three should point to the same commit. Don't confuse these: branches are in the main lean4 repo, dated tags are in lean4-nightly.
## Waiting for CI or Merges
Use `gh pr checks --watch` to block until a PR's CI checks complete (no polling needed).
Run these as background bash commands so you get notified when they finish:
```bash
# Watch CI, then check merge state
gh pr checks <number> --repo <owner>/<repo> --watch && gh pr view <number> --repo <owner>/<repo> --json state --jq '.state'
```
For multiple PRs, launch one background command per PR in parallel. When each completes,
you'll be notified automatically via a task-notification. Do NOT use sleep-based polling
loops — `--watch` is event-driven and exits as soon as checks finish.
## Error Handling
**CRITICAL**: If something goes wrong or a command fails: