reassemble: dependency-aware deletion, per-unit neighbour pruning, combo audit

reassemble/LeanReassemble/Main.lean

@@ -18,19 +18,33 @@ Usage:
   lean_reassemble materialize-units --source-root <lake-project>
     --records <declarations.jsonl> --output <artifact-dir>
     [--build-target <target>] [--proofs sorry|keep|delete]
+    [--manifest <manifest.json>] [--on-failure fail|skip|backoff]
 
 --proofs sorry (default) replaces each selected theorem's proof with `by sorry`.
 --proofs keep preserves the proofs verbatim, producing the compilable REFERENCE
 state of the same records: every record is still matched to its declaration and
 its proof range validated, so the artifact is evidence that the extraction agrees
 with the source. Use it to get an intermediate, fully-compiling checkout from an
 extractor run, or as the oracle to diff a sorried artifact against.
---proofs delete erases each selected declaration outright. It does no dependency
-analysis: deleting a theorem others reference will break the build.
+--proofs delete erases each selected declaration outright. materialize-repo and
+materialize-units check the records' `deps` BEFORE building and fail — naming each
+`dependent -> deleted` pair — when a surviving declaration would be left referencing
+a deleted theorem, rather than deferring to an opaque build break. (A --proofs sorry
+dependent is safe: its proof, and the references in it, are holed out. Deletes
+introduced by --on-failure backoff are not covered by this pre-flight and still
+surface at the final build.)
 
 --manifest <path> is a sparse per-theorem override: a JSON object mapping theorem
 names to keep|sorry|delete. Theorems it does not name follow --proofs.
 
+In materialize-units the manifest does double duty: the action on a UNIT'S TARGET
+theorem selects whether that unit is emitted (sorry -> hole and emit; keep/delete ->
+excluded), while a `delete` on a SAME-MODULE neighbour removes that neighbour from
+the emitted unit's file. A run that emits no task at all (e.g. a whole-run
+--proofs delete or keep) is an error, not an empty success. --build-target in
+materialize-units scopes only the pristine warm-up build that fills the shared
+cache, not the per-unit builds.
+
 --on-failure fail (default) aborts on the first theorem that fails to reassemble.
 skip omits it (recorded as skipped); backoff deletes it (recorded as failed) and
 continues. Both recover from PLANNING failures; a post-rewrite build break in
@@ -104,7 +118,13 @@ private def parseRewriteArgs (args : List String) : Except String RewriteConfig
     | flag :: _ => throw s!"unknown or incomplete argument: {flag}"
   go args none none none none none .replace .fail
 
-private def parseMaterializeArgs (args : List String) : Except String MaterializeConfig := do
+/-- Parse the shared `materialize-{repo,units}` arguments. `allowRepoFlags` gates the
+two flags that only `materialize-repo` honors: `--keep-eval` (eval-strip opt-out) and
+`--in-process` (isolation off). Both are inert in units mode — a unit is a single
+standalone module with its own build model — so they are rejected there as unknown
+arguments rather than silently accepted. -/
+private def parseMaterializeArgs (allowRepoFlags : Bool) (args : List String)
+    : Except String MaterializeConfig := do
   let rec go (remaining : List String) (sourceRoot records output buildTarget : Option String)
       (manifest : Option String) (mode : ProofMode) (onFailure : FailurePolicy)
       (keepEval : Bool) (isolated : Bool)
@@ -136,16 +156,22 @@ private def parseMaterializeArgs (args : List String) : Except String Materializ
     | "--on-failure" :: value :: tail => do
         go tail sourceRoot records output buildTarget manifest mode (← parseFailurePolicy value) keepEval isolated
     | "--keep-eval" :: tail =>
-        go tail sourceRoot records output buildTarget manifest mode onFailure true isolated
+        if allowRepoFlags then
+          go tail sourceRoot records output buildTarget manifest mode onFailure true isolated
+        else throw "--keep-eval is not valid for materialize-units (nothing to strip: a \
+          unit is a single standalone module); it applies to materialize-repo"
     | "--in-process" :: tail =>
-        go tail sourceRoot records output buildTarget manifest mode onFailure keepEval false
+        if allowRepoFlags then
+          go tail sourceRoot records output buildTarget manifest mode onFailure keepEval false
+        else throw "--in-process is not valid for materialize-units (units have their own \
+          per-target build model); it applies to materialize-repo"
     | flag :: _ => throw s!"unknown or incomplete argument: {flag}"
   go args none none none none none .replace .fail false true
 
 private def parseArgs : List String → Except String Command
   | "rewrite-file" :: rest => .rewriteFile <$> parseRewriteArgs rest
