diff --git a/reassemble/LeanReassemble/Main.lean b/reassemble/LeanReassemble/Main.lean index 393ab11..5787e1d 100644 --- a/reassemble/LeanReassemble/Main.lean +++ b/reassemble/LeanReassemble/Main.lean @@ -18,6 +18,7 @@ Usage: lean_reassemble materialize-units --source-root --records --output [--build-target ] [--proofs sorry|keep|delete] + [--manifest ] [--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 @@ -25,12 +26,25 @@ 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 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" diff --git a/reassemble/LeanReassemble/Materialize.lean b/reassemble/LeanReassemble/Materialize.lean index 3d9a011..82f12a8 100644 --- a/reassemble/LeanReassemble/Materialize.lean +++ b/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"), diff --git a/reassemble/LeanReassemble/Rewrite.lean b/reassemble/LeanReassemble/Rewrite.lean index e63e7ef..e9ae8e1 100644 --- a/reassemble/LeanReassemble/Rewrite.lean +++ b/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. diff --git a/reassemble/README.md b/reassemble/README.md index 6f4063c..3b96330 100644 --- a/reassemble/README.md +++ b/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 diff --git a/reassemble/ReassembleTests.lean b/reassemble/ReassembleTests.lean index 88ee7a0..7daefc6 100644 --- a/reassemble/ReassembleTests.lean +++ b/reassemble/ReassembleTests.lean @@ -674,6 +674,124 @@ private unsafe def testUnitFailurePolicies : IO Unit := do removeDirIfExists failOut if ← recordsPath.pathExists then IO.FS.removeFile recordsPath +/-- The shared dependency-conflict detector `danglingReferences`, over records with a +real theorem→theorem edge (`Fixture.Deps.mid` uses `Fixture.Deps.base`). It flags a +SURVIVING declaration that references a deleted theorem — a kept theorem or any def — +and nothing else: a holed (`sorry`) dependent drops its references, and a +`moduleFilter` scopes the check. -/ +private def testDanglingReferences (deps : Array Corpus.ConstRecord) : IO Unit := do + let base := "Fixture.Deps.base" + let mid := "Fixture.Deps.mid" + -- Delete `base`, keep `mid`: mid → base is a dangling reference. + let deleteBaseKeepMid := fun name => + if name == base then LeanReassemble.ProofMode.delete + else if name == mid then .keep else .replace + let conflicts := LeanReassemble.danglingReferences deps deleteBaseKeepMid + assertIO (conflicts.size == 1 && conflicts.any (fun (d, t) => d == mid && t == base)) + "danglingReferences flags a kept theorem referencing a deleted one" + -- Same delete, but `mid` is holed: its `by sorry` body drops the reference. + let deleteBaseSorryMid := fun name => + if name == base then LeanReassemble.ProofMode.delete else .replace + assertIO (LeanReassemble.danglingReferences deps deleteBaseSorryMid).isEmpty + "a holed (sorry) dependent does not dangle" + -- A surviving def (never holed) that references a deleted theorem IS flagged. + let midRec := (deps.filter (·.name == mid))[0]! + let defRec := { midRec with name := "Fixture.Deps.usesBase", kind := "def", deps := [base] } + let defConflicts := LeanReassemble.danglingReferences (deps.push defRec) deleteBaseSorryMid + assertIO (defConflicts.any (fun (d, t) => d == "Fixture.Deps.usesBase" && t == base)) + "a surviving def referencing a deleted theorem is flagged" + -- `moduleFilter` restricts the check to one module. + assertIO (LeanReassemble.danglingReferences deps deleteBaseKeepMid + (moduleFilter := some "Other.Module")).isEmpty + "moduleFilter restricts the check to one module" + -- No deletes → no conflicts; the message names both members of each pair. + assertIO (LeanReassemble.danglingReferences deps (fun _ => .replace)).isEmpty + "no deletes means no conflicts" + let msg := LeanReassemble.dependencyConflictMessage #[(mid, base)] + assertIO (msg.contains mid && msg.contains base) "conflict message names both members" + +/-- End-to-end dependency-conflict handling over `TestProject` using the +`records-deps.jsonl` fixture (a real `mid → base` edge). Covers the three regressions +the audit found — repo delete-with-kept-dependent, units `--proofs delete`, units +`--proofs keep` — plus the per-unit conflict. -/ +private unsafe def testDependencyConflicts : IO Unit := do + let pid ← IO.Process.getPID + let sourceRoot : System.FilePath := "TestProject" + let records : System.FilePath := sourceRoot / "records-deps.jsonl" + let out : System.FilePath := s!"/tmp/lean-reassemble-depconflict-{pid}" + let mp : System.FilePath := s!"/tmp/lean-reassemble-depmanifest-{pid}.json" + let deleteBaseKeepMid := + "{\"theorems\":{\"Fixture.Deps.base\":\"delete\",\"Fixture.Deps.mid\":\"keep\"}}" + removeDirIfExists out + try + -- repo: delete `base` while keeping `mid` → fail fast, before any lake build, naming + -- the pair (not an opaque lake error). + IO.FS.writeFile mp deleteBaseKeepMid + let repoErr ← try + LeanReassemble.materializeRepo { + sourceRoot, records, output := out, manifestPath := some mp } + pure "" + catch e => pure e.toString + assertIO (repoErr.contains "dependency conflict" && repoErr.contains "Fixture.Deps.mid" + && repoErr.contains "Fixture.Deps.base") + "repo conflict names the dependent → deleted pair" + removeDirIfExists out + -- units: whole-run `--proofs delete` → every target deleted → no tasks (not a + -- silent empty artifact reported as passed). + expectFailure "units --proofs delete yields no tasks" do + LeanReassemble.materializeUnits { + sourceRoot, records, output := out, proofMode := .delete } + assertIO (!(← (out / "units").pathExists)) "no units directory for an all-delete run" + removeDirIfExists out + -- units: whole-run `--proofs keep` → every target excluded → no tasks. + expectFailure "units --proofs keep yields no tasks" do + LeanReassemble.materializeUnits { + sourceRoot, records, output := out, proofMode := .keep } + removeDirIfExists out + -- units: per-unit conflict. Deleting `base` while keeping `mid` poisons every unit + -- in the module; under `fail` the run aborts naming the pair. + IO.FS.writeFile mp deleteBaseKeepMid + let unitErr ← try + LeanReassemble.materializeUnits { + sourceRoot, records, output := out, manifestPath := some mp } + pure "" + catch e => pure e.toString + assertIO (unitErr.contains "dependency conflict" && unitErr.contains "Fixture.Deps.mid") + "per-unit conflict names the dependent → deleted pair" + finally + removeDirIfExists out + if ← mp.pathExists then IO.FS.removeFile mp + +/-- The new units capability: a manifest `delete` on a same-module NEIGHBOUR removes +that declaration from every unit in the module, while the target stays holed and the +other neighbours stay proven. Deleting the leaf `Fixture.Deps.leaf` (nothing depends +on it) must succeed, and each emitted unit must still build. -/ +private unsafe def testUnitNeighbourPruning : IO Unit := do + let pid ← IO.Process.getPID + let sourceRoot : System.FilePath := "TestProject" + let records : System.FilePath := sourceRoot / "records-deps.jsonl" + let out : System.FilePath := s!"/tmp/lean-reassemble-prune-{pid}" + let mp : System.FilePath := s!"/tmp/lean-reassemble-prunemanifest-{pid}.json" + removeDirIfExists out + try + IO.FS.writeFile mp "{\"theorems\":{\"Fixture.Deps.leaf\":\"delete\"}}" + LeanReassemble.materializeUnits { + sourceRoot, records, output := out, manifestPath := some mp } + -- `leaf` is a delete target → no task; `base` (0) and `mid` (2) each get a unit. + assertIO (!(← (out / "units" / "1-Fixture.Deps.leaf").pathExists)) + "no unit for the deleted leaf target" + let midUnit := out / "units" / "2-Fixture.Deps.mid" + let midSrc ← IO.FS.readFile (midUnit / "Fixture" / "Deps.lean") + assertIO (!midSrc.contains "theorem leaf") "neighbour leaf pruned from mid's unit" + assertIO (midSrc.contains "theorem base") "kept neighbour base survives in mid's unit" + assertIO ((midSrc.splitOn "sorry").length == 2) "mid's proof is holed exactly once" + -- `task.json` exists only if the unit was emitted, which happens only after its own + -- `lake build` verification passed — so the pruned unit genuinely builds. + assertIO (← (midUnit / "task.json").pathExists) "mid's unit was emitted and verified" + finally + removeDirIfExists out + if ← mp.pathExists then IO.FS.removeFile mp + unsafe def run : IO Unit := do let result ← fixtureResult let records ← LeanReassemble.readRecords "TestFixtures/records.jsonl" @@ -712,6 +830,10 @@ unsafe def run : IO Unit := do testMaterializers testFailurePolicies testUnitFailurePolicies + let depsRecords ← LeanReassemble.readRecords "TestProject/records-deps.jsonl" + testDanglingReferences depsRecords + testDependencyConflicts + testUnitNeighbourPruning IO.println "reassemble tests passed" end ReassembleTests diff --git a/reassemble/TestProject/Fixture.lean b/reassemble/TestProject/Fixture.lean index a18298c..459bba2 100644 --- a/reassemble/TestProject/Fixture.lean +++ b/reassemble/TestProject/Fixture.lean @@ -1,2 +1,3 @@ import Fixture.Basic import Fixture.Examples +import Fixture.Deps diff --git a/reassemble/TestProject/Fixture/Deps.lean b/reassemble/TestProject/Fixture/Deps.lean new file mode 100644 index 0000000..1abc38f --- /dev/null +++ b/reassemble/TestProject/Fixture/Deps.lean @@ -0,0 +1,17 @@ +-- A module with a real theorem->theorem dependency edge (`mid` uses `base`), which +-- `Fixture/Basic.lean` lacks. The reassembler's dependency-conflict detection keys on +-- exactly such edges: deleting `base` while keeping `mid` would break the build, and +-- pruning `leaf` (which nothing depends on) must not. Self-contained (no +-- project-internal import) so the test harness can elaborate it directly. +namespace Fixture.Deps + +theorem base : True := by + trivial + +theorem mid : True := by + exact base + +theorem leaf : True := by + trivial + +end Fixture.Deps diff --git a/reassemble/TestProject/records-deps.jsonl b/reassemble/TestProject/records-deps.jsonl new file mode 100644 index 0000000..f982b71 --- /dev/null +++ b/reassemble/TestProject/records-deps.jsonl @@ -0,0 +1,3 @@ +{"attributes":[],"automation_tactics":[],"axioms":[],"body":"by\n trivial","calc_steps":null,"case_split_count":null,"closure_role":null,"decl_namespace":"Fixture.Deps","decl_source":"theorem base : True := by\n trivial","deps":["True","True.intro"],"doc":null,"end_col":9,"end_line":9,"file":"Fixture/Deps.lean","file_imports":["Init","Init"],"have_count":null,"is_private":false,"is_protected":false,"is_term_proof":false,"kind":"theorem","max_tactic_depth":null,"module":"Fixture.Deps","name":"Fixture.Deps.base","premises":[],"proof_method":null,"proof_script":null,"proof_term_depth":null,"proof_term_size":null,"rewrite_count":null,"scope_prelude":["namespace Fixture.Deps"],"signature":": True","start_col":0,"start_line":8,"tactic_histogram":{},"tactic_kinds":[],"tactic_metrics_source":null,"tactic_step_count":null,"tactic_total_count":null,"tags":{},"type":"True","value":"True.intro"} +{"attributes":[],"automation_tactics":[],"axioms":[],"body":"by\n trivial","calc_steps":null,"case_split_count":null,"closure_role":null,"decl_namespace":"Fixture.Deps","decl_source":"theorem leaf : True := by\n trivial","deps":["True","True.intro"],"doc":null,"end_col":9,"end_line":15,"file":"Fixture/Deps.lean","file_imports":["Init","Init"],"have_count":null,"is_private":false,"is_protected":false,"is_term_proof":false,"kind":"theorem","max_tactic_depth":null,"module":"Fixture.Deps","name":"Fixture.Deps.leaf","premises":[],"proof_method":null,"proof_script":null,"proof_term_depth":null,"proof_term_size":null,"rewrite_count":null,"scope_prelude":["namespace Fixture.Deps"],"signature":": True","start_col":0,"start_line":14,"tactic_histogram":{},"tactic_kinds":[],"tactic_metrics_source":null,"tactic_step_count":null,"tactic_total_count":null,"tags":{},"type":"True","value":"True.intro"} +{"attributes":[],"automation_tactics":[],"axioms":[],"body":"by\n exact base","calc_steps":null,"case_split_count":null,"closure_role":null,"decl_namespace":"Fixture.Deps","decl_source":"theorem mid : True := by\n exact base","deps":["Fixture.Deps.base","True"],"doc":null,"end_col":12,"end_line":12,"file":"Fixture/Deps.lean","file_imports":["Init","Init"],"have_count":null,"is_private":false,"is_protected":false,"is_term_proof":false,"kind":"theorem","max_tactic_depth":null,"module":"Fixture.Deps","name":"Fixture.Deps.mid","premises":["Fixture.Deps.base"],"proof_method":null,"proof_script":null,"proof_term_depth":null,"proof_term_size":null,"rewrite_count":null,"scope_prelude":["namespace Fixture.Deps"],"signature":": True","start_col":0,"start_line":11,"tactic_histogram":{},"tactic_kinds":[],"tactic_metrics_source":null,"tactic_step_count":null,"tactic_total_count":null,"tags":{},"type":"True","value":"Fixture.Deps.base"} diff --git a/reassemble/docs/parameter-matrix.md b/reassemble/docs/parameter-matrix.md new file mode 100644 index 0000000..77d1eec --- /dev/null +++ b/reassemble/docs/parameter-matrix.md @@ -0,0 +1,162 @@ +# Reassembler parameter matrix + +Status: spec. Defines the intended behavior of every meaningful combination of +`lean_reassemble` parameters, so each combination is either **sensible** or +**explicitly rejected** — never a silent wrong/misleading result. The +implementation (dependency-conflict detection, per-unit neighbour pruning, combo +guards) is verified against this matrix; see the "Validation" section. + +## Parameter surface + +Subcommands: `rewrite-file`, `materialize-repo`, `materialize-units`. + +| Parameter | Values | Meaning | +|---|---|---| +| `--proofs` | `sorry` (=replace) / `keep` / `delete` | global default action per theorem (`Rewrite.lean` `ProofMode`) | +| `--manifest` | per-theorem `keep`/`sorry`/`delete` | sparse override on `--proofs` (`Manifest.actionFor`) | +| `--on-failure` | `fail` / `skip` / `backoff` | what to do when a theorem cannot be reassembled | +| `--build-target` | a Lake target | scopes the build (see per-subcommand notes) | +| `--keep-eval` | flag | keep `#eval`/`#guard`/… instead of stripping (repo only) | +| `--in-process` | flag | rewrite all files in one process; performance only (repo only) | + +Each theorem's **resolved action** is `manifest[name]` if present, else `--proofs`. +The interesting axis is the *set* of resolved actions across the records. + +Dependency data on every record (`Corpus.ConstRecord`): `deps` — the direct +constants the declaration references; `premises` — the transitive project-owned +cone (polluted with undeletable auxiliaries like `._f`/`.match_1`/`._proof_*`); +`closureRole` — `"target"`/`"statement"`/`"proof"` within a `--decl` closure. + +### Flag applicability + +| Flag | rewrite-file | materialize-repo | materialize-units | +|---|---|---|---| +| `--proofs` | ✅ | ✅ | ✅ (target action) | +| `--manifest` | ✅ (optional) | ✅ | ✅ (target + neighbour pruning) | +| `--on-failure` | ✅ | ✅ | ✅ | +| `--build-target` | — | ✅ (final build) | ⚠️ pristine warm-up build only | +| `--keep-eval` | — | ✅ | 🚫 rejected (inert) | +| `--in-process` | — | ✅ | 🚫 rejected (inert) | + +## Verdict vocabulary + +- **sensible** — supported; the artifact is well-defined. +- **degenerate** — technically runs but yields no value; handled explicitly (excluded/warned) rather than shipped as a success. +- **rejected** — parser or pre-flight error, with a specific message. +- **requires-dependency-check** — runs only if the dependency pre-flight finds no dangling reference; otherwise fails fast naming each `dependent → deleted` pair. +- **inert** — flag has no effect for that subcommand; rejected at parse for units, documented for repo. + +## materialize-repo + +Copies the whole source tree, rewrites the files that carry records, then runs a +single `lake build` (scoped by `--build-target`). The build is the correctness +oracle for what remains; the dependency pre-flight makes *declared* deletes fail +with attribution before that build. + +| `--proofs` \ manifest | absent | mixes in `delete` | mixes in `keep`/`sorry` only | +|---|---|---|---| +| `sorry` | sensible — hole every recorded proof, strip eval, build | requires-dependency-check | sensible | +| `keep` | sensible — byte-identical reference state; nothing holed | requires-dependency-check | sensible | +| `delete` | requires-dependency-check — deletes all recorded theorems | requires-dependency-check | requires-dependency-check | + +Orthogonal flags: +- `--keep-eval`: meaningful with `sorry`/`delete` (something is holed); inert but + harmless with a pure `keep` run (nothing holed ⇒ eval never stripped). +- `--in-process` vs isolated: identical artifacts; performance/memory only. +- `--build-target`: scopes the final build. A holed/deleted theorem in a module + *outside* the target is not compiled, so a break there is not observed — see + "Rejections & guards". +- `--on-failure backoff`: degrades *planning*-failed theorems to `delete`. Those + discovered deletes are **not** covered by the pre-flight (which only sees + declared manifest/mode deletes); a resulting break still aborts at `lake build`. + +## materialize-units + +One standalone unit per theorem record. A unit is the target's whole module file +with the target's proof holed (`sorry`); statement neighbours stay proven and +resolve, together with cross-module dependencies, from the shared prebuilt cache. +A manifest may additionally **prune same-module neighbours** marked `delete`. + +| target's resolved action | verdict | +|---|---| +| `sorry` (replace) | sensible — the standard task (target holed) | +| `keep` | degenerate — a "prove-nothing" unit; excluded with a warning | +| `delete` | degenerate — no task for a deleted target; excluded (counted) | + +Neighbour actions **within** a unit (manifest, same module as the target): +- `delete` → the neighbour declaration is removed from that unit's file. +- `keep` / unlisted → kept proven (default is `keep`, not `--proofs`). +- `sorry` on a non-target neighbour → treated as `keep` (a unit only holes its own + target; holing an unrelated neighbour is out of scope). +- `delete` on a `where`/`let rec` auxiliary → no-op (no standalone syntax). + +Removing a neighbour can strand a *kept* neighbour or a def that references it; +that is caught per-unit by the dependency pre-flight (**requires-dependency-check**, +restricted to the target's module — cross-module refs come from the cache). + +Orthogonal flags: `--build-target` scopes only the *pristine warm-up* build that +populates the shared cache, **not** the per-unit builds; `--keep-eval` and +`--in-process` are inert and rejected at parse. + +## rewrite-file + +Rewrites one file and validates the edited document with the Lean LSP worker; it +does not build the project. + +- `sorry`/`keep`/`delete` on this file's records: **sensible**. A `delete` of a + name referenced *within the same file* is caught by the LSP validation. +- Cross-file dangling references are **not** checked (single-file scope, by + design). `--manifest` is accepted and validated against every record (a key + naming a theorem in another file is not a typo), but only this file's records + are rewritten. + +## Rejections & guards + +Each of these is an explicit error or excluded outcome, not a silent success: + +1. **repo/units dependency conflict** — a surviving declaration's `deps` names a + theorem the run deletes. Fail (under `--on-failure fail`) before building: + ``` + dependency conflict: N surviving declaration(s) reference deleted theorem(s); + deleting would break the build: + Trees.Tree.total_mirror -> Trees.sumList_reverse + ``` + In units under `--on-failure skip`/`backoff`, the affected unit is omitted and + named in the artifact's `manifest.json` instead of aborting the whole run. +2. **units empty artifact** — if no task is produced (every eligible theorem + resolved to `delete`/`keep`/auxiliary), fail rather than write a `manifest.json` + with `verification: passed` over zero tasks: + ``` + materialize-units produced no tasks: all N eligible theorem(s) resolved to + delete/keep/auxiliary — nothing to reconstruct + ``` +3. **units `--proofs delete`** (global default) — rejected early: it would delete + every target and produce no tasks. +4. **units `--proofs keep`** (global default) — every target is a prove-nothing + unit; all are excluded, so the empty-artifact guard (2) fails the run. +5. **units `--keep-eval` / `--in-process`** — rejected at parse as unknown + arguments; they have no effect in units mode. +6. **repo `--build-target` masking** — a build scoped to a target does not compile + modules outside it, so a dangling reference there is not observed by the build. + The dependency pre-flight (1) covers *declared* deletes regardless of target; + the artifact's `verification` object records the exact `lake build ` + command so a scoped verification is never mistaken for a whole-project one. + +## Validation + +Automated tests live in `reassemble/ReassembleTests.lean` against the in-repo +`TestProject` (and a new `TestProject/Fixture/Deps.lean` fixture that carries a +real theorem→theorem `deps` edge, which the original fixtures lack). They cover: +the pure `danglingReferences` relation, the three confirmed regressions +(units-delete → no tasks, units-keep → empty, repo delete-with-kept-dependent → +named conflict, not an opaque `lake` error), and the new units neighbour-pruning +and per-unit conflict behavior. + +Manual end-to-end on `examples/tree-project` (both pinned to the repo toolchain): +`materialize-repo --manifest '{"theorems":{"Trees.sumList_reverse":"delete"}}'` +reports the named conflict `Trees.Tree.total_mirror -> Trees.sumList_reverse`; +default `materialize-units` and a units run pruning a leaf theorem both build clean. + +Not in CI: the external corpus under `~/workplace/arg/src/LeanCorpusData/generated/*` +pins Lean v4.31.0 while leagent tracks a newer toolchain, so real-corpus checks +need version-matched binaries.