Develop carsten - #20
Closed
JuliusFiedler wants to merge 92 commits into
Closed
Conversation
Move taxonomy, scopes, math_expressions, operators and statement_utils helpers into a _builtin subpackage; builtin_entities.py becomes a re-export facade. Public and internal import paths unchanged; the ordering-sensitive bootstrap block stays in the facade (3226 -> 1913 lines). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 268c34f chore: bump minimum python to 3.10 and fix README typos # 7f2552b Merge branch 'develop_carsten' into develop # 8039cd2 test data paths renaming
Move keymanager, context, mod_management and serialization helpers into a _core subpackage; core.py becomes a re-export facade. Public and internal import paths unchanged. Also ignore the .orchester/ coordination dir (2902 -> 2151 lines). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # bb0b0f0 refactor: split builtin_entities into _builtin subpackage # 268c34f chore: bump minimum python to 3.10 and fix README typos # 7f2552b Merge branch 'develop_carsten' into develop
…rmance mcp_authoring.md: MCP-server design exposing the live DataStore to an LLM (retrieval-first, explicit modeling forks, immediate validation), with a LaTeX-textbook ingestion path. performance.md: profiling of the OCSE suite shows the bottleneck is per-access substrate overhead (attribute resolution + read-path validation), not the rule engine; ROI-ordered levers behind the stable API. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 980bb85 Merge branch 'refactor_autonomous' into develop_carsten # 413b047 refactor: split core into _core subpackage # bb0b0f0 refactor: split builtin_entities into _builtin subpackage
…ind asserts (H1) Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 738566c perf(tools): add reproducible performance benchmark harness (phase 0) # 1008072 docs: add design documents for LLM-assisted authoring (MCP) and performance # 980bb85 Merge branch 'refactor_autonomous' into develop_carsten
Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 4867c48 perf(core): precompile short-key regex, gate read-path validation behind asserts (H1) # 738566c perf(tools): add reproducible performance benchmark harness (phase 0) # 1008072 docs: add design documents for LLM-assisted authoring (MCP) and performance
Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # ba7490a perf(core): memoize attribute key resolution (H2) # 4867c48 perf(core): precompile short-key regex, gate read-path validation behind asserts (H1) # 738566c perf(tools): add reproducible performance benchmark harness (phase 0)
…plicit raise Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # b362fb8 perf(core): invalidate attr-name cache on module unload # ba7490a perf(core): memoize attribute key resolution (H2) # 4867c48 perf(core): precompile short-key regex, gate read-path validation behind asserts (H1)
…licit raise Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 7bfdad4 refactor(core): convert load-bearing assert in update_relations to explicit raise # b362fb8 perf(core): invalidate attr-name cache on module unload # ba7490a perf(core): memoize attribute key resolution (H2)
…icit raises - set_multiple_relations: TypeError on non-(tuple|list) obj_seq - overwrite_statement: TypeError on non-str rel_key_str_or_uri - get_first_qualifier_obj_with_rel: ValueError on key/uri exclusivity violation These were the three 'unklar' candidates from .orchester/assert_audit_inventory.md. Reviewed manually; all three are caller-precondition checks at public method entry points. Picked exception type per case (TypeError for type checks, ValueError for argument-exclusivity logic) instead of preserving AssertionError, so the failures are now self-documenting via type. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 341645c refactor(core): convert load-bearing assert in create_relation to explicit raise # 7bfdad4 refactor(core): convert load-bearing assert in update_relations to explicit raise # b362fb8 perf(core): invalidate attr-name cache on module unload
Brings in the autonomous performance work (perf_autonomous lineage) plus the assert audit follow-up: substrate optimizations H1 (regex precompile + read-path validation behind asserts) and H2 (attribute key resolution memoization), the reproducible perf benchmark harness, cache invalidation on module unload, and conversion of load-bearing precondition asserts in update_relations, create_relation, set_multiple_relations, overwrite_statement and get_first_qualifier_obj_with_rel to explicit raises. Effect: python -O is now a clean speedup without behavioural change, suites green under both python and python -O. # Last 3 commits: # 1008072 docs: add design documents for LLM-assisted authoring (MCP) and performance # 980bb85 Merge branch 'refactor_autonomous' into develop_carsten # 413b047 refactor: split core into _core subpackage
Two issues in `pyirk -utd` made the test-data subset effectively un-regenerateable: * The `insert_entities = [...]` list was parsed by splitting the raw source text on newlines, which mangled any multi-line list entry (e.g. a long `raw__I.set_relation(...)` call) into separate "lines" that the per-line dispatch could not classify, raising `InvalidGeneralKeyError: unexpected key_str: \`)\``. * Any template entry that no longer existed in the upstream OCSE (e.g. I4895, removed/renamed in newer OCSE versions) aborted the whole regeneration with KeyError, killing subsequent unrelated entries. The fix iterates the list elements via the AST (multi-line entries stay as one entry), and emits a warning for missing short keys instead of hard-failing. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 1008072 docs: add design documents for LLM-assisted authoring (MCP) and performance # 980bb85 Merge branch 'refactor_autonomous' into develop_carsten # 413b047 refactor: split core into _core subpackage # Last 3 commits: # f704652 Merge branch 'assert_audit_autonomous' into develop_carsten # 3a7cb1f refactor(core): convert remaining 'unklar' asserts in core.py to explicit raises # 341645c refactor(core): convert load-bearing assert in create_relation to explicit raise
Update the OCSE-subset template to track changes in upstream OCSE and to support a runnable theorem-howto example: * Remove three references that no longer exist in OCSE math1: I4895 (mathematical operator), R3033 (has type of elements), I7765 (scalar mathematical object). I7765 still appears inside a docstring of an extracted entity, which is fine -- it is not executed. * Add I1169 (point in vector space): newly required by I1168's R3 in the current OCSE, otherwise the regenerated subset NameErrors on load. * Add the planar-geometry building blocks needed by the theorem howto: I1913 geometric object, I7280 planar polygon, I2917 planar triangle, I8172 polygon side, R2495 has length, I9148 get polygon sides ordered by length (with custom_call setup). Regenerated subset via `pyirk -utd <ocse>`. Test baseline unchanged: 118 passed, 4 skipped, 2 xfailed. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 9478e60 fix(script): make update-test-data robust to template drift # 1008072 docs: add design documents for LLM-assisted authoring (MCP) and performance # 980bb85 Merge branch 'refactor_autonomous' into develop_carsten # Last 3 commits: # a3b4e3c fix(script): make update-test-data robust to template drift # f704652 Merge branch 'assert_audit_autonomous' into develop_carsten # 3a7cb1f refactor(core): convert remaining 'unklar' asserts in core.py to explicit raises
The theorem howto referenced aspirational items (I1002 angle, I1003 right angle) that do not exist in OCSE, the API items_to_symbols (never existed), and an incorrect new_equation signature with "==" in the middle -- so the example did not run. Rework as a runnable, self-contained example that loads the OCSE math subset from tests/test_data/ocse_subset (no external data dependency): * Add a shared value type "angle (quantity)" (subclass of real number) so the local `angle` operator and the `right angle` constant are explicitly typed as the same kind of quantity, instead of merely sharing real number by coincidence. * Use the prefix attribute form a.ma__R2495__has_length for the cross-module length relation that lives in the OCSE math module. * Use pyirk Item operator overloads (la**2 + lb**2) directly -- no sympy detour. * theorem.md: new "Dependencies and bootstrap" and "Local additions for missing concepts" sections; adjust literalinclude line ranges; drop the misleading note claiming the local items came from OCSE. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 923010a test(ocse_subset): drop stale items, add planar geometry block # 9478e60 fix(script): make update-test-data robust to template drift # 1008072 docs: add design documents for LLM-assisted authoring (MCP) and performance # Last 3 commits: # 36d6a67 test(ocse_subset): drop stale items, add planar geometry block # a3b4e3c fix(script): make update-test-data robust to template drift # f704652 Merge branch 'assert_audit_autonomous' into develop_carsten
Recurring question from newcomers and reviewers: why build a formal knowledge representation when LLMs can already read most engineering material? Adds a dedicated page that addresses this directly without hand-waving: where LLMs alone suffice (explicitly named, not glossed over), where they do not (five concrete classes, with named regulatory frameworks for the certification argument: DO-178C, ISO 26262, IEC 61508/61511, ISO 13849, IEC 62304), and how pyirk plus LLM-based tooling combine in practice. The complementarity section grounds the abstract argument in ``pyirk.authoring`` -- the LLM does the fuzzy ingestion step, the round-trip ``irkloader`` validation does the precise correctness step. Neither suffices alone. Linked from the index motivation section so the question is addressed where it naturally arises for a first-time reader. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 213e916d fix(authoring/lean): anchor regex; track namespace per theorem # ac07ea4b feat(authoring): Claude-Code-native authoring substrate + Lean adapter # c16a53ca docs(howto): make theorem howto runnable and fix modeling # Last 3 commits: # 289e2ce docs(howto): make theorem howto runnable and fix modeling # 36d6a67 test(ocse_subset): drop stale items, add planar geometry block # a3b4e3c fix(script): make update-test-data robust to template drift
Create a minimal stub at docs/source/authoring.md so other pages can link to it. Content is intentionally short: short description plus an explicit 'still in development' notice and pointers to the source tree and the design document. Update llm_complementarity.md to link the inline mention of ``pyirk.authoring`` to the new page, and add it to the index toctree. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 483a3c09 docs: add page on pyirk-LLM complementarity # 213e916d fix(authoring/lean): anchor regex; track namespace per theorem # ac07ea4b feat(authoring): Claude-Code-native authoring substrate + Lean adapter # Last 3 commits: # f588c8c docs: add page on pyirk-LLM complementarity # 289e2ce docs(howto): make theorem howto runnable and fix modeling # 36d6a67 test(ocse_subset): drop stale items, add planar geometry block
Two small fixes from the path-fragility plan: - tests/settings.py: derive TEST_DATA_DIR1 from the file's own location (current_dir, already in scope) instead of joining IRK_ROOT_DIR with the hardcoded literal 'pyirk-core'. The previous form broke whenever the package was checked out into a directory with a different name (e.g. a feature-branch worktree like pyirk-audit-followup), producing FileNotFoundError on every test that touches TEST_DATA_DIR1. - src/pyirk/irkloader.py:145: when a module is requested a second time, the cache-equality check now uses os.path.samefile instead of comparing abspath strings. samefile follows symlinks and compares inodes, so two path representations of the same file (typical when the worktree is accessed via a symlink) no longer trip the assertion. Verified by running the test suite in a worktree named pyirk-fragility-verify: without these fixes the suite produces 58 failures; with them, all but five pre-existing failures pass. The remaining five are unrelated to this fix (test ordering / sys.modules cache fragility around the staged math1.py, plus a hardcoded path in tests/test_data/reports/reportconf.toml, plus test_a01__directory_structure which intentionally tests the layout convention). They are documented separately in path_fragility_plan__gitignore__.md. get_irk_root_dir() generalization is intentionally out of scope here. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # a784986 Merge branch 'docs_update' into develop_carsten # e826367 docs: add placeholder page for pyirk.authoring # f588c8c docs: add page on pyirk-LLM complementarity
…-cache fragility
The staged ocse_subset/math1.py was missing 'real part' (I5005) and
'imaginary part' (I5006), which test_c07d__nested_boolean_scopes references
via ma.I5005 and ma.I5006. The full suite happened to pass because
test_c011 loaded the real OCSE math1 into sys.modules first, and subsequent
load_mod_from_path('./math1.py') returned the cached real module instead of
loading the staged subset. In isolation or under a different test order the
test failed with AttributeError.
Adding the two entity definitions (copied verbatim from real OCSE math1.py)
makes the staged subset self-sufficient for test_c07d, eliminating the cache
dependency for this test.
This is Phase 1 of test_fragility_plan__gitignore__.md. Phases 2/3 address
the remaining I4895 cross-test datastore contamination affecting
test_e02__is_true and test_c02__cc_multi_valued_domain.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
# Last 3 commits:
# 33a0e36 fix: make path resolution robust to renamed/symlinked worktrees
# a784986 Merge branch 'docs_update' into develop_carsten
# e826367 docs: add placeholder page for pyirk.authoring
…er it
test_e02__is_true and test_c02__cc_multi_valued_domain previously depended on
test_consistency_check.create_operators having run first (and not yet torn down)
to populate the global datastore with I4895['mathematical operator']. Without
that ordering, ma.I4895 raised AttributeError. The fragility was masked in the
'lucky' test order but failed in isolation or under random order.
Resolution per test_fragility_plan__gitignore__.md Phase 3:
- Define I4895 as a regular entity in the staged math1 (subclass of
p.I12['mathematical object']). Add the _custom_call=create_evaluated_mapping
method analogous to what p.I7 has in builtins, so that instances remain
callable (required by test_d02__custom_call_post_process1).
- Reclassify I5359['determinant'] as R4__is_instance_of=I4895 instead of
=p.I7['mathematical operation with arity 1']. This matches the original
modelling intent already documented in the I5359_cc_pp docstring
('The I5359["determinant"] is an I4895__mathematical_operator.') and
makes p.is_true(ma.I5359, p.R4, ma.I4895) true via a direct R4 statement
rather than via cross-test datastore pollution.
The staged subset now intentionally diverges from the real OCSE math1 (which
classifies I5359 under p.I7) — the staged version uses a less specific
classification so tests can rely on it without coupling to other test methods.
test_consistency_check.create_operators continues to define its own I4895
under TEST_BASE_URI; the two definitions are URI-disjoint and do not collide.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
# Last 3 commits:
# 6c10dfc fix(test_data): add I5005/I5006 to staged math1 to remove sys.modules-cache fragility
# 33a0e36 fix: make path resolution robust to renamed/symlinked worktrees
# a784986 Merge branch 'docs_update' into develop_carsten
``_load_mod_from_path`` had two stacked "is this module already loaded?" checks: a sys.modules cache check at the top (added later for "do not complain if the same module is loaded again", commit 35d211d), and a pyirk-registry check further down that consults ``reuse_loaded`` to decide between unload+reload and cache-return. The sys.modules check returned the cached module unconditionally, so the older ``reuse_loaded`` semantics were de facto bypassed for any second call. Downstream effect that surfaced during ``--all`` runs of ``authoring.import_lean``: ``authoring.validate_module(reuse_loaded= False)`` silently returned the stale cached module after each append, so theorems 2..N of an --all run were never actually round-trip- validated. The CLI test ``test_all_flag_iterates_theorems`` works around this with an explicit ``p.unload_mod`` + ``sys.modules.pop`` -- this commit removes the need for that workaround at the library level. The test is left in place; the workaround now has no effect but it stops the test breaking if a future regression reintroduces the bug. Fix: gate the early sys.modules return on ``reuse_loaded`` being truthy. When ``reuse_loaded`` is False, fall through to the existing reload path; ``pyirk.unload_mod`` (invoked via the ``old_mod_uri`` branch) then drops sys.modules[modname] itself, so we do not pop here. A first attempt that popped sys.modules early in this same branch broke 6 unrelated tests because ``unload_mod`` uses ``sys.modules.pop (modname)`` (strict) and crashed with KeyError on the now-absent entry. The corrected fix preserves the invariant that sys.modules contains the cached module until ``unload_mod`` removes it. Verified: lean-content-import local pytest goes from "116 passed, 7 failed" (with the broken early-pop variant) to "122 passed, 1 failed" (with this corrected version) -- identical to the baseline on develop_carsten + lean-content-import without the fix, but now exercising ``reuse_loaded=False`` semantics correctly. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> # Last 3 commits: # 323d6a13 fix(tests): make test_script subprocess calls PATH-independent # a6fc3853 feat(cli): wire --import-lean / authoring substrate into pyirk script + bootstrap helper + smoke tests # a92e764d feat(authoring): make FORK mandatory for ambiguous modeling decisions # Last 3 commits: # 8f17a10 fix(test_data): define I4895 in staged math1 and reclassify I5359 under it # 6c10dfc fix(test_data): add I5005/I5006 to staged math1 to remove sys.modules-cache fragility # 33a0e36 fix: make path resolution robust to renamed/symlinked worktrees
The de-facto test tooling now has a declared home instead of floating as ad-hoc installs. Deliberately NOT in requirements.txt (runtime deps via [tool.setuptools.dynamic]) and NOT wired into CI: randomized test order as a CI gate decouples failure from cause (fires on innocent commits, seed archaeology). Intended use: on-demand ordering diagnosis via `pytest -p randomly` after changes to test fixtures/infrastructure. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> # Last 3 commits: # 156514f fix(irkloader): honor reuse_loaded=False in the sys.modules cache check # 8f17a10 fix(test_data): define I4895 in staged math1 and reclassify I5359 under it # 6c10dfc fix(test_data): add I5005/I5006 to staged math1 to remove sys.modules-cache fragility
…les (PEP 563) Completes wave-2 stretch goal (P4). Singletons ds/pf stay in the core.py facade; method dependencies on core classes resolved lazily via _core.xxx. Verified identical to baseline: pytest (det.+randomized), python -O, unittest, sphinx-build, API smoke (see .orchester run report). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> # Last 3 commits: # cc9440e refactor(core): extract format_entity_html to _core/html_format (PEP 563) # 9a4c9d7 refactor(core): extract replace_and_unlink_entity to _core/entity_ops (PEP 563) # 69f00f0 refactor(core): extract query helpers to _core/queries (PEP 563)
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> # Last 3 commits: # c56961e refactor(core): extract DataStore and PrefixShortCut to _core submodules (PEP 563) # cc9440e refactor(core): extract format_entity_html to _core/html_format (PEP 563) # 9a4c9d7 refactor(core): extract replace_and_unlink_entity to _core/entity_ops (PEP 563)
Refactoring wave 2: extract queries, entity_ops, html_format, PrefixShortCut and DataStore from core.py into _core/ submodules (PEP 563). Verified on VPS and locally: identical to baseline. # Last 3 commits: # 0347e95 build: declare pytest + pytest-randomly as optional [test] extra # 156514f fix(irkloader): honor reuse_loaded=False in the sys.modules cache check # 8f17a10 fix(test_data): define I4895 in staged math1 and reclassify I5359 under it
Investigation (dead-end branch native_dup_hygiene) showed 4/5 'duplicates' differ by qualifier/scope (legit statements; the gate's (s,p,o) enumeration overcounts them) and statement multiplicity is intentional in pyirk (R54 match counts). A defensive dedup destroyed R54 multiplicity → discarded. Retroactively confirms the gate-3 dup-multiset==native calibration. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> # Last 3 commits: # 94f4bab Merge branch 'h5_phase2' into develop_carsten # 890f6c6 docs(h5_phase2): gate_ok=ja after gate-3 recalibration (376x, equiv to native) # 6d6e594 test(h5_phase2): recalibrate gate 3 to dup-multiset equivalence vs native
…ase 2 ocse gate Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 822354d feat(h5_extension): delegate literal-premise rules I705 I790 I800 I820 # ca20601 docs(h5): correct the 'native R30/R31 dup hygiene' note — not a bug # 94f4bab Merge branch 'h5_phase2' into develop_carsten
…inal report Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # db4f657 feat(nemobridge): robust nmo resolver, idempotent warnings, version check # ca7633c docs(h5_extension): final report # 14f784b test(h5_extension): add curated zebra equivalence gate, revalidate phase 2 ocse gate
…nd resolver - delegation: legacy nmo fallback is now ~/bin/nmo (expanduser) instead of the VPS-specific /home/user/bin/nmo - test_h5_extension_literal_premises: use the production nmo resolver for the skip condition, sys.executable for subprocesses, drop the sympy sys.path overlay (subprocess inherits the parent environment) - h5_extension equivalence gate: resolver-based nmo lookup, sys.executable default (PYIRK_VENV_PYTHON override), sympy overlay now pure opt-in via PYIRK_GATE_SYMPY_EXTRA and only applied if the directory exists - docs/howto + resolver-test docstring updated accordingly Historical reports and gate logs keep their literal VPS paths (they are records of concrete runs, not executable configuration). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
H5 extension (literal-premise delegation, q32) + deployment robustness (resolver, fallback, version check, docs, q33) + host-path portability fix. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 0aa598f Merge branch 'h5_deployment' into develop_carsten # b429427 refactor(h5): remove host-specific hardcoded paths from tests, gate and resolver # 3495663 chore(h5_deployment): commit acceptance-gate logs referenced by the report
… delegation Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 311e12d feat(nemobridge): translate pure-BGP SPARQL premises for I798 # 0aa598f Merge branch 'h5_deployment' into develop_carsten # b429427 refactor(h5): remove host-specific hardcoded paths from tests, gate and resolver
H5 SPARQL premise delegation (q36): pure-BGP (Stage 1) and BGP+inequality (Stage 4) translation via the rdflib SPARQL algebra. 5 rules newly classified direct (I710/I730/I740/I792/I798); I725/I803/I741 honest-stop python_only. All three equivalence gates green, full suite unchanged with flag off. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Same path-portability fix already applied to the extension gate (commit b429427); the phase2 gate was missed then: - nmo via delegation._resolve_nmo_bin() instead of /home/user/bin/nmo - OCSE dir via PYIRK_OCSE_DIR env or the pyirk config (package.ocse.path), legacy default kept as last resort - subprocess interpreter via sys.executable (PYIRK_VENV_PYTHON override) - sympy overlay now opt-in via PYIRK_GATE_SYMPY_EXTRA, only if the dir exists Verified locally: overall_gate_ok=true (native_dups=5, deleg_dups=5). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The delegation flag was env-only (PYIRK_NEMO_DELEGATION), which is tedious for a developer who wants the speedup in all their own runs. Add a delegation_enabled() resolver: env var (decisive in both directions) over pyirk config [nemo] delegation over a shipped default of off. The general user is unaffected unless they opt in; an individual can enable it persistently in their config. Also fixes a latent bug: the old 'if os.environ.get(...)' treated PYIRK_NEMO_DELEGATION=0 / =false as truthy and wrongly ENABLED delegation, contradicting the docs. Falsy tokens (0/false/no/off) now disable correctly. Docs (how-to + README) document the config toggle and precedence; 7 new unit tests cover the env/config/default matrix. Full suite green with flag off (197 passed); rule-based reasoning green with flag on. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`pyirk --help` now ends with the resolved config.toml path and whether it exists (with a hint to --bootstrap-config if not), so users do not have to remember where platformdirs puts it. Single source of truth: reuses settings.config_file. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A fresh 'pyirk --bootstrap-config' now writes a commented [nemo] delegation stanza next to the existing package example, so on a new install the user sees the opt-in decision while editing the file, with an inline pointer to the docs (readthedocs -> How-to -> Nemo delegation) for the background. CI bootstrap content is left unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Squash-merge of branch lean-content-import: a Claude-Code-native authoring substrate that imports formal statements into pyirk content modules, with a Lean/mathlib4 source adapter as the first frontend. Core (src/pyirk/authoring/): retrieval-first prompting with a worked example, structured append + round-trip validation via irkloader, claude -p subprocess with JSON cost tracking, mandatory FORK escalation for ambiguous modeling, and pipeline-owned guards for the failure classes surfaced by three bulk runs: key-collision remapping, non-ASCII Lean operators, scope-reopen, and retryable timeouts. CLI (pyirk --import-lean): single/--all import, unattended --fork-policy, per-theorem --stats-jsonl, --keep-going, --resume, --limit; plus a mocked dry-run tool and a regression guard for the irkloader reuse_loaded short-circuit. The three bulk-run evaluations are kept as bulk_runs*/SUMMARY.md (66/89 -> 80/89 ok across runs; the raw generated modules/stats/logs are intentionally left on the lean-content-import branch). Full suite green: 223 passed, 12 skipped, 2 xfailed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> # Last 3 commits: # c10d298 feat(cli): seed bootstrapped config with commented nemo-delegation block # e247a6d feat(cli): show config file path in --help output # d2d921c feat(nemobridge): persistent opt-in for nemo delegation via pyirk config
Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # acd5c66 feat(authoring): add LaTeX snippet adapter for fnl_vs_direct experiment # 9e43a87 feat(authoring): Lean-theorem import substrate + 3 validation runs # c10d298 feat(cli): seed bootstrapped config with commented nemo-delegation block
… for fnl_vs_direct Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 18b7138 feat(experiment): add snippet selection + README for fnl_vs_direct # acd5c66 feat(authoring): add LaTeX snippet adapter for fnl_vs_direct experiment # 9e43a87 feat(authoring): Lean-theorem import substrate + 3 validation runs
Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # a4d7e53 feat(experiment): tokenfree mock dry-run harness + metrics aggregator for fnl_vs_direct # 18b7138 feat(experiment): add snippet selection + README for fnl_vs_direct # acd5c66 feat(authoring): add LaTeX snippet adapter for fnl_vs_direct experiment
…_direct Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 1b4fcef feat(experiment): structural pyirk diff (corpus A) for fnl_vs_direct # a4d7e53 feat(experiment): tokenfree mock dry-run harness + metrics aggregator for fnl_vs_direct # 18b7138 feat(experiment): add snippet selection + README for fnl_vs_direct
…pter Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 1698e13 feat(experiment): LLM-judge harness (mock + Opus skeleton) for fnl_vs_direct # 1b4fcef feat(experiment): structural pyirk diff (corpus A) for fnl_vs_direct # a4d7e53 feat(experiment): tokenfree mock dry-run harness + metrics aggregator for fnl_vs_direct
Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # 3536f41 feat(authoring): math-tuned LATEX_PROMPT_HEADER for LaTeX snippet adapter # 1698e13 feat(experiment): LLM-judge harness (mock + Opus skeleton) for fnl_vs_direct # 1b4fcef feat(experiment): structural pyirk diff (corpus A) for fnl_vs_direct
…es for fnl_vs_direct Co-Authored-By: claude-orchester <noreply@anthropic.com> # Last 3 commits: # ac2bb63 feat(experiment): direct-arm full run (Opus, 50/50 snippets, 46/50 ok) # 3536f41 feat(authoring): math-tuned LATEX_PROMPT_HEADER for LaTeX snippet adapter # 1698e13 feat(experiment): LLM-judge harness (mock + Opus skeleton) for fnl_vs_direct
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.