Keep work impact working beside Lean files whose names are not identifiers

[Deicyde]

Follow-up to #136. Re-reviewing it after it merged, I found one problem a user can hit and two error-path nits. All three still reproduce on main 4c80749.

What a user sees. A Finder duplicate such as Demo/Basic copy.lean under a library's srcDir made autoform work impact exit 2 with invalid Lean declaration name: 'Demo.Basic copy', even though no root or glob selects that file. With this PR the impact report comes out as usual.

• Non-identifier module names (5a11922, impact.py). project_modules counts every source module under a library as local, and the probe spelled each name with _lean_name, which cannot parse Demo.Basic copy. _source_modules now quotes components that are not plain identifiers the way Lean does (Demo.«Basic copy»), so constants from that module stay local and keep their impact. The module-to-path lookup compares names by component, so Demo.α, which Lean prints unquoted, still finds its file. A dotted stem such as Demo/Foo.Bar.lean is now the single component «Foo.Bar», as in Lean, so a Demo.Foo.* glob no longer selects it as Demo.Foo.Bar, and Demo/..lean is Demo.«.» (with_suffix("") rejects that stem on Python 3.13). A component containing » has no quoted spelling: Lake still builds Demo/«Foo».lean, but no import can name it, so such files are never local, and a glob that selects one is refused as it is on main. The glob branch refuses every quoted module, so the probe imports nothing new.
• lake not on PATH (9a2d26f, skeleton.py). The message said "a built Lean project is required to extract skeletons" for the impact probe too. It now names the probe's purpose, like the neighboring messages: "lake is not on PATH; running the impact probe requires a built Lean project".
• An unresolvable --lean-root (4139fee, lean.py, skeleton.py, audit.py). expanduser() raises RuntimeError for an unknown ~user on every Python version, and before 3.13 resolve() raises it for a symbolic link loop; check, audit, and skeleton crashed with a traceback on either. check now prints "Lean sources could not be indexed: Lean root cannot be resolved" (index errors never show host paths), skeleton names the root and the cause, and audit reports its existing invalid-lean-root finding. work list, work context, work impact, and doctor already handled both. This one predates Report Lean revision impact and deprecated targets #136.

Tests, in tests/test_impact.py: test_unselected_source_with_a_quoted_module_name_stays_local (Basic copy.lean, α.lean, ..lean, x»y.lean), test_project_modules_read_a_dotted_file_stem_as_one_component (Foo.Bar.lean and Foo.x»y.lean beside a Demo.Foo.* glob), two test_project_modules_fail_closed cases where a glob selects «Foo».lean or x»y.lean, and the extended test_impact_probe_freshness_messages_never_mention_skeletons. In tests/test_cli.py: test_lean_root_commands_report_an_unresolvable_root_without_traceback, which runs check, audit, and skeleton against both roots on every Python version (on 3.13 check fails later for the loop, when it reads the sources, with the same prefix).

Not changed: render has the same crash for --lean-root, and for its blueprint and output paths. #165, which rewrites render, already guards all three, so this PR leaves render.py alone rather than conflict with it.

Overlap: merges cleanly with every open PR except three. #140 and #141 already conflict with main in 24 files; this adds 3 hunks to their tests/test_impact.py conflict. #75 conflicts with main only in skills/setup/SKILL.md; this adds a one-hunk conflict in tests/test_cli.py.

Validation at 4139fee: locally, the full suite on Python 3.13 and 3.10 (1855 passed, 56 skipped, 1 xfailed each), the real-Lean impact tests (77 passed), ruff check, and make check-example. The real-Lean skeleton and open-statement jobs (173 passed; 95 passed, 1 skipped) last ran before a final change to _source_modules and its tests, which they do not exercise.

[Deicyde]

Review at 4139fee

Verdict: merge-ready. The quoting, the component-keyed locator and the three error-path fixes are correct on main, and CI is green at this head. It also fixes one silent drop the body doesn't claim (test gap 1). The interaction with #183 that item 3 of the posted #183 review predicts is real. The fix belongs in #183, which needs the same change for its own bug 3 anyway. Details are under Landing.

Test gaps

1. Digit-leading module components are fixed but not pinned (autoform_cli/impact.py:266)

On main, Demo/1.lean is keyed Demo.1, and _lean_name renders it into the probe's projectModules as Name.num (Name.str (Name.anonymous) "Demo") 1. Lean names that module Name.str "1", because an import can only spell it Demo.«1». isLocalModule never matches, so the probe emits no record for any constant in that module and drops every use edge through it. work impact then reports a smaller impact than the real one, and nothing errors. At this head the component fails _MODULE_COMPONENT, gets quoted, and renders as Name.str (...) "1".

