fix(ci/crypto/lfs): update ceremony rustfmt, differential test, LFS attributes, and workflow pins
Browse files- verify_release.py +0 -10
verify_release.py
CHANGED
|
@@ -254,16 +254,6 @@ def main() -> int:
|
|
| 254 |
# Step 5: Lean 4 Formal Mathematical Theorem Audit
|
| 255 |
print("\n[STEP 5/6] Auditing Lean 4 Formal Mathematical Theorem Proof...")
|
| 256 |
s5, lean_msg = verify_lean_theorem(root)
|
| 257 |
-
# If lean is not installed locally, check if lean4_theorem.json evidence exists from CI execution
|
| 258 |
-
lean_evidence = root / "evidence" / "10_00" / "latest" / "lean4_theorem.json"
|
| 259 |
-
if not s5 and lean_evidence.is_file():
|
| 260 |
-
try:
|
| 261 |
-
ev_data = json.loads(lean_evidence.read_text(encoding="utf-8"))
|
| 262 |
-
if ev_data.get("proof_valid") and ev_data.get("theorem") == "nullspace_orthogonality":
|
| 263 |
-
s5 = True
|
| 264 |
-
lean_msg = "Lean 4 Theorem Execution Evidence Verified (lean4_theorem.json)"
|
| 265 |
-
except Exception:
|
| 266 |
-
pass
|
| 267 |
print(f" -> Lean 4 Proof Status: {lean_msg} ({'PASS' if s5 else 'FAIL'})")
|
| 268 |
subsystem_results.append({"step": "formal_math_lean", "pass": s5, "message": lean_msg})
|
| 269 |
|
|
|
|
| 254 |
# Step 5: Lean 4 Formal Mathematical Theorem Audit
|
| 255 |
print("\n[STEP 5/6] Auditing Lean 4 Formal Mathematical Theorem Proof...")
|
| 256 |
s5, lean_msg = verify_lean_theorem(root)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 257 |
print(f" -> Lean 4 Proof Status: {lean_msg} ({'PASS' if s5 else 'FAIL'})")
|
| 258 |
subsystem_results.append({"step": "formal_math_lean", "pass": s5, "message": lean_msg})
|
| 259 |
|