chore: lake: rm autoParam in Lake.Load.Resolve (#13495)

This PR fixes a segfault in the stage2 build of `Lake.Load.Resolve`
caused by the presence of an `autoParam`.

src/Lean/Elab/Do/Basic.lean

@@ -587,7 +587,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x newX
-    withDeadCode (if callerInfo.exitsDead then .deadSemantically else .alive) do
+    withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do

src/Lean/Elab/Do/Control.lean

@@ -232,8 +232,9 @@ def ControlLifter.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM Contr
     breakBase?,
     continueBase?,
     pureBase := controlStack,
-    -- The success continuation `origCont` is dead code iff the `ControlInfo` says so semantically.
-    pureDeadCode := if info.exitsDead then .deadSemantically else .alive,
+    -- The success continuation `origCont` is dead code iff the `ControlInfo` says that there is no
+    -- regular exit.
+    pureDeadCode := if info.numRegularExits > 0 then .alive else .deadSemantically,
     liftedDoBlockResultType := (← controlStack.stM dec.resultType),
   }
 

src/Lean/Elab/Do/InferControlInfo.lean

@@ -16,75 +16,48 @@ namespace Lean.Elab.Do
 
 open Lean Meta Parser.Term
 
-/--
-Represents information about what control effects a `do` block has.
-
-The fields split by flavor:
-
-* `breaks`, `continues`, `returnsEarly`, and `reassigns` are **syntactic**: `true`/non-empty iff
-  the corresponding construct appears anywhere in the source text of the block, independent of
-  whether it is semantically reachable. Downstream elaborators must assume every such syntactic
-  effect may occur, because the elaborator visits every doElem (only top-level
-  `return`/`break`/`continue` short-circuit via `elabAsSyntacticallyDeadCode`).
-* `numRegularExits` is also **syntactic**: the number of times the block wires the enclosing
-  continuation into its elaborated expression. `withDuplicableCont` reads it as a join-point
-  duplication trigger (`> 1`).
-* `exitsDead = true` asserts that the next doElem in the enclosing sequence is semantically
-  irrelevant (control never falls through to it). `exitsDead = false` makes no such
-  assertion. The dead-code warning fires on the next element when this is `true`.
-
-Invariant: `numRegularExits = 0 → exitsDead`. The converse does not hold.
--/
+/-- Represents information about what control effects a `do` block has. -/
 structure ControlInfo where
-  /-- The `do` block syntactically contains a `break`. -/
+  /-- The `do` block may `break`. -/
   breaks : Bool := false
-  /-- The `do` block syntactically contains a `continue`. -/
+  /-- The `do` block may `continue`. -/
   continues : Bool := false
-  /-- The `do` block syntactically contains an early `return`. -/
+  /-- The `do` block may `return` early. -/
   returnsEarly : Bool := false
   /--
-  The number of times the block wires the enclosing continuation into its elaborated expression.
-  Consumed by `withDuplicableCont` to decide whether to introduce a join point (`> 1`).
+  The number of regular exit paths the `do` block has.
+  Corresponds to the number of jumps to an ambient join point.
   -/
   numRegularExits : Nat := 1
-  /--
-  When `true`, asserts that the next doElem in the enclosing sequence is semantically irrelevant
-  (control never falls through to it). `false` asserts nothing.
-  -/
-  exitsDead : Bool := false
-  /-- The variables that are syntactically reassigned somewhere in the `do` block. -/
+  /-- The variables that are reassigned in the `do` block. -/
   reassigns : NameSet := {}
   deriving Inhabited
 
 def ControlInfo.pure : ControlInfo := {}
 
 def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := {
-    -- Syntactic fields aggregate unconditionally; the elaborator keeps visiting `b` unless `a` is
-    -- a syntactically-terminal element (only top-level `return`/`break`/`continue` are, via
-    -- `elabAsSyntacticallyDeadCode`).
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
+    -- Once `a` has no regular exits, `b` is statically unreachable, so no regular exit survives.
+    -- We still aggregate the other effects because the elaborator keeps visiting `b` unless it is
+    -- skipped via `elabAsSyntacticallyDeadCode`.
+    numRegularExits := if a.numRegularExits == 0 then 0 else b.numRegularExits,
     reassigns := a.reassigns ++ b.reassigns,
-    numRegularExits := b.numRegularExits,
-    -- Semantic: the sequence is dead if either part is dead.
-    exitsDead := a.exitsDead || b.exitsDead,
   }
 
 def ControlInfo.alternative (a b : ControlInfo) : ControlInfo := {
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    reassigns := a.reassigns ++ b.reassigns,
     numRegularExits := a.numRegularExits + b.numRegularExits,
-    -- Semantic: alternatives are dead only if all branches are dead.
-    exitsDead := a.exitsDead && b.exitsDead,
+    reassigns := a.reassigns ++ b.reassigns,
   }
 
 instance : ToMessageData ControlInfo where
   toMessageData info := m!"breaks: {info.breaks}, continues: {info.continues},
