From 262410ddf60f6f710fa6e9bf92c408165de539c9 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Thu, 27 Mar 2025 18:32:17 +0000 Subject: [PATCH 1/3] feat: allow a general `evalTac` at `evalSepTactics` --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index af9ec3e363e2..eb6486782af0 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -33,8 +33,9 @@ open Language in /-- Evaluates a tactic script in form of a syntax node with alternating tactics and separators as children. - -/ -partial def evalSepTactics : Tactic := goEven +-/ +@[specialize] +partial def evalSepTactics (evalTac : Tactic := evalTactic) : Tactic := goEven where -- `stx[0]` is the next tactic step, if any goEven stx := do @@ -64,7 +65,7 @@ where -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do let some snap := (← readThe Term.Context).tacSnap? - | do evalTactic tac; goOdd stxs + | do evalTac tac; goOdd stxs let mut reusableResult? := none let mut oldNext? := none if let some old := snap.old? then @@ -87,15 +88,15 @@ where next := #[{ stx? := stxs, task := next.resultD default }] } -- Run `tac` in a fresh info tree state and store resulting state in snapshot for - -- incremental reporting, then add back saved trees. Here we rely on `evalTactic` + -- incremental reporting, then add back saved trees. Here we rely on `evalTac` -- producing at most one info tree as otherwise `getInfoTreeWithContext?` would panic. let trees ← getResetInfoTrees try let (_, state) ← withRestoreOrSaveFull reusableResult? - -- set up nested reuse; `evalTactic` will check for `isIncrementalElab` + -- set up nested reuse; `evalTac` will check for `isIncrementalElab` (tacSnap? := some { old? := oldInner?, new := inner }) do Term.withReuseContext tac do - evalTactic tac + evalTac tac finished.resolve { diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog)) @@ -120,7 +121,7 @@ where Term.withNarrowedTacticReuse (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) goEven stx @[builtin_tactic seq1] def evalSeq1 : Tactic := fun stx => - evalSepTactics stx[0] + (evalSepTactics) stx[0] @[builtin_tactic paren, builtin_incremental] def evalParen : Tactic := Term.withNarrowedArgTacticReuse 1 evalTactic From a7b929a61329bf41f4f7831459aea841ca3d963f Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Thu, 27 Mar 2025 18:34:39 +0000 Subject: [PATCH 2/3] add comment to doc-string --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index eb6486782af0..aeb79fad36be 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -33,6 +33,8 @@ open Language in /-- Evaluates a tactic script in form of a syntax node with alternating tactics and separators as children. + +The user can provide their own tactic evaluation function `evalTac`. -/ @[specialize] partial def evalSepTactics (evalTac : Tactic := evalTactic) : Tactic := goEven From 643e4f538dbffc2629dd40a60be8a6c71ebe2ff2 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 29 Mar 2025 12:57:34 +0000 Subject: [PATCH 3/3] make CI happy