From f3cbdca6e2f218150f134a414b5ae26f3167a059 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 18 Feb 2026 11:57:20 +1100
Subject: [PATCH] chore: add module/prelude guidance to CLAUDE.md (#12542)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 .claude/CLAUDE.md | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 58a8b9cfdf..78007fe938 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -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.