-    returnsEarly: {info.returnsEarly}, numRegularExits: {info.numRegularExits},
-    exitsDead: {info.exitsDead}, reassigns: {info.reassigns.toList}"
+    returnsEarly: {info.returnsEarly}, exitsRegularly: {info.numRegularExits},
+    reassigns: {info.reassigns.toList}"
 
 /-- A handler for inferring `ControlInfo` from a `doElem` syntax. Register with `@[doElem_control_info parserName]`. -/
 abbrev ControlInfoHandler := TSyntax `doElem → TermElabM ControlInfo
@@ -118,9 +91,9 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return ← ofElem ⟨stxNew⟩
 
   match stx with
-  | `(doElem| break) => return { breaks := true, numRegularExits := 0, exitsDead := true }
-  | `(doElem| continue) => return { continues := true, numRegularExits := 0, exitsDead := true }
-  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0, exitsDead := true }
+  | `(doElem| break) => return { breaks := true, numRegularExits := 0 }
+  | `(doElem| continue) => return { continues := true, numRegularExits := 0 }
+  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0 }
   | `(doExpr| $_:term) => return { numRegularExits := 1 }
   | `(doElem| do $doSeq) => ofSeq doSeq
   -- Let
@@ -161,12 +134,17 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
   -- For/Repeat
   | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq)
   | `(doRepeat| repeat $bodySeq) =>
+    -- `numRegularExits := 1` unconditionally, matching `for ... in`. For break-less `repeat` the
+    -- loop never terminates normally, so `0` looks more accurate semantically. But the loop
+    -- expression still has type `m Unit`, and the do block's continuation after the loop is what
+    -- carries that type. Reporting `0` makes the elaborator flag that continuation as dead code,
+    -- yet the user has no way to remove it without breaking the type of the enclosing do block
+    -- (unless its monadic result type happens to be `Unit`). So we pin at `1`; see #13437.
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
       numRegularExits := 1,
       continues := false,
-      breaks := false,
-      exitsDead := false,
+      breaks := false
     }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>

src/lake/Lake/Load/Resolve.lean

@@ -163,7 +163,7 @@ See `Workspace.updateAndMaterializeCore` for more details.
 @[inline] def Workspace.resolveDepsCore
   [Monad m] [MonadError m] [MonadLiftT LogIO m] (ws : Workspace)
   (resolve : Package → Dependency → Workspace → m MaterializedDep)
-  (root : Nat := 0) (h : root < ws.packages.size := by exact ws.size_packages_pos)
+  (root : Nat) (h : root < ws.packages.size)
   (leanOpts : Options := {}) (reconfigure := true)
 : m (MinWorkspace ws) := do
   go ws root h
@@ -473,7 +473,7 @@ def Workspace.updateAndMaterializeCore
     -- that the dependencies' dependencies are also properly set
     return ws.setDepPkgs ws.root ws.packages[start...<stop] ws.wsIdx_root_lt
   else
-    ws.resolveDepsCore updateAndAddDep (leanOpts := leanOpts) (reconfigure := true)
+    ws.resolveDepsCore updateAndAddDep ws.root.wsIdx ws.wsIdx_root_lt leanOpts (reconfigure := true)
 where
   @[inline] updateAndAddDep pkg dep ws := do
     let matDep ← updateAndMaterializeDep ws pkg dep
@@ -570,7 +570,7 @@ public def Workspace.materializeDeps
   if pkgEntries.isEmpty && !ws.root.depConfigs.isEmpty then
     error "missing manifest; use `lake update` to generate one"
   -- Materialize all dependencies
-  ws.resolveDepsCore (leanOpts := leanOpts) (reconfigure := reconfigure) fun pkg dep ws => do
+  let materialize pkg dep ws := do
     if let some entry := pkgEntries.find? dep.name then
       entry.materialize ws.lakeEnv ws.dir relPkgsDir
     else
@@ -584,3 +584,4 @@ public def Workspace.materializeDeps
           this suggests that the manifest is corrupt; \
           use `lake update` to generate a new, complete file \
           (warning: this will update ALL workspace dependencies)"
+  ws.resolveDepsCore materialize ws.root.wsIdx ws.wsIdx_root_lt leanOpts reconfigure

tests/elab/doControlInfoAggregate.lean

@@ -66,8 +66,11 @@ example : IO Nat := do
     return 42
   return 1
 
--- The `return 2` is required to give the do block its `Id Nat` result type; no dead-code warning
--- should fire on it.
+-- Break-less `repeat` under both branches of an `if`. If `repeat` reported
+-- `numRegularExits := 0`, the if's combined info would have `numRegularExits = 0` too, and the
+-- dead-code warning would fire on `return 2`. The user cannot remove `return 2` though: the loop
+-- expression is `Id PUnit`, so without a trailing element the do block's result type can't be
+-- `Id Nat`. We therefore pin `repeat`'s `numRegularExits` at `1` (same as `for ... in`).
 #guard_msgs in
 example (x : Nat) : Id Nat := do
   if x = 3 then

tests/pkg/homo/Homo.lean

