feat: allow a general evalTac at evalSepTactics

[JovanGerb]

This PR generalizes evalSepTactics, so that users can use incremental elaboration in their own proof environment.

#lean4 > custom incremental elaboration

This was suggested by @mirefek

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7bd937580494311ecdb9502a7b5ab0ccf473bd44 --onto 1465c23e12f6f8b608ef944be4559b1b5e38f40a. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-27 19:02:53)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7bd937580494311ecdb9502a7b5ab0ccf473bd44 --onto 060b2fe46fe728934744ee52271b92ab74cbd5b4. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-29 13:19:18)

[JovanGerb]

changelog-language

[Kha]

Could you please expand this comment with an example of why one might want to do this? Otherwise future maintainers will be absolutely puzzled.

[mirefek]

I would write something like this:

Assume a tactic developer writes a new general modified tactic execution,
for example calling automation each step, displaying the goal in a specific
way, modifying the behavior of some tactics...

def customEvalTactic : Tactic :=

Then it is possible to create a tactic scope in which this tactic is called
on each line of the scope, while preserving the incremental elaboration by

@[tactic my_scope, incremental]
def myScopeElab : Tactic := fun stx => do
  withNarrowedArgTacticReuse 1 (
    withNarrowedArgTacticReuse 0 (
      withNarrowedArgTacticReuse 0 (
        (evalSepTactics customEvalTactic)
      )
    )
  ) stx

[Kha]

Please just pass the argument explicitly, in which case we may as well remove the default value

[kim-em]

This hasn't been touched in over a year, and has a merge conflict. I'm closing now; please re-open if you think appropriate.