Propagating errors through Unhygienic.run

Stream: lean4

[Heather Macbeth]

I'd like to understand what is happening with error messages in the following code (which is a stripped-down version of the logic of the Mathlib linear_combination tactic).

import Lean.Elab.Tactic.Basic

open Lean Elab

elab "tac1" : tactic => do
  Tactic.evalTactic <| ← `(tactic| (rw [eq_comm]; rfl))

elab "tac2" : tactic => do
  let norm : Syntax.Tactic := Unhygienic.run `(tactic| rfl)
  Tactic.evalTactic <| ← `(tactic| (rw [eq_comm]; $norm))

example (a b : Int) : a - a + b = 0 := by
  rw [eq_comm]
  rfl -- error here

example (a b : Int) : a - a + b = 0 := by
  tac1 -- error here

example (a b : Int) : a - a + b = 0 := by
  tac2 -- "hidden" error

[Kyle Miller]

You need to have the "ref" set to some relevant syntax, to tag the components of the tactic with the source position from that ref.

Here's acquiring the "ref" from the tactic syntax being elaborated.

elab "tac2" : tactic => do
  let norm : Syntax.Tactic := Unhygienic.run <| withRef (← getRef) `(tactic| rfl)
  Tactic.evalTactic <| ← `(tactic| (rw [eq_comm]; $norm))

[Heather Macbeth]

In the case of tac2 here, the tactic is constructing the tactic sequence rw [eq_comm]; rfl, which doesn't solve the goal. But there is no red underline on tac2. Instead, there is a red underline on the by, but you can "keep working" on the proof for as long as you like, with no changes produced to the tactic state:

example (a b : Int) : a - a + b = 0 := by
  tac2 -- "hidden" error
  sorry
  sorry
  sorry
  sorry -- none of these sorries solve the goal

I'm assuming that somehow the Unhygienic.run partially absorbs the error, although the error remains in whatever term is presented to the kernel. Is that a correct interpretation? And is there a workaround which "preserves" the error location?

[Kyle Miller]

The source position information inside the norm syntax will then be used for later error reporting.

[Kyle Miller]

By the way, you can use this to localize the error:

elab tk:"tac2" x:ident : tactic => do
  let norm : Syntax.Tactic := Unhygienic.run <| withRef tk `(tactic| rfl)
  Tactic.evalTactic <| ← `(tactic| (rw [eq_comm]; $norm))

example (a b : Int) : a - a + b = 0 := by
  tac2 a -- error only on tac2

[Heather Macbeth]

Thanks! I'm preparing the bugfix now, but can you suggest what to add to the test file? The messages produced don't change, so guard_msgs doesn't work.

[Heather Macbeth]

#16072

[Eric Wieser]

I think probably for now just manually testing the error is where you want it is sufficient

[Eric Wieser]

But agreed it would be nice to have a position-reporting version of guard_msgs

[Heather Macbeth]

Eric Wieser said:

I think probably for now just manually testing the error is where you want it is sufficient

@Eric Wieser Is there a way of doing that?

[Eric Wieser]

Manually testing? I mean open the file that tests for an error _somewhere_, and look at the red squiggle by eye!

[Heather Macbeth]

Ah ... I don't mean to ask how to check that the bugfix was working (I can see that it does!). Rather, I was asking about what kind of test to add to the Mathlib test file for linear_combination (as is traditional after fixing a bug).

[Eric Wieser]

Yes, and my comment was "I would be happy to merge it without such a test, since I think such a test is unreasonably hard to write!"

[Eric Wieser]

I think the way lean core handles this is to capture the stdout of lean, and compare it to a sample file

[Eric Wieser]

I don't think mathlib has the infrastructure for such tests, but I am happy to be proven wrong

[Eric Wieser]

Perhap I'm missing something obvious here, but why do you need Unhygienic.run in the first place? Things seem to work fine in your mwe without it:

import Mathlib

open Lean Elab Tactic

elab "tac2" x:term : tactic => do
  let norm : Syntax.Tactic ←  `(tactic| rfl)
  Tactic.evalTactic <| ← `(tactic| (rw [eq_comm]; $norm))

elab tk:"tac2'" x:term : tactic => do
  let norm : Syntax.Tactic ← withRef tk `(tactic| rfl)
  Tactic.evalTactic <| ← `(tactic| (rw [eq_comm]; $norm))

example (a b : Int) : a - a + b = 0 := by
  tac2 1 -- error on this line

example (a b : Int) : a - a + b = 0 := by
  tac2' 1  -- error on `tac2'`

[Heather Macbeth]

It seems to work without it in the un-MWE'd code, too. This line dates from @Mario Carneiro's original code in #605 -- Mario, do you remember what the Unhygienic.run is doing there?

[Mario Carneiro]

If a syntax quotation doesn't need hygiene, I think it is more hygienic to use Unhygienic.run so that you can get the value as a pure value and not a monadic one. In particular, that makes it eligible for closed term extraction, unlike monadic syntax quotations.

[Kyle Miller]

I could see extending #guard_msgs to include relative source position information, with some option set. That would help here, right @Heather Macbeth ?

(By the way, in core Lean's testing framework, there are interactive tests that use comments to pick out information that appears at particular source positions. Example source, example out)

[Heather Macbeth]

Yes, seems like it!

[Eric Wieser]

@Kyle Miller, since you agree with Mario's advice, could you PR a small docstring for docs#Lean.Unhygienic.run to explain that use-case?

[Eric Wieser]

(documentation PRs from non-FRO members tend to get stuck on things like this, c.f. borrow notation)

[Sebastian Ullrich]

Eric Wieser said:

(documentation PRs from non-FRO members tend to get stuck on things like this, c.f. borrow notation)

I see multiple unresolved questions in that PR and have thus marked it as awaiting-author now. Do you disagree with that?

[Eric Wieser]

Do you disagree with that?

Yes, I think I'm waiting a ruling from the FRO on whether I should take David or Mac's suggestion. My point above was that if either of them owned the PR, then presumably such a ruling would be easier to arrive at internally.

[Sebastian Ullrich]

But that was only one out of three open threads, with no response from you. The PR looked quite abandoned. Your new comments look much more helpful for leading this PR to a conclusion. I removed the label.