choice nodes are mishandled in tactic and command elaboration

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The current implementation of choice node elaboration in tactics and commands is broken in two ways. Only the first argument is ever evaluated, even when elaboration of it throws an unsupported syntax error (which source code implicitly attempts to catch); and for tactic choice nodes, logged messages are obliterated when errors are (re-)thrown.

Context

Both of these bugs arise due to choices made near the same point in source code (more or less), hence the report of both of them at once.

The second occurred in Mathlib's override of the show tactic (zulip) (which performed a linting step then elaborated a term). (Note: the solution was to properly override the syntax by using (priority := high), avoiding choice nodes altogether, but the investigation still uncovered these bugs.) These bugs were found during the Meta Café.

1. In Tactic.evalChoice and Command.elabChoice, the implementation uses

    catchInternalId unsupportedSyntaxExceptionId
      (evalTactic tactic)
      (fun _ => evalChoiceAux tactics (i+1))

and respectively

    catchInternalId unsupportedSyntaxExceptionId
      (elabCommand cmds[i])
      (fun _ => elabChoiceAux cmds (i+1))

However, both evalTactic and elabCommand catch unsupported syntax errors internally, and re-throw them as ordinary errors. This means that the handler branch is never taken, and so we under no circumstances attempt to elaborate subsequent arguments of the choice node.

Possibly: evalTactic and elabCommandsUsing could log the user-friendly unsupported syntax error (instead of throwing), and re-throw the internal unsupported syntax error.

2. Tactic.evalChoice, in its use of catchInternalId, uses the ambient monad's try-catch, i.e. TacticM's backtracking try-catch. This erases any logged messages when re-throwing exceptions. Combined with the fact that exceptions with synthetic sorries are not logged themselves (and rely on previously-logged messages for visible error reporting), this can mean that a choice node silently fails when errors would otherwise be visible (without a choice node).

A non-backtracking monad instance could be inlined just before the call instead, but maybe there ought to be a dedicated Tactic.catchInternalId which calls the non-backtracking try-catch.

Steps to Reproduce

Control flow bug

1. Create a choice node for a command or tactic
2. throw an unsupported syntax error during elaboration of the first argument of the choice node

Expected behavior: the next arguments to the choice node are tried.

Actual behavior: a human-readable unsupported syntax error is visible.

import Lean

elab "foo" : tactic => pure ()
elab "foo" : tactic => Lean.Elab.throwUnsupportedSyntax

/--
error: Unexpected syntax
  foo
-/
#guard_msgs in
example : True := by foo; trivial

Backtracking bug

1. Create a choice node for a tactic
2. Log messages during elaboration of the first argument, then throw an ordinary, non-unsupportedSyntax exception

Expected behavior: the same as elaborating the first argument outside of a choice node: the exception propagates to the surface, and the logged messages are visible. (The exception itself is logged iff it would have been without a choice node.)

Actual behavior: the exception propagates to the surface, but the logged messages are not visible. (The exception itself is logged iff it would have been without a choice node; this is as expected.)

import Lean

elab "bar" _t:term : tactic => do pure ()
elab "bar" t:term : tactic => do
  let e ← Lean.Elab.Term.elabTerm t none
  Lean.logError "this error is dropped as well"
  throwError m!"`bar` failed: {e}"

-- "`bar` failed {e}" error thrown but not visible due to synthetic sorry in `e`
/-- warning: declaration uses `sorry` -/
#guard_msgs in
example : True := by bar nonexistent_constant

Versions

4.34.0, commit f2bcf2e8660ab2d16cf3cb50c8e127de0439a337 (on web)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by locating Tactic.evalChoice and Command.elabChoice, then read evalTactic, elabCommand, and elabCommandsUsing to trace unsupported-syntax handling and backtracking. Run the two self-contained reproductions from the issue. Done means later choice arguments are tried after unsupported syntax, and logged tactic messages remain visible when an ordinary error propagates.