Skip to content

generated-files.md

Latest commit

 

History

History
68 lines (51 loc) · 3.66 KB

generated-files.md

File metadata and controls

68 lines (51 loc) · 3.66 KB
Raw

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. Emitted in module form: module, blank line, one public import per file.
CompPoly/Fields/*/Ext*/*CertData.lean Generated and committed Rabin irreducibility certificate data for non-binomial extension moduli. Regenerate with scripts/gen_rabin_certificate.py --p <p> --f <coeffs> --lean <path> --namespace <NS>; the exact command is recorded in each file's docstring. Do not hand-edit. Nothing in them is trusted — the kernel re-checks every step through CompPoly.RabinCert.runChain.
bench/report-*.md, bench/results-*.jsonl, bench/evaluation-bench-* Generated, not source Produced by lake exe CompPolyBench; keep reports as local or CI artifacts. All three patterns are ignored — the first two by bench/.gitignore, evaluation-bench-* by the root .gitignore — so a benchmark run leaves the working tree clean.
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.

CompPoly.lean

../../CompPoly.lean is generated from tracked source files by ../../scripts/update-lib.sh.

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.

Rabin Certificate Data

CompPoly/Fields/KoalaBear/Ext5/QuinticCertData.lean and CompPoly/Fields/KoalaBear/Ext6/SexticCertData.lean are emitted verbatim by ../../scripts/gen_rabin_certificate.py. The generator writes a complete, compilable module — header, docstring with the regenerating command, and the step lists — so the workflow after changing a modulus is:

python3 scripts/gen_rabin_certificate.py --p <prime> --f <little-endian coeffs> \
    --lean <path to CertData.lean> --namespace <Field>.<Name>Cert
./scripts/update-lib.sh

The generator's exit code is its verdict: non-zero means the polynomial is reducible. Run python3 scripts/gen_rabin_certificate.py --self-test to check the generator itself against known-answer cases before trusting a new certificate.

Regenerating an unchanged modulus is byte-identical, so these files are safe to re-emit as a consistency check.

Derived Build State

  • .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.

Documentation Compatibility Files

  • 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.