diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index ce19929d3a..fd6acafb10 100644 --- a/src/Lean/CoreM.lean +++ b/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 := "", 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 diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 5a7b1bc297..a43a168c01 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 660a4a2eaf..c15d2850d7 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/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` diff --git a/tests/lean/906.lean.expected.out b/tests/lean/906.lean.expected.out index aa176b6ce6..dc783ba79b 100644 --- a/tests/lean/906.lean.expected.out +++ b/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 ` 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 ` to increase limit)