Allow proof imports with measured impact

[Deicyde]

Summary

• Add autoform work import-impact to report the loaded reverse-import, article, helper, and claim scope of a module header edit without forbidding the edit.
• Bind module evidence to the captured root source and the exact configured root-package OLean, expose a stable v1 JSON contract, and reject dependency-shadowed or ambiguous ownership evidence.
• Require only the selected article and module claim up front; keep downstream scope advisory until validation proves another article must change.
• Document a permissive, fail-closed claim lifecycle in Formalize, AGENTS.md, and the development skill while keeping the CLI reference concise.

Policy

Lean imports are allowed. Autoform measures their loaded-build impact and reports active coordination risks; it does not impose a blanket import ban. Unresolved declarations are disclosed without globally blocking unrelated edits. Claims are acquired atomically, renewed and released as a complete set, and released before waiting after any refusal or recheck conflict.

Validation

• make lint
• make test: 1,920 passed, 6 skipped, 1 expected failure
• make check-example, including strict MkDocs
• skill-creator validation for develop-plugin and formalize
• real Lean regressions for reverse-import evidence and dependency OLean shadowing
• independent adversarial code and contract reviews: ready

[Deicyde]

Adversarial review at 788c6f1

Five review passes ran on this head: logic, evidence binding, CLI and docs contract, test teeth (mutation testing), and golf. A separate refuter re-ran every finding and tried to knock it down; only what survived is below. All four bugs were reproduced on real Lean at this head.

Verdict: not merge-ready yet. Two cases silently under-report the import scope, and two valid project layouts make every query fail. Each fix is local. CI is green and the PR merges cleanly onto main (landing notes at the end).

Bugs

1. A root module missing from the snapshot inventory silently cuts import edges (autoform_cli/probes/impact_probe.lean:134, :142)

The probe emits evidence only for inventory modules (:134) and drops every import of a non-inventory module (:142). A module that Lake builds into the root artifact dir, but whose source the snapshot skips, gets no node, so every reverse-import path through it disappears. _validated_module_evidence checks only the records that were emitted, so nothing refuses.

• Triggers: a source directory with a .git entry (a submodule), a directory named build or listed in lean.py's _IGNORED_DIRECTORIES, a symlinked source directory, and (at this head) a numeric component such as Demo/1.lean, because skeleton._lean_name builds Name.num while Lean names the module with Name.str "1".
• Repro: Demo.lean imports Demo.Top, which imports Demo.Mid.X, which imports Demo.Base. Demo/Mid/.git is a gitlink file, and chapter/top names Demo.Top.t. work import-impact chapter/base Demo.Base --json exits 0 with affected_modules=["Demo.Base"], article_local=true, affected_claim_targets=[]. With the .git marker renamed away (same OLeans): affected_modules=["Demo","Demo.Base","Demo.Mid.X","Demo.Top"], affected_claim_targets=["chapter/top","lean/demo-mid-x-v-e01855e454039a2c"].
• Fix: fail closed. Pass the root artifact dir into the probe. For each loaded module outside projectModules, refuse when IO.FS.realPath (← findOLean m) lies under that dir, and name the module and say its source is outside the captured inventory. Add a real-Lean test with a nested .git or a build source directory.

2. Removing an import can drop modules from the build, and the report never mentions them (autoform_cli/impact.py:949)

The scope is the reverse-import closure of MODULE, which covers what an added import can affect. A removed import can also take modules out of a roots-only library's build.

• Repro: roots-only lean_lib Imp2. Imp2.lean imports Imp2.Base and Imp2.ModD. Only Imp2.ModD imports Imp2.OnlyPriv, whose Imp2.onlyPriv is named by chapter/onlypriv. work import-impact chapter/modd Imp2.ModD reports Imp2, Imp2.ModD, prints "Article scope: no other article names a declaration in the reverse-import scope.", and requires only chapter/modd plus the module key. After ModD's import is removed, lake build succeeds and Imp2.OnlyPriv silently leaves the build. chapter/onlypriv never got a claim check or a baseline.
• Fix: pass the probe's selected imports (already in _load_impact_evidence) into compute_module_import_impact and report what may leave the build:

  forward = {m: set(e.direct_local_imports) for m, e in modules.items()}
  forward[module] = set()
  may_leave = set(modules) - _reverse_closure(imports, forward)

  On the repro graph this returns ["Imp2.OnlyPriv"]. Add those modules' articles to the affected scope or to a separate field. At minimum, document that the scope covers added imports only; the docstring at :935 and the CLI help call it "conservative".

