Allaun Silverfox
0ee6563348
chore(pending): quarantine python MCP server (Lean-first unification)
2026-05-26 17:56:25 -05:00
Allaun Silverfox
6bd0eb4eb7
feat(runtime): register lean_mcp_manifest module
2026-05-26 17:50:05 -05:00
Allaun Silverfox
1da805783e
feat(runtime): source tools/list from Lean manifest env var when spec.tools empty
2026-05-26 17:49:55 -05:00
Allaun Silverfox
4ddc4e9800
feat(runtime): load MCP tools list from Lean manifest JSON (shim-only)
2026-05-26 17:42:33 -05:00
Allaun Silverfox
016d8b203d
feat(lean): define MCP surface manifest schema for JsonL connector tools
2026-05-26 17:32:55 -05:00
Allaun Silverfox
82964b7077
docs: add Lean-first boundary contract (Lean vs shims, receipts, float ban)
2026-05-26 17:31:54 -05:00
Allaun Silverfox
3b7f107dab
cleanup(ene): load node list from nodes.yaml instead of hardcoded hostnames
2026-05-26 17:16:02 -05:00
Allaun Silverfox
5f41114dcd
cleanup(ene): use nodes.yaml inventory instead of hardcoded host resource map
2026-05-26 17:15:50 -05:00
Allaun Silverfox
2391e8c385
cleanup(ene): make obsidian shim provenance configurable and schema-complete
2026-05-26 16:54:12 -05:00
Allaun Silverfox
27e267f58c
cleanup(ene): make provenance node/tailscale configurable via env vars and CLI arg
2026-05-26 16:42:03 -05:00
Allaun Silverfox
eab5393aaa
cleanup(ene): make provenance node/tailscale configurable via env vars and CLI arg
2026-05-26 16:40:35 -05:00
Allaun Silverfox
d3dcd6ae01
cleanup(ene): make provenance node/lake_seed/tailscale_ip configurable via env vars
2026-05-26 16:39:43 -05:00
Allaun Silverfox
152c7cd5b8
cleanup(ene): read canonical SQL schema file for chat tables; remove embedded DDL string
2026-05-26 16:34:23 -05:00
Allaun Silverfox
e5705e5ad2
cleanup(ene): add canonical SQL schema for chat/session sync tables
2026-05-26 16:23:51 -05:00
Allaun Silverfox
b5d3614c5d
cleanup(ene): remove hardcoded schema path, drop inline schema fallback, add legacy shim strip receipt
2026-05-26 16:22:40 -05:00
Allaun Silverfox
e9ba3dd6a4
docs(shim): annotate alignment shim as legacy pending AVM port; add strip receipt metadata
2026-05-26 16:14:52 -05:00
Allaun Silverfox
e15f04f500
docs(shim): annotate as legacy shim pending AVM port; add strip receipt metadata
2026-05-26 16:13:43 -05:00
Allaun Silverfox
75b8cb13e6
feat(avm): add Lean-only strict-typed ISA skeleton (v1)
2026-05-26 16:05:08 -05:00
Allaun Silverfox
8692a26916
docs(avm): strengthen float prohibition and documentation requirement
2026-05-26 16:02:05 -05:00
Allaun Silverfox
911bc5233e
docs(avm): add stripping policy and bad-code elimination rules
2026-05-26 15:59:41 -05:00
Allaun Silverfox
ebd39dc11d
docs(avm): redefine AVM as Lean-only ISA with adapter shims/backends
2026-05-26 15:58:25 -05:00
Allaun Silverfox
8931175f94
fix(pist): correct repo root + fail-on-raw-disagreement check
2026-05-26 15:50:29 -05:00
Allaun Silverfox
447e6f2c0e
docs: add RRC PIST shape-alignment phase
2026-05-26 15:47:19 -05:00
Allaun Silverfox
e767561730
feat(pist): add RRC PIST shape-alignment calibration pass
2026-05-26 15:43:45 -05:00
Allaun Silverfox
890fcb688a
archive: remove duplicate PISTMachine search-space copy
2026-05-26 15:42:48 -05:00
Allaun Silverfox
959614f5da
feat(pist): add RRC PIST validation report cleaner
2026-05-26 15:38:07 -05:00
Allaun Silverfox
4f195992c1
fix(lean): remove stale PISTMachine sorries
2026-05-26 15:31:59 -05:00
Allaun Silverfox
d076fb55b5
docs: add receipt-density verification sequence
2026-05-26 15:19:07 -05:00
Allaun Silverfox
d01ab8bc2e
feat(pist): add receipt-density sidecar readback validator
2026-05-26 15:18:11 -05:00
Allaun Silverfox
b7f8946f37
test(pist): add receipt-density injector regression harness
2026-05-26 15:16:40 -05:00
Allaun Silverfox
30df68ec2f
feat(pist): use shared rds_connect for receipt-density writer
2026-05-26 15:13:35 -05:00
Brandon Schneider
bdba17b4a4
chore: remove unused import subprocess from v14a (handled by rds_connect)
2026-05-26 15:11:11 -05:00
Brandon Schneider
ad251e20bc
refactor(rds): consolidate 14 psycopg2 connect patterns into shared rds_connect module
...
Creates 4-Infrastructure/shim/rds_connect.py with a single connect_rds()
function that resolves connection parameters in priority order:
1. explicit kwargs
2. DATABASE_URL env var (postgres://user:pass@host:port/dbname?sslmode=...)
3. individual RDS_* env vars (RDS_HOST, RDS_PORT, RDS_USER, etc.)
4. built-in defaults
Auth resolution (when password is empty or RDS_IAM=1):
1. RDS_IAM_TOKEN env var (pre-computed)
2. boto3 SDK generate_db_auth_token (preferred)
3. subprocess aws rds generate-db-auth-token (fallback)
4. RDS_PASSWORD env var (non-IAM)
Replaces 8 connection pattern variants across 14 active shims:
- subprocess + RDS_IAM_TOKEN fallback: pist_trace_classify_mcp, joint_classifier,
pist_prove_and_classify, ingest_57_flexures
- boto3 SDK: ene_wiki_body_reingest, ene_migrate_and_tag, dataset_ingest_rds
- subprocess + RDS_PASSWORD: batch_embed_artifacts, sync_wiki_to_rds, seed_flexure_dataset
- RDS_IAM_AUTH: pist_classify
- bashrc parsed: credential_loader
v1.4a benchmark confirmed at 100% after refactor.
2026-05-26 15:09:34 -05:00
Allaun Silverfox
395255f8c9
docs: add PIST receipt-density backfill guide
2026-05-26 14:46:55 -05:00
Allaun Silverfox
0352f6b5b4
feat(pist): add RRC receipt-density backfill injector
2026-05-26 14:46:13 -05:00
Allaun Silverfox
4512d0bd51
wiki: link PIST route-repair receipt update from home
2026-05-26 14:38:39 -05:00
Allaun Silverfox
f23e8f1518
wiki: add PIST route-repair receipt update tiddler
2026-05-26 14:36:34 -05:00
Allaun Silverfox
0407a559e3
docs: add PIST route-repair and receipt update
2026-05-26 14:36:15 -05:00
Allaun Silverfox
9a28ba54d7
archive: remove duplicate PISTMachine search-space copy
2026-05-26 14:31:44 -05:00
Allaun Silverfox
c6d05c005e
archive: preserve duplicate PISTMachine search-space copy
2026-05-26 14:30:39 -05:00
Allaun Silverfox
ca8758fdaa
fix(lean): remove stale PISTMachine sorries
2026-05-26 14:29:04 -05:00
Allaun Silverfox
101d1f7348
fix(lean): align SLUQ quaternion theorem with unit witness receipts
2026-05-26 14:25:04 -05:00
Allaun Silverfox
3128649b5a
fix(lean): prove resonance quaternion unit witness preservation
2026-05-26 14:22:00 -05:00
Allaun Silverfox
c1a5202f37
fix(lean): align genomic quaternion theorems with unit receipts
2026-05-26 14:18:28 -05:00
Allaun Silverfox
7b68e877a7
fix(lean): replace quaternion sorries with unit witness receipts
2026-05-26 14:14:31 -05:00
Allaun Silverfox
86d00b1030
feat(pist): add genus-0 sphere shell projection demo
2026-05-26 14:10:17 -05:00
Brandon Schneider
4ceb75eff7
feat(pist): v1.4a — 100% recovery across 35 theorems
...
All buckets sealed at 100%:
arithmetic_gap: 14 rec=100% (omega, simpa_nat, arith8_calc)
contradiction_bridge: 6 rec=100% (notnot_by_cases, notnot_intro,
notnot_apply_chain, neg_apply_chain)
missing_assumption_bridge: 5 rec=100% (chain_exact, forall_exact_0,
exact_hyp_match)
missing_destructuring: 5 rec=100% (dot_left/right, apply_dot_left/right)
case_split_missing: 1 rec=100%
constructor_missing: 1 rec=100%
Key fixes that closed the last gaps:
- parse_theorem regex: [^:=] → [^:] so goal with '=' is captured
- Classifier: arithmetic gap (goal has +-*/) checked before rewrite
- notnot_apply_chain: ¬¬Q from P, P→Q → intro h; apply h; apply hPQ; exact hP
- neg_apply_chain: ¬P from h:P→Q, hnQ:¬Q → intro hp; apply hnQ; apply h; exact hp
- forall_exact_0: ∀ n, P n ⊢ P 0 via exact h 0
- exact_hyp_match: A→B ⊢ A→B via exact h (hyp type matches goal)
- Added ∀ hyps to _imp_objs so chain builder considers them
- Removed leading whitespace from all multi-line patch strings
Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=100%
2026-05-26 14:03:59 -05:00
Brandon Schneider
82f65e9a60
feat(pist): Route-Repair v1.4a — 97% recovery, residual closure
...
v1.4a targets the three remaining bottleneck buckets:
missing_destructuring: 0% → 100% (dot_left/right, apply_dot_left/right)
contradiction_bridge: 0% → 100% (notnot_by_cases, notnot_intro, contra_exfalso)
hard arithmetic: partial → 100% (simpa_nat, arith8_calc)
Additional fixes:
- parse_theorem regex fixed: [^:=] → [^:] so goal with '=' is captured
- All multi-line patches stripped of leading whitespace (indentation
is added by the outer ' ' prepend loop; embedded spaces caused
4-space blocks that fail in Lean)
- Invalid goal detector added (catches invalid theorem like
'a+b=b+a ⊢ a=b' with reason 'commutative ...')
- Implication chain detector for multi-level apply chains
(A→B, B→C ⊢ C → exact hBC (hAB hA))
- Classifier prioritizes contradictory hypothesis pairs before
implication fallthrough (fixes P,¬P ⊢ Q misclassification)
Final per-bucket:
missing_rewrite_direction: 8 rec=88% (1 misclassified, marked INVALID)
arithmetic_gap: 7 rec=100%
missing_destructuring: 5 rec=100%
contradiction_bridge: 4 rec=100%
missing_assumption_bridge: 3 rec=100%
case_split_missing: 1 rec=100%
intro_chain_missing: 1 rec=100%
Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=97%
2026-05-26 13:51:05 -05:00
Brandon Schneider
150ddb6376
feat(pist): Route-Repair v1.4 — 71% recovery
2026-05-26 13:09:37 -05:00
Brandon Schneider
f09b7b84d7
feat(pist): Route-Repair v1.3b — multi-step templates, 54% recovery
2026-05-26 12:56:24 -05:00
