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

chore: add module/prelude guidance to CLAUDE.md (#12542)

Browse source 
This PR adds guidance to `.claude/CLAUDE.md` about the `module` +
`prelude` convention required for files in `src/Lean/`, `src/Std/`, and
`src/lake/Lake/`. CI enforces that these files contain `prelude`, but
with `prelude` nothing is auto-imported, so explicit `Init.*` imports
are needed for standard library features like `while`,
`String.startsWith`, etc.

🤖 Prepared with Claude Code

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

15
.claude/CLAUDE.md
View file

@ -84,6 +84,21 @@ leading quantifiers are stripped when creating a pattern.
If you're unsure which label applies, it's fine to omit the label and let reviewers add it.
## Module System for `src/` Files
Files in `src/Lean/`, `src/Std/`, and `src/lake/Lake/` must have both `module` and `prelude` (CI enforces `^prelude$` on its own line). With `prelude`, nothing is auto-imported — you must explicitly import `Init.*` modules for standard library features. Check existing files in the same directory for the pattern, e.g.:
```lean
module
prelude
import Init.While -- needed for while/repeat
import Init.Data.String.TakeDrop -- needed for String.startsWith
public import Lean.Compiler.NameMangling -- public if types are used in public signatures
```
Files outside these directories (e.g. `tests/`, `script/`) use just `module`.
## 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.