Lean4
/-- Run all tactics registered using `register_hint`.
Print a "Try these:" suggestion for each of the successful tactics.
If one tactic succeeds and closes the goal, we don't look at subsequent tactics.
-/
-- TODO We could run the tactics in parallel.
-- TODO With widget support, could we run the tactics in parallel
-- and do live updates of the widget as results come in?
def hint (stx : Syntax) : TacticM Unit :=
withMainContext
(do
let tacs := (← getHints).toArray.qsort (·.1 > ·.1) |>.toList.map (·.2)
let tacs := Nondet.ofList tacs
let results :=
tacs.filterMapM fun t : TSyntax `tactic => do
if let some msgs← observing? (withMessageLog (withoutInfoTrees (evalTactic t))) then
if msgs.hasErrors then
return none
else
return some (← getGoals, ← suggestion t msgs)
else
return none
let results ← (results.toMLList.takeUpToFirst fun r => r.1.1.isEmpty).asArray
let results := results.qsort (·.1.1.length < ·.1.1.length)
addSuggestions stx (results.map (·.1.2))
match results.find? (·.1.1.isEmpty) with
| some r =>
-- We don't restore the entire state, as that would delete the suggestion messages.
setMCtx r.2.term.meta.meta.mctx
| none =>
admitGoal (← getMainGoal))