3. Module names that need «» make every query fail with a false error (autoform_cli/impact.py:408, :443)

The probe prints Name.toString spellings (H.«2_1»), while _source_modules keys modules by raw path parts (H.2_1). The lookup at :408 misses and raises "the impact probe loaded H.«2_1» without a captured root-project source" for every MODULE, including plain ones. Textbook layouts hit this: H/2_1.lean, Q/my-lemmas.lean, Demo/x-y.lean.

• Repro (re-run at this head): roots-only lean_lib H, where H.lean has import H.«2_1». work import-impact chapter/top H exits 2 with that error. work impact chapter/top on the same project exits 0.
• Fix: compare by name components on both sides (tuple(p for p, _ in _lean_name_parts(name)), already in skeleton.py). Build the artifact path from the components too: artifact_dir.joinpath(*parts[:-1], parts[-1] + ".olean"). That also avoids with_suffix, which truncates a dotted stem such as «a.b». A patched copy passes test_impact.py (93 passed with real Lean). Add a stub-probe test with a quoted name.
• Keep work impact working beside Lean files whose names are not identifiers #182 makes this worse, because it quotes components that fail an ASCII identifier regex. After both land, R/α.lean (fine at this head) is keyed R.«α» while Lean prints R.α, so :408 regresses. Q.«my-lemmas» then passes :408 but fails at :443, which expects Q/«my-lemmas».olean. The same component fix covers both; whichever PR lands second should carry it.

4. A library nested inside another library's srcDir blocks every query (autoform_cli/impact.py:297, :378)

The strict one-to-one check maps every captured file under every srcDir, not just the modules a library selects. Take lean_lib Demo (srcDir ".") plus lean_lib Extra (srcDir "extra"). Then extra/Extra.lean maps to both extra.Extra and Extra, and every query fails before the probe with "project source extra/Extra.lean maps to more than one module: extra.Extra, Extra". Demo never selects extra.Extra and Lake has no such module (on the equivalent T/TTests layout, lake build tests.TTests gives "unknown target"), so the refusal protects nothing. work impact handles the same project, and skeleton.module_of (skeleton.py:1310) already resolves nested srcDirs to the innermost library. The existing refusal test (tests/test_impact.py:1219) has both libraries select the file, so it cannot tell the cases apart.