• Repro: a project with Demo.lean and Demo/1.lean. project_modules + render_impact_probe give Name.num ... 1 on main and Name.str ... "1" at this head. On real Lean 4.34.1, import Demo.«1» loads a module whose last component is Name.str "1", and m == Name.num Demo 1` is false.
• Teeth: a mutant at :266 that quotes only components _lean_name_parts cannot read (re.fullmatch(r"[^.\s«»]+", part)) brings Name.num back. It passes all 38 test_impact.py tests that touch module naming (-k "project_modules or quoted or located or source or probe"). No test in tests/ names a digit-leading module file.
• Fix: add 1.lean to test_unselected_source_with_a_quoted_module_name_stays_local, and assert that 'Name.str (Name.str (Name.anonymous) "Demo") "1"' is in the probe.

Landing

• main (89dff279): merges cleanly.

• Allow proof imports with measured impact #183: one textual conflict, in _module_source_paths. Keep Allow proof imports with measured impact #183's strict loop and iterate over _source_modules(library, snapshot)[0].items(). There is also a semantic interaction that the textual resolution doesn't fix. Allow proof imports with measured impact #183's _validated_module_evidence looks up Lean's Name.toString spelling of each loaded module by string (impact.py:408 at 788c6f1d). It builds the expected artifact path with module.split(".") (:443). This PR changes the keys from raw path parts to quoted spellings. Measured with real _validated_module_evidence calls on module evidence that uses Lean's spellings:

  source	Allow proof imports with measured impact #183 alone	Allow proof imports with measured impact #183 + Keep work impact working beside Lean files whose names are not identifiers #182
  R/α.lean (Lean prints R.α)	OK	refused at :408, "loaded R.α without a captured root-project source"
  R/2_1.lean (R.«2_1»)	refused at :408	refused by the artifact check (:421, path from :443), expects R/«2_1».olean
  R/my-x.lean (R.«my-x»)	refused at :408	refused by the artifact check, expects R/«my-x».olean
  R/1.lean (R.«1»)	silently dropped: Name.num is never local, so no evidence and no import edges (bug 1 of the Allow proof imports with measured impact #183 review)	refused by the artifact check, expects R/«1».olean

  The R/1.lean cell for Allow proof imports with measured impact #183 alone comes from the probe's isLocalModule gate (impact_probe.lean:134 at 788c6f1d), not from a call. So R/α.lean regresses after both PRs land, and the other three still fail, now with a different message. required_modules is not affected: it is the probe's plain imports plus Lean-printed record modules.

  Allow proof imports with measured impact #183 should carry the fix. The cause is Allow proof imports with measured impact #183's string comparison, which is already wrong for quoted names without this PR (its bug 3). _name_key exists on main, so Allow proof imports with measured impact #183 can use it now. With a component-keyed lookup, landing order stops mattering. If Allow proof imports with measured impact #183 lands first without the fix, this PR must carry it when rebasing, or R/α.lean regresses. The change below was applied to Allow proof imports with measured impact #183 alone and to the Keep work impact working beside Lean files whose names are not identifiers #182+Allow proof imports with measured impact #183 merge. On the merge, all four rows validate, and test_impact.py without Lean gives 95 passed, 2 skipped. On Allow proof imports with measured impact #183 alone, α, 2_1 and my-x validate. R/1.lean there still needs this PR's quoting to become local at all.
  Allow proof imports with measured impact #183 has no test in which a local module with a non-plain name passes validation. The fix should land with stub-probe cases for the rows above, as bug 3 of the Allow proof imports with measured impact #183 review already asks.

  source_paths = _module_source_paths(libraries, snapshot, strict=True)
  expected_paths = {_name_key(name): path for name, path in source_paths.items()}
  expected_artifacts = {
      _name_key(name): path for name, path in _module_artifact_paths(libraries, source_paths).items()
  }
  for module, record in evidence.items():
      relative = expected_paths.get(_name_key(module))
      ...
      expected_artifact = expected_artifacts[_name_key(module)]
  # _module_artifact_paths: build from components, not module.split(".") / with_suffix
      module: artifact_dir.joinpath(*parts[:-1], parts[-1] + ".olean").resolve()
      for module in source_paths
      for parts in [[part for part, _quoted in _lean_name_parts(module)]]

• Share the leaf filter in work and the parent walk in impact, and inline two skeleton checks #187: merges cleanly in either order, and the two touch disjoint functions. This PR edits project_modules, _source_modules, _module_source_paths and _locator in impact.py, plus run_probe and extract_skeletons in skeleton.py. Share the leaf filter in work and the parent walk in impact, and inline two skeleton checks #187 edits _owners, _descends_from and _users_through_internal in impact.py, _report_entry in skeleton.py, and list_ready_work in work.py. On main + Keep work impact working beside Lean files whose names are not identifiers #182 + Share the leaf filter in work and the parent walk in impact, and inline two skeleton checks #187, ruff is clean. test_impact.py, test_work.py and test_cli.py without Lean give 113 passed, 1 skipped.

• Add verified statement-review bundles #75: adds one conflict in tests/test_cli.py, in the import block. Both PRs add import pytest, and Add verified statement-review bundles #75 also adds import autoform_cli.__main__ as cli. Take Add verified statement-review bundles #75's side. Its other conflicts already exist against main.

• Deploy Pages only after autoform verify passes, and refuse a lean: name defined twice #140, Bind statement: formalized to a recorded statement_hash #141, Rebuild artifact verification on bound project evidence #145, Scale roadmap inventories and the full DAG explorer #90: no conflict beyond what each already has against main. skeleton: read lakefile.lean when both lakefiles exist #189, Report unclosed Markdown fences during audit #202, Keep implementation notes separate from mathematical articles #172: clean.

Posted by PR swarm: Review #182 #185 #187