allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-30 17:16:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: update test matrix — C1 FAIL, C2 PARTIAL (HCMR builds, rest fail)

Browse source 
Lake build results (run 019f2f3f, 24min, 8 vCPUs):
- HCMR.lean: BUILT ✅ (agent fix worked — removed excess omega,
  downgraded false theorem from > to ≥)
- CacheSieve.lean: FAILED ❌ (agent fix incomplete — still has errors)
- Blitter6502OISC.lean: FAILED ❌ (type class synthesis L62,
  rewrite failures L135/L142)
- YangMillsPerformance.lean: FAILED ❌ (10 errors — omega/linarith
  can't handle Nat.div, 1 sorry)
- WorkloadTestbench.lean: NOT REACHED (depends on failed CacheSieve)
- CRTSidonN.lean: FAILED ❌ (errors after agent fix)

Root causes:
- YangMills: proofs use omega/linarith for Nat.div goals (wrong tactic)
- Blitter: type class instance missing, rw patterns don't match
- CacheSieve: agent fix didn't fully resolve all issues
- CRTSidonN: compilation errors remain

For future builds: add 'lake exe cache get' before 'lake build' to
download precompiled Mathlib oleans (saves ~20min).
This commit is contained in:
openresearch 2026-07-04 22:55:02 +00:00
parent 2f0328602f
commit e5cecac388
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
docs/research/COMPLETE_TEST_MATRIX.md
View file

@ -103,8 +103,8 @@ For each component of the framework, we ask:
| Test | Question | Input | Prediction | Receipt | Status |
|------|----------|-------|------------|---------|--------|
| T35 | Does CRTSidonN compile? | lake build | exit 0 | C1 | PENDING (build at 89%) |
| T36 | Does HCMR suite compile? | lake build | exit 0, 2 sorries | C2 | PENDING (same build) |
| T35 | Does CRTSidonN compile? | lake build | exit 0 | C1 | DONE: FAIL ❌ (errors after agent fix) |
| T36 | Does HCMR suite compile? | lake build | exit 0, 2 sorries | C2 | DONE: PARTIAL — HCMR ✅, CacheSieve ❌, Blitter ❌, YangMills ❌, WorkloadTestbench not reached |
| T37 | Are the proven theorems non-tautological? | Review each proof | At least sidon_preserved_mod is non-trivial | Adversarial review | DONE: sidon_preserved (componentwise) is tautological, sidon_preserved_mod is real |
| T38 | Does native_decide use violate AGENTS.md? | helical_coverage_74 | Uses native_decide | HopfFibration.lean | DONE: YES, uses native_decide (documented exception for finite decidability) |