chore: the previous commit exposed an issue with simp

`simp` was previously swallowing runtime exceptions and masking an
issue with this example.

`runT` is defined by well-founded recursion, but reducing the ground
term `runT x` takes a long time when `decide := true`.

Remark PR #2722 changes the `decide` default value to `false`.

When `decide := true`, we should probably have better diagnostics /
error messages for this kind of situation.

src/Lean/CoreM.lean

@@ -65,6 +65,12 @@ structure Context where
   initHeartbeats : Nat := 0
   maxHeartbeats  : Nat := getMaxHeartbeats options
   currMacroScope : MacroScope := firstFrontendMacroScope
+  /--
+  If `catchRuntimeEx = false`, then given `try x catch ex => h ex`,
+  an runtime exception occurring in `x` is not handled by `h`.
+  Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
+  -/
+  catchRuntimeEx : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -350,4 +356,42 @@ def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
+/-- Return `true` if the exception was generated by one our resource limits. -/
+def Exception.isRuntime (ex : Exception) : Bool :=
+  ex.isMaxHeartbeat || ex.isMaxRecDepth
+
+/--
+Custom `try-catch` for all monads based on `CoreM`. We don't want to catch "runtime exceptions"
+in these monads, but on `CommandElabM`. See issues #2775 and #2744
+-/
+@[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
+  try
+    x
+  catch ex =>
+    if ex.isRuntime && !(← read).catchRuntimeEx then
+      throw ex
+    else
+      h ex
+
+instance : MonadExceptOf Exception CoreM where
+  throw    := throw
+  tryCatch := Core.tryCatch
+
+@[inline] def Core.withCatchingRuntimeEx (flag : Bool) (x : CoreM α) : CoreM α :=
+  withReader (fun ctx => { ctx with catchRuntimeEx := flag }) x
+
+@[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α → CoreM α) {α} (x : m α) : m α :=
+  controlAt CoreM fun runInBase => f <| runInBase x
+
+/--
+Execute `x` with `catchRuntimeEx = flag`. That is, given `try x catch ex => h ex`,
+if `x` throws a runtime exception, the handler `h` will be invoked if `flag = true`
+Recall that
+-/
+@[inline] def withCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
+  mapCoreM (Core.withCatchingRuntimeEx true) x
+
+@[inline] def withoutCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
+  mapCoreM (Core.withCatchingRuntimeEx false) x
+
 end Lean

src/Lean/Meta/SynthInstance.lean

@@ -582,13 +582,16 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
      let action : SynthM (Option AbstractMVarsResult) := do
        newSubgoal (← getMCtx) key mvar Waiter.root
        synth
-     try
-       action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {}
-     catch ex =>
-       if ex.isMaxHeartbeat then
-         throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}"
-       else
-         throw ex
+     -- TODO: it would be nice to have a nice notation for the following idiom
+     withCatchingRuntimeEx
+       try
+         withoutCatchingRuntimeEx do
+           action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {}
+       catch ex =>
+         if ex.isRuntime then
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}"
+         else
+           throw ex
 
 end SynthInstance
 

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -606,13 +606,11 @@ where
         try
           if (← processCongrHypothesis x) then
             modified := true
-        catch ex =>
+        catch _ =>
           trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"
-          if ex.isMaxRecDepth then
-            -- Recall that `processCongrHypothesis` invokes `simp` recursively.
-            throw ex
-          else
-            return none
+          -- Remark: we don't need to check ex.isMaxRecDepth anymore since `try .. catch ..`
+          -- does not catch runtime exceptions by default.
+          return none
       unless modified do
         trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
         return none
@@ -810,21 +808,23 @@ where
 
 def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
   let ctx := { ctx with config := (← ctx.config.updateArith) }
-  withSimpConfig ctx do
+  withSimpConfig ctx do withCatchingRuntimeEx do
     try
-      let (r, s) ← simp e methods ctx |>.run { usedTheorems := usedSimps }
-      trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
-      return (r, s.usedTheorems)
+      withoutCatchingRuntimeEx do
+        let (r, s) ← simp e methods ctx |>.run { usedTheorems := usedSimps }
+        trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
+        return (r, s.usedTheorems)
     catch ex =>
-      if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
+      if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex
 
 def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
-  withSimpConfig ctx do
+  withSimpConfig ctx do withCatchingRuntimeEx do
     try
-      let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
-      pure (r, s.usedTheorems)
+      withoutCatchingRuntimeEx do
+        let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
+        pure (r, s.usedTheorems)
     catch ex =>
-      if ex.isMaxHeartbeat then throwNestedTacticEx `dsimp ex else throw ex
+      if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
 
 /--
   Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`

tests/lean/906.lean.expected.out

@@ -1,2 +1,3 @@
 906.lean:2:4-2:15: warning: declaration uses 'sorry'
-906.lean:14:2-14:28: error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
+906.lean:14:2-14:28: error: tactic 'simp' failed, nested error:
+maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

tests/lean/run/lazyUnfoldingPerfIssue.lean

@@ -18,7 +18,7 @@ theorem equivalent: Run.run x = Run.run x := by
   apply Eq.refl (runT x)
 
 example : Run.run x = Run.run x := by
-  simp [Run.run]
+  simp (config := { decide := false }) [Run.run]
 
 end Ex1