-  | "materialize-repo" :: rest => .materializeRepo <$> parseMaterializeArgs rest
-  | "materialize-units" :: rest => .materializeUnits <$> parseMaterializeArgs rest
+  | "materialize-repo" :: rest => .materializeRepo <$> parseMaterializeArgs (allowRepoFlags := true) rest
+  | "materialize-units" :: rest => .materializeUnits <$> parseMaterializeArgs (allowRepoFlags := false) rest
   | command :: _ => .error s!"unknown command: {command}"
   | [] => .error "command is required"
 

reassemble/LeanReassemble/Materialize.lean

@@ -350,6 +350,14 @@ unsafe def materializeRepo (config : MaterializeConfig) : IO Unit := do
   let theorems ← eligibleTheorems records
   let manifest ← loadManifest config.manifestPath theorems
   let modeFor := fun name => manifest.actionFor name config.proofMode
+  -- Fail fast on declared deletes that would strand a surviving reference, naming the
+  -- offending pairs — rather than letting the whole-tree `lake build` below report an
+  -- opaque break at a dependent with no attribution. Pure over the records, so it runs
+  -- before the expensive copy and leaves no half-written artifact behind. (`backoff`
+  -- deletes discovered during planning are not visible here; those still fall through
+  -- to the build, per the failure-policy contract.)
+  let conflicts := danglingReferences records modeFor
+  unless conflicts.isEmpty do fail (dependencyConflictMessage conflicts)
   let name ← projectName sourceRoot
   let repoRel : System.FilePath := ("repos" : System.FilePath) / name
   let repoRoot := artifact / repoRel
@@ -465,7 +473,11 @@ unsafe def materializeRepo (config : MaterializeConfig) : IO Unit := do
     ("repository", artifactPath repoRel),
     ("build_target", toJson config.buildTarget),
     ("rewrite_summary", rewriteSummary config.proofMode theorems.size counts failures),
-    ("verification", Json.mkObj [("status", "passed")])
+    -- Record the exact build command so a scoped `--build-target` verification is
+    -- never mistaken for a whole-project one: a break in a module outside the target
+    -- is not compiled, so "passed" means "passed for this command", not "for the tree".
+    ("verification", Json.mkObj [("status", "passed"), ("command",
+      String.intercalate " " (["lake", "build"] ++ config.buildTarget.toList))])
   ]
 
 private def splitSearchPath (value : String) : Array System.FilePath :=
@@ -702,11 +714,19 @@ unsafe def materializeUnits (config : MaterializeConfig) : IO Unit := do
     let targetMode := manifest.actionFor record.name config.proofMode
     -- A unit is the problem "reconstruct THIS theorem", so a `delete` target has no
     -- task to emit: deleting the very theorem a unit would ask a solver to prove is
-    -- meaningless. Record it in the summary and move on. (`keep`/`sorry` neighbours
-    -- are irrelevant here — a unit only ever touches its own target.)
+    -- meaningless. Record it in the summary and move on.
     if targetMode == .delete then
       counts := counts.bump .delete
       continue
+    -- A `keep` target holes nothing, so its "task" would be the unmodified module — a
+    -- prove-nothing unit. Exclude it (counted as preserved) with a warning rather than
+    -- ship a degenerate task; an all-keep run then trips the empty-artifact guard below
+    -- and fails honestly instead of reporting success over no tasks.
+    if targetMode == .keep then
+      counts := counts.bump .keep
+      IO.eprintln s!"lean-reassemble: skipping keep target {record.name} \
+        (a keep unit holes nothing — there is nothing to reconstruct)"
+      continue
     -- A `where`/`let rec` helper or `mutual` member has no standalone declaration to
     -- reconstruct, so it is not a valid unit target ("prove this helper in isolation"
     -- is meaningless — it only exists inside its parent). Exclude it, like `delete`.
@@ -722,12 +742,30 @@ unsafe def materializeUnits (config : MaterializeConfig) : IO Unit := do
       let file := normalizeRelativePath record.file.get!
       let some prepared := preparedByFile[file]?
         | fail s!"prepared source missing for {record.name}"
