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

Revert "doc: add changelog label instructions to CLAUDE.md"

Browse source 
This reverts commit 119533d602.
This commit is contained in:
Kim Morrison 2026-01-29 03:16:10 +00:00
parent 119533d602
commit e441ed8e46
1 changed files with 0 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
.claude/CLAUDE.md
View file

@ -46,21 +46,6 @@ This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
leading quantifiers are stripped when creating a pattern.
```
**Changelog labels:** Add one `changelog-*` label to categorize the PR for release notes:
- `changelog-language` - Language features and metaprograms
- `changelog-tactics` - User facing tactics
- `changelog-server` - Language server, widgets, and IDE extensions
- `changelog-pp` - Pretty printing
- `changelog-library` - Library
- `changelog-compiler` - Compiler, runtime, and FFI
- `changelog-lake` - Lake
- `changelog-doc` - Documentation
- `changelog-ffi` - FFI changes
- `changelog-other` - Other changes
- `changelog-no` - Do not include this PR in the release changelog
If you're unsure which label applies, it's fine to omit the label and let reviewers add it.
## CI Log Retrieval
When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.