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

chore: update Claude prompting (#11370)

Browse source 
Co-authored-by: Claude <noreply@anthropic.com>
This commit is contained in:
Kim Morrison 2025-11-26 13:53:36 +11:00 • committed by GitHub
parent b68ac99d26
commit 387833be70
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 25 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
.claude/CLAUDE.md
View file

@ -1,14 +1,34 @@
To build Lean you should use `make -j -C build/release`.
To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
## New features
When asked to implement new features:
* begin by reviewing existing relevant code and tests
* write comprehensive tests first (expecting that these will initially fail)
* and then iterate on the implementation until the tests pass.
To build Lean you should use `make -j$(nproc) -C build/release`.
All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
## Success Criteria
*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass. You have to keep working until you have verified both of these.
*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
All new tests should go in `tests/lean/run/`. Note that these tests don't have expected output, and just run on a success or failure basis. So you should use `#guard_msgs` to check for specific messages.
## Build System Safety
If you are not following best practices specific to this repository and the user expresses frustration, stop and ask them to help update this `.claude/CLAUDE.md` file with the missing guidance.
**NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
- ONLY use the project's documented build command: `make -j -C build/release`
- If a build is broken, ask the user before attempting any manual cleanup
## LSP and IDE Diagnostics
After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
## Update prompting when the user is frustrated
If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
## Creating pull requests.
All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.