-      -- A unit is a task for ONE theorem: hole out only this record's proof and
-      -- leave every other declaration in the module intact. Rewriting the whole
-      -- file's records here would sorry the target's neighbours too — including
-      -- lemmas its own proof depends on — and would make every task from a given
-      -- file byte-identical.
-      let rewritten ← rewritePreparedFile prepared #[record] targetMode
+      -- A unit holes its own target and, when the manifest marks same-module
+      -- neighbours `delete`, removes those neighbour declarations too. Kept/unlisted
+      -- neighbours (default `keep`) stay proven and need no edit; a neighbour `sorry`
+      -- is treated as keep — a unit only ever holes its own target. Only SAME-module
+      -- neighbours are prunable: cross-module references resolve from the shared cache,
+      -- not this file. Holing the target's own proof (rather than the whole file) is
+      -- what keeps each task distinct and its depended-on lemmas intact.
+      let deleteNeighbour := fun (t : Corpus.ConstRecord) =>
+        t.name != record.name && t.module == record.module &&
+          manifest.actions.getD t.name .keep == .delete
+      let neighbours := theorems.filter deleteNeighbour
+      -- Before editing, reject a prune that would strand a surviving neighbour (or a
+      -- def) on a removed one, naming the pairs — the per-unit analogue of the repo
+      -- check, scoped to this module. The target is `.replace` here, so it is never a
+      -- flagged dependent. Inside the `try`, so `--on-failure` governs it: `fail`
+      -- aborts, `skip`/`backoff` omit this unit and record the reason.
+      let unitResolve := fun name =>
+        if name == record.name then targetMode
+        else if manifest.actions.getD name .keep == .delete then .delete else .keep
+      let conflicts := danglingReferences records unitResolve (moduleFilter := some record.module)
+      unless conflicts.isEmpty do fail (dependencyConflictMessage conflicts)
+      let selected := #[record] ++ neighbours
+      let unitModeFor := fun name => if name == record.name then targetMode else .delete
+      let rewritten ← rewritePreparedFile prepared selected targetMode (modeFor := unitModeFor)
       if rewritten.moduleName.toString != record.module then
         fail s!"module mismatch for {record.name}"
       let some span := replacementSpan? rewritten.edits record.name
@@ -767,14 +805,18 @@ unsafe def materializeUnits (config : MaterializeConfig) : IO Unit := do
       let sorryWarnings := (diagnostics.splitOn "\n").filter
         (fun line => line.contains "warning:" && line.contains "declaration uses `sorry`")
       let sourceSorryCount := sourceSorryCountFor records file
+      -- Deleted neighbours that were ALREADY incomplete in the source no longer emit
+      -- their own `sorry` warning (we removed the whole declaration), so drop them from
+      -- the baseline the count is measured against.
+      let removedIncomplete := (neighbours.filter (·.axioms.contains "sorryAx")).size
+      let baseline := sourceSorryCount - removedIncomplete
       let expectedSorries :=
-        -- `.keep` adds nothing (delete emits no task, so it never reaches here). Only
-        -- `.replace` introduces a fresh sorry.
-        if targetMode == .keep then sourceSorryCount
+        -- Only `.replace` introduces a fresh sorry (the target is always `.replace`
+        -- here; `keep`/`delete` targets were excluded above).
         -- The target itself is holed out; if it was already incomplete it is counted
         -- in the baseline, so it must not be counted twice.
-        else if record.axioms.contains "sorryAx" then sourceSorryCount
-        else sourceSorryCount + 1
+        if record.axioms.contains "sorryAx" then baseline
+        else baseline + 1
       if sorryWarnings.length > expectedSorries then
         fail s!"{record.name}: {sorryWarnings.length} `sorry` warning(s) but at most \
           {expectedSorries} expected for proof mode {targetMode} \
@@ -822,6 +864,14 @@ unsafe def materializeUnits (config : MaterializeConfig) : IO Unit := do
       IO.eprintln s!"lean-reassemble: {action} {record.name}: {reason}"
       failures := failures.push { name := record.name, action, reason }
   removeIfExists (artifact / ".work")
