!4#3758 – rfl refactor & fix

Stream: mathlib4

[Thomas Murrills]

I want to check something before I go forward. The following is the for loop with surrounding commands in rfl (goal : MVarId) : MetaM Unit in the present state of the PR:

...
  let s ← saveState
  for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
    try
      let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
      if gs.isEmpty then return () else
        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n
          {goalsToMessageData gs}"
    catch e =>
      s.restore
      throw e
  throwError "rfl failed, no lemma with @[refl] applies"

The following is the original, in TacticM:

...
  let s ← saveState
  for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
    try
      liftMetaTactic (·.apply (← mkConstWithFreshMVarLevels lem))
      return
    catch e =>
      s.restore
      throw e
  throwError "rfl failed, no lemma with @[refl] applies"

Questions I have:

1. Why do we throw e from the catch block? Does this exit the for loop early? It seems not to. If not, why throw it at all, since we don't catch and use it?

2. Should we restore the state if apply fails to close the goal? That is, should we exit to the catch with

...
     let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
      if gs.isEmpty then return () else
        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n
          {goalsToMessageData gs}"
        failure

Though, does try not automatically restore the state? (I was under the impression it did...)

[Mario Carneiro]

1. Yes, it exits early. Why throw? Because we want to report the apply failure as the error message, not "no @[refl] lemma applies"

[Mario Carneiro]

2. No we should not restore the state, the state at an error should reflect whatever was happening at the time as an aid to debugging. No, try does not automatically restore the state. <|> does.

[Thomas Murrills]

Ah, ok. But, re (1)...why would we want to exit the for loop early if a single lemma in the loop failed to be applied? Wouldn't we want to try the rest and continue the loop?

[Thomas Murrills]

I guess we're betting on the getMatch meaning that apply always succeeds (in MetaM), and if it doesn't, tell us.

[Mario Carneiro]

that's a fair point. Both throw and return mean we will exit early, so the loop is not a loop

[Mario Carneiro]

better would be to stash the first error and report it if we fall out of the loop

[Thomas Murrills]

Makes sense—just the first one, or all of them in e.g. an Array?

[Mario Carneiro]

just the first

[Thomas Murrills]

Ok, cool!

[Mario Carneiro]

you can't report multiple errors like that

[Mario Carneiro]

if this mattered more, we might want to consider putting in those structured trace messages so that you can get a tree of emoji explosions and see all the errors

[Thomas Murrills]

ah, gotcha! So wait, is reporting this kind of error something we'd want to log or throw? I can see logError doesn't fail/except out, but I'm not sure when we want to use each

[Thomas Murrills]

Or, is logging even compatible with Exceptions?

[Mario Carneiro]

throw means early exit. Use it if you can't complete the task given by the type signature

[Mario Carneiro]

logging and Exceptions are mostly orthogonal. logError means put a red squiggle, throw means early exit until you get caught by something, like a tactic control flow operator like repeat / try, or the default handler that turns the exception into a logError otherwise

[Mario Carneiro]

actually thinking about control flow manipulation is probably the easiest way to understand things here. If you use logError and continue on failure, then if the user uses try rfl when it doesn't apply they will get a red squiggle on rfl anyway

[Thomas Murrills]

Ah, ok—thanks for clearing that up, I didn't know how red squiggles were born!

[Thomas Murrills]

So I guess the stashing-exception approach has us manipulate control flow when the loop ends, but varies why (i.e. "because the loop ended" or "because the loop ended and some apply failed in the middle of it")

[Thomas Murrills]

re (2): good to have the try behavior cleared up! :) Having the state reflect what was happening at the error suggests that if we stash the first exception and fall out of the loop, we actually want to save the state when the exception is encountered, then restore it before throwing that exception (if we do)

[Thomas Murrills]

Is there any reason to restore the MetaM state before each round of the for loop just under normal (successful) circumstances? Tbh I'm a little unclear on what state MetaM carries—mvar assignments, for one, I'm guessing? Seems like this gets by without worrying about that, though...and I'm a little unclear on how.

[Mario Carneiro]

In both cases, rfl has "failed". (More precisely, rfl fails whenever no @[refl] lemma applies.) The only difference is the error message we produce

[Mario Carneiro]

the mvar assignments are the important thing. If the apply fails we want to roll back any partial unification that happened when applying the next lemma

[Thomas Murrills]

That 's what I would expect! But, why does it seem to work if we don't do that?

[Mario Carneiro]

because the loop wasn't a loop?

[Mario Carneiro]

I don't think the multiple refl lemma case has been tested at all

[Mario Carneiro]

the discrimination tree is good enough to avoid needing it most of the time

[Thomas Murrills]

ahh ok! makes sense.

[Thomas Murrills]

Ok, I think that's sufficient for me to fix it up! :) ty!

[Thomas Murrills]

One last thing: is the raw throw e in the case of an apply exception what we want? Seems like it might be mysterious. Or do we want something more descriptive, involving throwError "... {e.toMessageData}"? (Currently it just throws.)

[Mario Carneiro]

the error message from apply is pretty okay, something like couldn't match 2 + 2 = 5 with ?a <= ?a, I don't see much reason to put a header on that

[Thomas Murrills]

Ok, so the benchmark says:

There were significant changes against commit 42f68ca:

  Benchmark                      Metric         Change
  ====================================================
- ~Mathlib.Tactic.Relation.Rfl   instructions    13.9%

in red—does this mean that that file took 13.9% longer (which is fine, since it’s very quick in absolute time), or that instructions(?) “from” that file took longer?

[Sebastian Ullrich]

There were 13.9% more CPU instructions, which essentially means it got 13.9% slower

[Thomas Murrills]

But, just while processing that file, or overall, because of that file?

[Thomas Murrills]

(Well, not quite “overall”, but what I mean is—are these instructions that will be reused when declarations in Mathlib.Tactic.Relation.Rfl are used in other files?)

[Sebastian Ullrich]

While processing that specific file

[Thomas Murrills]

Ok, ty! :)