- Do not introduce
sorryin safety-critical modules. - Keep extraction and bindings aligned with canonical contracts.
- Prefer explicit errors over silent behavior changes.
- Keep changes small, testable, and evidence-backed.
Run this before opening a pull request:
python scripts/validate_local.pypython scripts/check_proof_completeness.pypython scripts/check_contract_consistency.pypython scripts/lake_doctor.pypython scripts/lake_resilient.py --attempts 3 --timeout 600 lake buildpython scripts/run_runtime_checks.py
- Describe reliability impact and operational risk.
- Include command output evidence for changed behavior.
- Update
docs/api.mdandREADME.mdif public behavior or guarantees change.