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

doc: document nightly infrastructure in release command (#12129)

Browse source 
This PR adds documentation about the nightly build infrastructure to the
`/release` command to help future release managers understand the
relationship between branches and tags:

- `nightly` and `nightly-with-mathlib` are **branches** in
`leanprover/lean4`
- Dated tags like `nightly-YYYY-MM-DD` are **tags** in
`leanprover/lean4-nightly`
- When a nightly succeeds with mathlib, all three should point to the
same commit

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison 2026-01-24 11:06:44 +11:00 • committed by GitHub
parent c9facc8102
commit 88823b27a6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
.claude/commands/release.md
View file

@ -61,6 +61,15 @@ Every time you run `release_checklist.py`, you MUST:
This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
The user needs to see the complete picture of what's waiting for review.
## Nightly Infrastructure
The nightly build system uses branches and tags across two repositories:
- `leanprover/lean4` has **branches** `nightly` and `nightly-with-mathlib` tracking the latest nightly builds
- `leanprover/lean4-nightly` has **dated tags** like `nightly-2026-01-23`
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.
## Error Handling
**CRITICAL**: If something goes wrong or a command fails: