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

chore: basic dev instructions for Claude (#11074)

Browse source 
This PR adds a `.claude/claude.md`, with basic development instructions
for Claude Code to operate in this repository.
This commit is contained in:
Kim Morrison 2025-11-04 15:07:53 +11:00 • committed by GitHub
parent e4fb780f8a
commit 04d72fe346
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
.claude/CLAUDE.md Normal file
View file

@ -0,0 +1,14 @@
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`.
To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
*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.
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.
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.