Generated Files

This page records which paths are source of truth and which are derived outputs.

Source Of Truth Table

Path	Status	How it is maintained
`CompPoly.lean`	Generated and committed	Regenerate with `./scripts/update-lib.sh` after adding, renaming, or deleting `CompPoly/*/.lean` files.
`bench/report-.md`, `bench/results-.jsonl`	Generated, not source	Produced by `lake exe CompPolyBench`; keep reports as local or CI artifacts.
`CLAUDE.md`	Compatibility symlink	Must remain a symlink to `AGENTS.md`; do not replace it with a separate copy.
`.lake/`	Derived, not source	Local dependency cache and build output produced by Lake. Do not edit files here by hand.
`.lake/build/`	Derived, not source	Build artifacts from `lake build` and `lake test`. Safe to delete and regenerate.

Use this workflow whenever the source tree changes:

./scripts/update-lib.sh
./scripts/check-imports.sh

Do not hand-edit CompPoly.lean; any manual edits will be overwritten the next time the script runs.

.lake/ and .lake/build/ are generated by Lake and CI.
bench/results-*.jsonl and bench/report-*.md are generated benchmark outputs.
Build-timing reports and timing-data artifacts produced by ../../scripts/build_timing_report.sh are CI artifacts, not committed repo state.
When debugging stale build issues, deleting .lake/build/ and rebuilding resets local build artifacts. Do not commit changes from that directory.

AGENTS.md is canonical for agent-oriented tooling.
CLAUDE.md exists only so tooling that looks for that filename lands on the same content.
python3 ./scripts/check-docs-integrity.py is the enforcement point for the symlink and for local markdown links across the handbook.