• Fix: keep "one module, one source". Check "one source, one module" only for modules a library selects (by root prefix or glob, as Lake's LeanLib.isLocalModule does), or only for modules Lean loaded. Add a positive nested-srcDir case next to the refusal test.

Should fix

5. A case-mismatched --lean-root is refused on macOS (autoform_cli/impact.py:414, :422)

Path(lean_root).resolve() keeps the typed case, while the probe's IO.FS.realPath returns the on-disk case. On case-insensitive APFS, --lean-root .../PROJ for a project stored as proj fails on the first module: "resolved to .../proj/Demo/Base.lean, expected captured root source .../PROJ/Demo/Base.lean". work impact accepts the same root. The check fails closed, but the message reads like a shadowing failure. Fix: keep string equality as the fast path, and fall back to os.path.samefile (OSError means no match) at both lines.

6. article_local is true while affected_claim_targets names other articles (autoform_cli/impact.py:723-727, :1009-1015)

The owner clause adds another article's claim target when that article owns, through the parent chain, a helper in an affected module. That article is not in affected_articles, and owned helpers are listed nowhere. Example: chapter/x names structure Demo.A.Foo, and its API lemma Demo.A.Foo.lemma lives in Demo.B. For MODULE Demo.B the report prints "Article scope: no other article names a declaration in the reverse-import scope." and then "Check active claims or semantic changes for: chapter/x" with no reason given. article_local is true. Formalize baselines only "named affected articles", so chapter/x gets no baseline. Unowned helpers behave the same way. Putting API lemmas in a later file is ordinary Lean style.

• Fix: define article_local as self.selected_affected and not self.affected_claim_targets and not any(a.id != self.article.id for a in self.unresolved_articles), matching revision impact's contained. List owner articles in affected_articles, or list owned helpers with their owner, so every claim target has a visible reason.
• The README's v1 contract (README.md:710-723) never describes affected_articles, selected_affected, article_local or module_claim_key. Yet Formalize (SKILL.md:59-60) sends readers to that reference for "named affected articles". Document these fields, or drop the two booleans before v1 freezes, since nothing consumes them.

7. Formalize contradicts itself on downstream edits (skills/formalize/SKILL.md:71-72, :172, against :87-90 and :143)

The import section says "If any article actually needs changes, atomically acquire the full held set plus its targets". The claim lifecycle keeps "any validated expansion", and so do AGENTS.md and the comment at impact.py:1019-1021. The unchanged rules still say "do not modify another article or its Lean declarations ... The one exception is revising a declaration other articles' Lean uses". They also send "a change another article needs" back to Roadmap. A worker following the skill either stalls, or edits a downstream article without the per-article gates the revision contract requires: the reload gate and an Agent Review of each repair. Pick one policy and state it once. Either list import repairs as a second exception at :89 with those gates, or route them to Roadmap and drop the expansion language.

Test gaps

These come from mutation testing of test_impact.py and test_skill_examples.py with Lean off PATH. Every mutant below still gives 117 passed, 2 skipped.

• Owner and helper filters (impact.py:995-998, :1009-1015). These mutants all survive: deleting the owner generator, dropping record.module in affected_set, dropping owner != selected.id, and dropping the module, internal or owner helper filter. On the real Imp fixture, dropping the module filter adds 23 out-of-scope helpers, giving 33 targets instead of 10. One exact compute test kills all six. Build records with parent set, an internal companion and an out-of-scope owned record. Then assert affected_claim_targets == ("af_base", _lean_key("Demo.Use.helper")) and assert the helper names. Also change the >= at test_impact.py:2340 to ==.
• Module claim key (impact.py:1067-1072). Only a regex pins it (test_impact.py:181). Hashing module.lower() survives, even though it changes every key across versions and gives Demo.Foo and Demo.foo the same key. Assert the exact value, "lean-module/demo-base-" + hashlib.sha256(b"Demo.Base").hexdigest()[:16], and add one name whose slug exceeds 48 characters.
• Shared srcDir (impact.py:370, :378). Every fixture declares one lean_lib. Weakening either comparison to is not None survives, yet it refuses every main-plus-test project on a shared srcDir. Add Demo and DemoTest on "." and assert that strict project_modules succeeds. Pair it with the nested case from bug 4.
• Text output. Every successful import-impact CLI test passes --json. Swapping the formatter at __main__.py:749 for format_impact survives. Yet the default text output then raises AttributeError outside the try block (__main__.py:783), which means a traceback and exit 1. The six optional text sections are not pinned either. Add an exact-lines test modelled on test_cli_text_report_lists_each_section.
• Article with no lean: declaration. Flipping require_default_declarations=False (impact.py:1386) survives. chapter/empty would then be refused with "pass --declaration NAME", a flag import-impact does not have. empty.md already exists in the fixture.

Golf (optional)

Each item was applied alone to a copy of this head. Each passed ruff and test_impact.py (93 passed with real Lean). A differential harness, using random inputs or CLI scenarios, found output identical to head.

• __main__.py:725-785: replace the two lambdas and _run_impact_command with one _work_impact handler. That drops the Callable import, the ModuleImportImpactReport import, and the formatter: Callable[[ImpactReport | ModuleImportImpactReport], list[str]] annotation, which is wrong for both callers. Net -25 lines.
• impact.py:992-1018: build the unowned helpers and the claim targets in one pass, calling _owners once per record. owner in article_by_id (:1014) is always true, because _owners returns only ids from named and those come from articles.
• impact.py:955-986: resolve each article's names once into (name, record_name) pairs, as compute_impact does at :824.
• impact.py:294-297 and :405: compute the strict map once, before the probe, and pass it in. That drops the strict_module_ownership flag. The final shape depends on the bug 4 fix.
• impact.py:1357-1358: delete. For the declared Sequence[str] input this check is unreachable, because _load_impact_evidence raises the same error before the probe.
• impact.py:432-445: inline the single-use _module_artifact_paths with (artifact_dir,) = artifact_dirs, which drops the assert. Fold this into the bug 3 fix.
• impact.py:366-386: two setdefault calls, then two strict and ... checks, keeping the same messages in the same order. This also shrinks the hunk that conflicts with Keep work impact working beside Lean files whose names are not identifiers #182.
• impact.py:228-251: let one fields tuple drive the key check and the unpacking, and replace the six type and emptiness clauses with one all(...).
• impact.py:1522-1539: one local keyed() join for both claim lines.
• impact.py:1067-1072: _module_claim_target is _helper_claim_target with a different prefix and fallback. Give the helper two defaulted parameters instead.
• __main__.py:207-214 and :227-234: register the shared --json and --timeout options in one loop. The help output does not change.
• impact.py:1040-1056: share one _json_sha256 between _build_revision and _module_graph_revision.
• impact.py:725-727: if article_local keeps its current meaning, write it as one set equality plus one all(...).

Nits

• README.md:702-708: the import-impact paragraph lacks the trusted-checkout sentence that work impact has at :690-691, though both run the same Lake evaluation and probe.
• skills/formalize/SKILL.md:72-75: "On any acquisition refusal" also covers a refused lake-build. But :51-53 says to wait on that refusal without abandoning the leaf. Say "a refused import-claim acquisition".
• impact.py:942: MODULE is validated only after the full probe. A typo costs a whole probe, and so does the work impact argument order (. --lean-root . binds . to MODULE). project_modules already has the inventory before the probe runs.
• skills/develop-plugin/SKILL.md:13-14: "Keep Cabannes-specific facts in examples and plugin and formalization roots distinct" is a garden-path sentence, and :30 dropped "releases". A fix that keeps the word count: "Keep Cabannes-specific facts in examples; keep plugin and formalization roots distinct." and "For claims/views/mirrors/pins/releases, read".
• impact.py:228: a probe line missing a field raises KeyError. _run_impact_command does not catch it, so the user sees a traceback. The tests cover only extra fields and non-list imports.
• __main__.py:746: the --timeout wiring has no test. If it were dropped, the command would silently use the 600 s default.
• impact.py:1310: work impact's "found no project-local constants" hint depends on allow_empty=require_modules, which no test covers.
• impact_probe.lean:138-139: path canonicalization has no effective test, because pytest temp paths are already canonical. A real-Lean case with a symlinked .lake would pin it.
• test_impact.py:932 duplicates the compatibility pin at :989-992.

Landing

• Onto main (cc7e3a85): merges cleanly. Ruff is clean; test_impact gives 91 passed and 2 skipped (fast suite); test_skeleton gives 144 passed; test_cli and test_skill_examples pass.
• Keep work impact working beside Lean files whose names are not identifiers #182: one conflict, in _module_source_paths, because Keep work impact working beside Lean files whose names are not identifiers #182 makes _source_modules return a tuple. Keep this PR's strict loop and iterate over _source_modules(library, snapshot)[0].items(). The resolved tree passes ruff, test_impact (95 passed fast, 97 passed with real Lean), test_skeleton, test_cli and test_skill_examples. Bug 3 describes the follow-up that whichever PR lands second needs.
• Blueprint search and reuse: phase 1 items 1-3 and 5 (#143) #171: additive conflicts in autoform_cli/README.md and autoform_cli/__main__.py, where both PRs add a block at the same spot. Keep both.
• Keep implementation notes separate from mathematical articles #172: additive conflicts. In AGENTS.md, take Keep implementation notes separate from mathematical articles #172's rewording of the roadmap bullet, followed by this PR's import bullet. In tests/test_skill_examples.py, keep both new tests.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Fixes for the four bugs, pushed as c9a48f95

The four bugs from our review of 788c6f1d are fixed on this branch, one commit each, followed by a merge of main and one follow-up commit. The push fast-forwards from 788c6f1d.

• Bug 1 (ef2eac6b, tightened in c9a48f95): import-impact now refuses instead of silently cutting the scope. Two checks, each naming the module:
  • a loaded root-package module whose OLean lies under the root artifact directory but whose source the inventory skipped (a nested checkout, an ignored directory such as build, a symlinked directory, or a spelling the inventory does not hold);
  • a module that an M.* or M.+ glob reaches, found by walking the glob directory the way Lake does, that the probe did not load. Lake builds those modules even when nothing imports them.
• Bug 3 (2c21b426): module names that need «» are matched by component on both sides, and artifact paths are built from components, so H/2_1.lean, Q/my-lemmas.lean, H/a.b.lean, R/α.lean and H/1.lean all work.
• Bug 4 (1d8197ee): the strict ownership checks cover only modules a library selects, so a library nested in another library's srcDir, and an unselected stray file in two srcDirs, no longer block every query. Two libraries that really select one file are still refused. The probe now finds a module's source by exact file existence, which fixes nested libraries on case-insensitive file systems.
• Bug 2 (67931c70): as decided for this PR, the scope stays the reverse-import closure, which covers what an added import can affect. The docstrings, README, CLI help, text report and the Formalize import workflow now say that removing an import can drop modules from the build without listing them.
• Merge of main (41b3f708): takes Keep work impact working beside Lean files whose names are not identifiers #182's _source_modules naming, keeps this branch's strict ownership loop over its first map, and keeps both sides of the README and __main__.py changes from Blueprint search and reuse: phase 1 items 1-3 and 5 (#143) #171. The probe check and the locator now key names with Keep work impact working beside Lean files whose names are not identifiers #182's _name_key, so H.α and H.«α» agree.

Validation on this branch: ruff clean; tests/test_impact.py with real Lean, 110 passed at the merge, plus the extended glob test at c9a48f95; tests/test_skeleton.py with real Lean, 172 passed; the full suite without Lean, 2058 passed. Each new regression test fails without its fix. The branch still merges cleanly into current main (93c5d282).

Left for follow-ups, all predating this PR or failing closed: work impact has the same two blind spots; the probe resolves a module's source through the first srcDir that holds the path, so a stray file ahead of the selecting library's srcDir causes a false refusal; MODULE must be spelled as Lean prints it.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Items 5 to 7 of our review are merge blockers

The four bugs from our review of 788c6f1d are fixed at 95a6f57b. The three should-fix items from that review also block the merge, and all three still hold at 95a6f57b:

• 5. A case-mismatched --lean-root is refused on macOS (autoform_cli/impact.py:444, :452). Path(lean_root).resolve() keeps the typed case, while the probe's IO.FS.realPath returns the on-disk case. On a case-insensitive file system the source and artifact comparisons therefore fail, with a message that reads like a shadowing failure.
• 6. article_local can be true while affected_claim_targets names other articles (autoform_cli/impact.py:802, :1093). An article that owns, through the parent chain, a helper in an affected module becomes a claim target without appearing in affected_articles, and owned helpers are listed nowhere, so the text report asks for a claim check with no reason given. The README's v1 contract also leaves affected_articles, selected_affected, article_local and module_claim_key undocumented.
• 7. Formalize contradicts itself on downstream edits (skills/formalize/SKILL.md:77-78 against :94-101 and :186-189). The import workflow, the claim lifecycle, AGENTS.md and impact.py:1101 all expect an import edit to acquire and repair any article that validation shows must change. The general rules still forbid modifying another article except for implementation notes and declaration revisions, and send "a change another article needs" back to Roadmap.

We are fixing all three on this branch now, each with a regression test.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Final review at 60d20dd

Verdict: merge-ready. Our review of 788c6f1d found four bugs and three should-fix items. All seven are fixed on this branch. Every code fix has a regression test; bug 2 was, by decision, documented rather than computed. CI is green on this head, including the real-Lean job, and the branch merges cleanly into main (82cca35c).

What changed since 788c6f1d

Review item	Commits	Change
Bug 1: a root module outside the snapshot inventory silently cut import edges	ef2eac6b, c9a48f95	import-impact now refuses and names the module. It refuses a loaded root-package module whose OLean lies under the root artifact directory but whose source the inventory skipped. It also refuses a module that an M.* or M.+ glob reaches, found by walking the glob directory the way Lake does, when the probe did not load it.
Bug 2: removing an import dropped modules without reporting them	67931c70	As decided for this PR, the scope stays the reverse-import closure, which covers what an added import can affect. The docstrings, the README, the CLI help, the text report and the Formalize import workflow now say that removing an import can drop modules from the build that the report does not list.
Bug 3: module names that need «» failed every query	2c21b426	Names are matched by component on both sides, and artifact paths are built from components.
Bug 4: a nested srcDir blocked every query	1d8197ee	The ownership checks cover only modules a library selects. The probe finds a module's source by exact file existence, which also fixes nested libraries on case-insensitive file systems.
5: a case-mismatched --lean-root was refused on macOS	e5e3ab4a	The source and artifact comparisons fall back to os.path.samefile, so two spellings of one file match while a different or missing file is still refused.
6: article_local could be true while other articles were claim targets	05220c70	An article that owns, through the parent chain, a helper in an affected module is listed in affected_articles, so every affected claim target has a visible reason. article_local now holds only when nothing else is a claim target, like contained in work impact. The README documents article, module_claim_key, affected_articles, selected_affected and article_local.
7: Formalize contradicted itself on downstream edits	60d20dd6	Repairing another article's Lean that a validated import edit breaks is now a listed exception, made under the revision contract's review gates, and the Roadmap rule leaves import repairs out.
Style	95a6f57b	One CLI handler for work impact and work import-impact, docstrings that match the code, rewrapped docs, and a shared _lake_build test helper.
Merges of main	41b3f708, a2b5018a	Takes #182's module naming and keeps both sides of the #171 and #172 documentation changes.

Validation

• CI at 60d20dd6: the pull-request run passes all four jobs (Python 3.10, Python 3.13, real Lean with the fixture toolchain, and the Windows hardening job), and so did the push run of the same commit on the scratch branch swarm/183-blockers. On this branch's push run, the real-Lean job timed out in its "Install the fixture's Lean toolchain" step, before any repository code ran; that job has been re-run.
• The tests for bugs 1, 3 and 4 were checked locally to fail without their fixes. At the first merge of main, real-Lean tests/test_impact.py passed (110 tests), real-Lean tests/test_skeleton.py passed (172), and the full suite without Lean passed (2058). The style pass and the fixes for items 5 to 7 were checked by CI only, because the machine we test on was overloaded.

Follow-ups, not blockers

• Test gaps from our first review that remain: the exact module_claim_target value, two libraries sharing srcDir ., the default text output of work import-impact through the CLI (every successful CLI test passes --json), an article with no lean: declaration, and the --timeout wiring for import-impact.
• work impact has the same two blind spots this PR closes for import-impact: a loaded root module outside the inventory, and an unimported glob module in a directory the inventory skips.
• The probe takes a module's source from the first srcDir that holds the path, so a stray file in an earlier srcDir gives a false refusal. It fails closed.
• MODULE must be spelled as Lean prints it, so H.2_1 is refused where H.«2_1» works.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Still merge-ready at 3c4631e

3c4631e3 merges main (b1b00941) into this branch to clear new conflicts in autoform_cli/skeleton.py and autoform_cli/impact.py. lean_libraries now computes both this branch's root artifact directory and main's package srcDir (#248). Main's resolve_lean_root change (#231) landed in _load_impact_evidence. No other code changed since the final review at 60d20dd6. CI passes at 3c4631e3 on both the push and pull-request runs, real Lean included, and the branch still merges cleanly into current main (41330b40). The verdict stands: merge-ready.

Posted by PR swarm: PR Swarm Lead