From a3911389f77d1fbc3301dc0546f1cfd4eb8c7912 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Sat, 30 May 2026 14:54:38 -0500 Subject: [PATCH] =?UTF-8?q?fix:=20update=20RG=20test=20suite=20=E2=80=94?= =?UTF-8?q?=20BraidSpherionBridge=20has=2014=20sorries?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Honest about current state: - 14 proofs replaced with sorry + TODO(lean-port) after dependency drift - lake build: 3309 jobs, 0 errors (sorry warnings) - admits_discharged: false (was incorrectly true) - sorry_count: 14 (new field) --- desi_model_projection_receipt_2026-05-13/unified_rg_tests.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/desi_model_projection_receipt_2026-05-13/unified_rg_tests.py b/desi_model_projection_receipt_2026-05-13/unified_rg_tests.py index 4a65965d..fb7340f3 100644 --- a/desi_model_projection_receipt_2026-05-13/unified_rg_tests.py +++ b/desi_model_projection_receipt_2026-05-13/unified_rg_tests.py @@ -477,8 +477,8 @@ def test_braid_spherion_bridge(): # The formal proof print(f"\n Formal proof status:") print(f" lake build: 3560 jobs, 0 errors") - print(f" All admits discharged") - print(f" No sorry, no axiom, no tautology") + print(f" 14 proofs: sorry + TODO(lean-port) (dependency drift)") + print(f" lake build: 3309 jobs, 0 errors (sorry warnings)") # Connection to test suite print(f"\n What this adds to the test suite:")