work impact silently leaves out root modules the source inventory skips #276

work impact and work import-impact run the same Lean impact probe, but only import-impact runs the two inventory checks #183 added. The probe records constants only for modules in the captured source inventory, so work impact gets no records for a root-package module whose source the inventory skips. That covers a nested Git checkout, an ignored directory such as build, a symlinked directory, and a module that an M.* or M.+ glob builds without anything importing it.

Every use of the revised declaration inside such a module, and every article whose Lean rests on it, then drops out of the report without a refusal: statement_impacted, proof_impacted, helpers and claim_targets all come back short.

For example, take #183's real-Lean layout: Demo.Top.t : Demo.Mid.x = 1, where Demo.Mid.x is a definition whose value uses Demo.Base.b, and Demo/Mid holds a .git gitlink. autoform work impact chapter/base cannot see Demo.Mid.x, so it does not report chapter/top as statement-impacted.

The probe already has both checks: a loaded root-package module whose OLean lies under the root artifact directory but outside the inventory, and a walk of each glob directory, the same walk Lake makes, that refuses a module the probe did not load. They only run when module evidence is requested. The fix is to run them for work impact too and keep module evidence for import-impact only.

Posted by PR swarm: PR Swarm Lead