Spaces:
Running
Running
Commit History
-
fix(drift-heal): sync corpus/formulas/a11oy__gates_manifest.json to GitHub canonical (lean_commit_sha b675cd84)
Verified signatureHeal GitHub<->HF module drift: the live HF Space served the stale gates_manifest (older lean_commit_sha 1dca0003). GitHub HEAD is canonical (source-of-truth built by Dockerfile COPY; regenerated manifest references the newer lutar-lean commit b675cd84). Pushing GitHub bytes byte-identical (valid JSON, same 53529 bytes). a11oy-specific corpus artifact (not a killinchu shared module), so cross-organ byte-identity unaffected.04dddc7
-
sync(hf): mirror corpus theorem-runtime-manifest doctrine fix to live Space (additive)
Verified signatureFollow-on to the GitHub doctrine fix: the corpus/ in-image mirror manifest was updated on GitHub (honest Lambda-monotonicity vs Conjecture-1 uniqueness wording, b675cd84 lean pins). corpus/ is Dockerfile-COPY'd so the HF module-drift guard compares it; mirror GitHub->Space byte-identical so GitHub==Space.638a721 -
fix(citations): repoint 7 phantom proofs to real Lean (task #938)
Verified signatureA2/A3/A6/T2/T7/TH1/T8 repointed from Lutar/Gate/* to real lutar-lean decls; corpus mirror in lockstep; 20 stay honestly phantom.9b8541f
-
chore(sync): mirror backend .py + Dockerfile to Space (hf-sync-backend)
Verified signatureAutomated backend sync from szl-holdings/a11oy main via hf-sync-backend. Updated (differed from the Space): corpus/formulas/a11oy__szl_formula_wiring.py Deleted (gone from the repo + Dockerfile COPY set): (none) Keeps the Space-built backend (serve.py + the Dockerfile-COPY'd .py modules) identical to GitHub main so the Space never rebuilds from a stale backend, new endpoints don't 404 there, and orphaned modules removed from the repo don't linger in the Space tree.e7c45ca -
chore(sync): mirror backend .py + Dockerfile to Space (hf-sync-backend)
Verified signatureAutomated backend sync from szl-holdings/a11oy main via hf-sync-backend. Updated (differed from the Space): corpus/formulas/a11oy__szl_formulas.py Deleted (gone from the repo + Dockerfile COPY set): (none) Keeps the Space-built backend (serve.py + the Dockerfile-COPY'd .py modules) identical to GitHub main so the Space never rebuilds from a stale backend, new endpoints don't 404 there, and orphaned modules removed from the repo don't linger in the Space tree.8c6af52
-
Task #695: relabel phantom Lean citations in theorem-runtime-manifest (md5 parity w/ GitHub)
Verified signature27 relabeled phantom, 1 repointed to Lutar/Bound.lean, +leanCitationAuditf374b2e
-
fix(org-rag): in-image corpus mirror for GitHub-only categories (egress fix)
Verified signatureIn-image corpus mirror for the 4 GitHub-only org-RAG categories (egress fix). a11oy_org_rag.py kept byte-identical with the GitHub copy; corpus files trace to real GitHub blob_sha/commit_sha via corpus/INDEX.json.545c5f9 -
chore(sync): mirror backend .py + Dockerfile to Space (hf-sync-backend)
Verified signatureAutomated backend sync from szl-holdings/a11oy main via hf-sync-backend. Updated (differed from the Space): Dockerfile, a11oy_org_rag.py, corpus/formulas/a11oy__a11oy_v4_formulas.py, corpus/formulas/a11oy__szl_formula_wiring.py, corpus/formulas/a11oy__szl_formulas.py, corpus/formulas/a11oy__szl_puriq_formulas.py Keeps the Space-built backend (serve.py + the Dockerfile-COPY'd .py modules) identical to GitHub main so the Space never rebuilds from a stale backend and new endpoints don't 404 there.7d695cb