+  -- An artifact with no tasks is not a success: every eligible theorem resolved to
+  -- delete/keep/auxiliary (e.g. a whole-run `--proofs delete`/`keep`), so there is
+  -- nothing to reconstruct. Fail rather than write a `manifest.json` reporting
+  -- `verification: passed` over zero tasks. (`skip`/`backoff` runs that legitimately
+  -- omit some units still succeed as long as at least one task remains.)
+  if tasks.isEmpty then
+    fail s!"materialize-units produced no tasks: all {theorems.size} eligible \
+      theorem(s) resolved to delete/keep/auxiliary — nothing to reconstruct"
   let name ← projectName sourceRoot
   writeJson (artifact / "manifest.json") <| Json.mkObj [
     ("format", "lean-corpus-reassembly.v1"),

reassemble/LeanReassemble/Rewrite.lean

@@ -372,6 +372,57 @@ def planEdits (frontendResult : Corpus.Frontend.ElabResult)
     fail reason
   return outcome.edits
 
+/-- Full names the run resolves to `.delete`. Only theorem records are deletable —
+a `def`/`inductive`/`structure` is never holed or removed — so `modeFor` (which
+returns the default action for any name it does not override) is only consulted for
+theorem names here. `moduleFilter`, when set, restricts the set to one module:
+`materialize-units` removes only a target's SAME-module neighbours. -/
+def deletedNames (records : Array Corpus.ConstRecord)
+    (modeFor : String → ProofMode) (moduleFilter : Option String := none)
+    : Std.HashSet String := Id.run do
+  let mut result : Std.HashSet String := {}
+  for record in records do
+    if Corpus.Artifact.isTheoremRecord record && moduleFilter.all (· == record.module) then
+      if modeFor record.name == .delete then
+        result := result.insert record.name
+  return result
+
+/-- `(dependent, deleted)` pairs where a SURVIVING declaration's `deps` names a
+theorem the run deletes — the deletions that would break the build.
+
+A survivor is any non-theorem record (defs/inductives/structures are never removed)
+or a theorem resolved to `.keep`. A `.replace` (holed) theorem is deliberately NOT
+a survivor: its proof becomes `by sorry`, which drops the references it carried, so
+a holed dependent cannot dangle. Deleted names are always theorems, and theorems
+are referenced from proofs, so this direct-`deps` check is complete over transitive
+chains: every hop is itself a record we evaluate (S→M→D is caught as M→D if M
+survives, or as S→M if M is itself deleted).
+
+`moduleFilter` restricts BOTH the delete-set and the dependents to one module —
+units prunes same-module neighbours only, and cross-module references resolve from
+the prebuilt shared cache rather than the unit's file. -/
+def danglingReferences (records : Array Corpus.ConstRecord)
+    (modeFor : String → ProofMode) (moduleFilter : Option String := none)
+    : Array (String × String) := Id.run do
+  let deleted := deletedNames records modeFor moduleFilter
+  if deleted.isEmpty then return #[]
+  let mut pairs := #[]
+  for record in records do
+    unless moduleFilter.all (· == record.module) do continue
+    let survives :=
+      if Corpus.Artifact.isTheoremRecord record then modeFor record.name == .keep else true
+    if survives then
+      for dep in record.deps do
+        if deleted.contains dep then
+          pairs := pairs.push (record.name, dep)
+  return pairs
+
+/-- One fail-fast message naming every `dependent -> deleted` pair. -/
+def dependencyConflictMessage (pairs : Array (String × String)) : String :=
+  let lines := pairs.toList.map fun (dependent, deleted) => s!"  {dependent} -> {deleted}"
+  s!"dependency conflict: {pairs.size} surviving declaration(s) reference deleted \
+    theorem(s); deleting would break the build:\n{String.intercalate "\n" lines}"
+
 /-- Delete-edits that erase every evaluation command (`#eval`, `#eval!`, `#reduce`,
 `#guard`, `#guard_msgs`) in an elaborated file.
 

reassemble/README.md

@@ -123,6 +123,15 @@ Keys are full theorem names (the same names the records carry); values are
 `keep | sorry | delete`. A key that matches no theorem in the records is a hard
 error, to catch typos.
 
+Deleting a theorem that a surviving declaration still references would break the
+build. `materialize-repo` and `materialize-units` detect this from the records'
+`deps` **before** building and fail with the offending `dependent -> deleted`
+pairs named, rather than deferring to an opaque `lake build` error (a
+`--proofs sorry` dependent is safe — its proof, and the references in it, are
+holed out). For the full account of which parameter combinations are supported,
+degenerate, or rejected — including the manifest's neighbour-pruning role in
+units mode — see [`docs/parameter-matrix.md`](../docs/parameter-matrix.md).
+
 ## Failure Policy
 
 `--on-failure` controls what happens when a theorem cannot be reassembled — it does