@@ -0,0 +1,25 @@
+import Homo.Init
+
+set_option warn.sorry false
+
+opaque TSpec : (α : Type) × α := ⟨Unit, ()⟩
+abbrev T : Type := TSpec.1
+instance : Inhabited T := ⟨TSpec.2⟩
+opaque add : T → T → T
+opaque le : T → T → Prop
+opaque pos : T → Prop
+opaque small : T → Prop
+opaque f : Nat → T
+opaque toInt : T → Int
+
+@[grind_homo] theorem T.eq (a b : T) : a = b ↔ toInt a = toInt b := sorry
+@[grind_homo] theorem T.le (a b : T) : le a b ↔ toInt a ≤ toInt b := sorry
+@[grind_homo] theorem T.pos (a : T) : pos a ↔ toInt a > 0 := sorry
+@[grind_homo] theorem T.small (a : T) : small a ↔ toInt a < 8 := sorry
+@[grind_homo] theorem T.add (a b : T) : toInt (add a b) = (toInt a + toInt b) % 128 := sorry
+@[grind_homo] theorem cleanLeft (a b n : Int) : (a % n + b) % n = (a + b) % n := by simp
+@[grind_homo] theorem cleanRight (a b n : Int) : (a + b % n) % n = (a + b) % n := by simp
+
+set_option trace.homo true
+example (b : T) : pos b → small b → le b (add b b) := by
+  grind

tests/pkg/homo/Homo/Init.lean

@@ -0,0 +1,96 @@
+module
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Sym.Simp.Attr
+import Lean.Meta.Sym.Simp.Simproc
+import Lean.Meta.Sym.Simp.Rewrite
+import Lean.Meta.AppBuilder
+
+namespace Homomorphism
+
+open Lean Meta Grind Sym Simp
+
+initialize registerTraceClass `homo
+initialize registerTraceClass `homo.visit
+
+/--
+Declares attribute `[grind_mono]` for marking theorems implementing the homomorphism.
+-/
+initialize homoSimpExtension : SymSimpExtension ←
+  registerSymSimpAttr `grind_homo "`grind` homomorphism attribute"
+
+/--
+Returns theorems marked with `[grind_mono]`
+-/
+def getTheorems : CoreM Theorems :=
+  homoSimpExtension.getTheorems
+
+/--
+Creates a simproc that applies the theorems marked with `[grind_mono]`.
+This simproc is meant to be applied as a `pre` method.
+
+Recall that `grind` internalizes terms bottom-up. By the time a
+simplification set runs on a term `e`, all subterms of `e` are already
+in the E-graph and have been processed by the pipeline.
+
+**Stop condition.** When simp encounters a term `t` during traversal:
+
+- If a rule matches `t`: apply it, continue (result is a new term).
+- If no rule matches `t` AND `t` is already in the E-graph:
+  stop, don't descend. Otherwise: descend normally.
+-/
+def mkRewriter : GoalM Sym.Simp.Simproc := do
+  let s ← get
+  -- Remark: We are not using any discharger. So, our rewriting rules are all context
+  -- independent.
+  let rw := (← getTheorems).rewrite
+  return fun e => do
+    trace[homo.visit] "{e}"
+    let r ← rw e
+    if !r.isRfl then return r
+    -- If `e` is already in the E-graph, we don't revisit its children
+    let done := s.enodeMap.contains { expr := e }
+    return .rfl (done := done)
+
+structure State where
+  cache : Sym.Simp.Cache := {}
+
+initialize homoExt : SolverExtension Sym.Simp.Cache ←
+  registerSolverExtension (return {})
+
+/-- Apply the homomorphism theorems. -/
+def applyHomo (e : Expr) : GoalM Sym.Simp.Result := do
+  let methods := { pre := (← mkRewriter) }
+  -- Reuse cache.
+  let persistentCache ← homoExt.getState
+  homoExt.modifyState fun _ => {} -- Improve uniqueness. This is a minor optimization
+  let (r, s) ← Sym.Simp.SimpM.run (Sym.Simp.simp e) (methods := methods) (s := { persistentCache })
+  homoExt.modifyState fun _ => s.persistentCache
+  return r
+
+/--
+Returns `true` if some theorem marked with `[grind_homo]` is applicable to `e`.
+
+Motivation: we don't want to start the simplifier and fail immediately.
+-/
+def isTarget (e : Expr) : CoreM Bool := do
+  let thms ← getTheorems
+  return !(thms.getMatch e).isEmpty
+
+/--
+Internalization procedure for this module. See `homoExt.setMethods`
+-/
+def internalize (e : Expr) (_ : Option Expr) : GoalM Unit := do
+  unless (← isTarget e) do return ()
+  let .step e₁ h₁ _ ← applyHomo e | return ()
+  let r ← preprocess e₁
+  let h ← mkEqTrans h₁ (← r.getProof)
+  let gen ← getGeneration e
+  Grind.internalize r.expr gen
+  trace[homo] "{e}\n====>\n{r.expr}"
+  pushEq e r.expr h
+
+initialize
+  homoExt.setMethods
+    (internalize := internalize)
+
+end Homomorphism

tests/pkg/homo/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package homo
+@[default_target] lean_lib Homo

tests/pkg/homo/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/homo/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build