bug in convert

Stream: mathlib4

[Scott Morrison]

Here's a fascinating bug in convert:

import Mathlib
open BigOperators

example (h₁ : ∑ k in Finset.Icc 0 122, 0 = 0) : 0 ∣ 1 := by -- (kernel) declaration has metavariables '_example'
  apply Nat.dvd_of_mul_dvd_mul_left zero_lt_one
  convert dvd_mul_left 0 1

This is a minimised example in the sense that it works (i.e. errors with unsolved goals) for any smaller value of 122! Note that h₁ is just an innocent bystander in the context here.

Any ideas?

[Eric Wieser]

set_option maxRecDepth 516 in makes 122 too small

[Eric Wieser]

So I guess something is silencing an error when it shouldn't

[Kyle Miller]

I think it's because congr! (and so convert) tries doing assumption with semireducible transparency at the end. If you do convert (config := {closePost := false}) dvd_mul_left 0 1 you can see that there are some goals where doing assumption isn't crazy (but it probably shouldn't do this).

[Kyle Miller]

In the kmill_congr_post_reducible branch I was experimenting with having it doing the closePost routines at reducible transparency.

[Kyle Miller]

I think it needs a better heuristic, since often you want instance arguments to be equated by rfl at higher-than-reducible-transparency. Stuff like Preorder.toLT = instLTNat. To get this to work nicely, I think congr! would need to keep track of reducibility settings per argument. Right now it just maintains a list of metavariables.

[Scott Morrison]

I don't particularly mind how hard it tries with assumption, the key thing is not dropping the goal if something goes wrong.

[Scott Morrison]

#7945 fixes the error handling, at least, so it just spits out the subgoals it can't handle.

[Scott Morrison]

It's not perfect, as the internal error is not visible unless you set_option trace.congr! true.

[Scott Morrison]

My attempts to just rethrow the error result in it vanishing somewhere, and I couldn't work out where!

[Floris van Doorn]

I don't like tactics that will create a subgoal iff you set its allowed number of heartbeats too low. Or in other words: given a proof that works, raising the number of heartbeats should not break the proof (which will happen if a tactic suddenly solves one of the subgoals itself). This is also currently a problem with gcongr. Tactics like this should only use cheap dischargers (e.g. assumption with reducible transparency) and if the discharger times out, the tactic should fail.

[Eric Wieser]

My reading is that Scott agrees with you, but can't work out where the error is being silenced

[Eric Wieser]

I pushed a fix that removes the offending try/catch

[Floris van Doorn]

I expect that will cause failures in the library if we don't make the default discharger cheaper

[Eric Wieser]

It would be helpful if exceptions carried some kind of stack trace so that it was easier to debug this kind of thing

[Eric Wieser]

The issue here is indeed assumption with default transparency; have : 1 = 0 := by assumption fails with a recursion issue in the testcase

[Kyle Miller]

I should have mentioned that I tested that (to validate my suspicion about why setting closePost := false circumvents the error). Somehow assumption does show the error. I was going to look into this too to see why congr! seems to consume the error.

[Eric Wieser]

The answer is that congr! didn't consume the error, but convert did

[Kyle Miller]

Oh, I looked through the convert code and I didn't see that try ... catch ... at the end... That explains it!

[Kyle Miller]

That try/catch isn't justified, but just for the record, a way to make it safe (modulo the concerns that Floris brings up) is to do something like

return (← observing? <| m.congrN! depth config patterns).getM [m]

[Kyle Miller]

It'll still gobble up the error, and it'll be heartbeat-dependent, but at least it won't lead to forgotten goals.

[Kyle Miller]

Heather has mentioned the "three patron saints of metaprogramming" (whnfR, withMainContext, and instantiateMVars), but maybe this needs to be upgraded to the four horsemen, with the fourth being observing?, or more generally, correctly reverting MetaM state during error handling.

[Eric Wieser]

Do MetaM functions make any promises about what state they leave things in after an error?

[Damiano Testa]

Kyle Miller said:

Heather has mentioned the "three patron saints of metaprogramming" (whnfR, withMainContext, and instantiateMVars), but maybe this needs to be upgraded to the four horsemen, with the fourth being observing?, or more generally, correctly reverting MetaM state during error handling.

There are also consumeMData/cleanupAnnotations that trip up tactics.

[Eric Wieser]

Floris van Doorn said:

I expect that will cause failures in the library if we don't make the default discharger cheaper

It didn't; after all, anywhere that it previously would have failed would have given the kernel error that started this thread

[Heather Macbeth]

Floris van Doorn said:

given a proof that works, raising the number of heartbeats should not break the proof (which will happen if a tactic suddenly solves one of the subgoals itself). This is also currently a problem with gcongr.

@Floris van Doorn I was not aware of this being a possibility with gcongr, can you give an example?

[Floris van Doorn]

In this line on our branch of the Sobolev inequality I had to raise the heartbeat limit because otherwise gcongr succeeded but gave an extra subgoal.

[Eric Wieser]

I think generally we have a big design problem where we can't distinguish "this goal is within the scope of this tactic but there's a bug / timeout" and "this tactic failed because the goal was not appropriate"

[Thomas Murrills]

Floris van Doorn said:

I don't like tactics that will create a subgoal iff you set its allowed number of heartbeats too low. Or in other words: given a proof that works, raising the number of heartbeats should not break the proof (which will happen if a tactic suddenly solves one of the subgoals itself). This is also currently a problem with gcongr. Tactics like this should only use cheap dischargers (e.g. assumption with reducible transparency) and if the discharger times out, the tactic should fail.

If there are tactics that absolutely need the ability to allow more heartbeats in some circumstances, perhaps they could carry a config option that sets the heartbeats for that invocation of the tactic. (The tactic would be otherwise unaffected by the ambient maxHeartbeats, and always use its own default.)

[Eric Wieser]

#7972 is another fix for accidental error silencing, with mwe:

import Mathlib.Data.List.Defs
import Mathlib.Tactic.ApplyFun


def funFamily (_i : ℕ) : Bool → Bool := id

set_option maxRecDepth 2000 in -- changes the behavior of the tactic!
example (_h₁ : Function.Injective (funFamily ((List.range 128).map (fun _ => 0)).sum)) : true = true := by
  apply_fun funFamily 0

[Heather Macbeth]

Floris van Doorn said:

In this line on our branch of the Sobolev inequality I had to raise the heartbeat limit because otherwise gcongr succeeded but gave an extra subgoal.

I'm really surprised by that, I can't think how the implementation would lead to that. I'll investigate.

[Eric Wieser]

Any use of docs#MVarId.assumption (instead of assumptionCore) can lead to this behavior

[Eric Wieser]

But that's probably just the tip of the iceberg

[Heather Macbeth]

That would explain it. But then the fix should be there, right? We should ban the use in mathlib of any tactic which uses that.

[Eric Wieser]

I think this requires major re-plumbings of many complex tactics

[Eric Wieser]

Pretty much every use of observe? or try/catch is also suspect

[Eric Wieser]

Sorry, I got confused above; assumption is harmless, but catching errors from it is bad

[Eric Wieser]

Eric Wieser said:

I think this requires major re-plumbings of many complex tactics

A rough outline would be to replace things like side_goal_discharger : MVarId → MetaM Unit with side_goal_discharger : MVarId → MetaM Bool, where a return value of false means "I can't process this goal"

[Heather Macbeth]

Could someone do a census of where this behaviour occurs in mathlib meta code currently?

[Heather Macbeth]

Is it something that a linter could be written for?

[Eric Wieser]

Searching for catch \w+ => has 108 results, observing\? has 32

[Kyle Miller]

I think if the diagnosis is that try/catch inside tactics is suspect then we should seriously consider finding another solution here. This affects everything that has to do with doing an alternative when there is an exception (like with the <|> operator).

For example, should running out of heartbeats or hitting the max recursion depth be a mere exception, or should it be a higher-priority signal of some sort? One that's not catchable with try/catch and which throws even if it's the first argument to <|>?

[Eric Wieser]

If we had more structured exceptions, then we could have a linter analogous to the python one that rejects except: (aka except BaseException) and forces you to write except Exception: (which could translate to a pattern match in Lean). But all our errors are unstructured strings, so it's currently annoying to tell them apart (and so we don't)

[Thomas Murrills]

The typical Exception type (which is used by e.g. TacticM) does at least support "internal" exceptions as well:

inductive Exception where
  /-- Error messages that are displayed to users. `ref` is used to provide position information. -/
  | error (ref : Syntax) (msg : MessageData)
  /-- Internal exceptions that are not meant to be seen by users.
  Examples: "pospone elaboration", "stuck at universe constraint", etc -/
  | internal (id : InternalExceptionId) (extra : KVMap := {})

Maybe there's an argument for overriding or modifying the tryCatches to never catch errors with a certain InternalExceptionId?

[Thomas Murrills]

(We could then supply try ... catch! ... as a means of saying "actually, expose every error to being caught, including 'higher-level' ones like maxHeartbeats errors" if ever really needed)

[Thomas Murrills]

(Also currently the maxHeartbeats error seems to be(?) just an .error, so this strategy would also require modifying that)

[Thomas Murrills]

There might be implicit support for promoting the maxHeartbeats error to an internal exception, at least, given the following docstring for Exception.isMaxHeartbeat:

/--
  Return true if `ex` was generated by `throwMaxHeartbeat`.
  This function is a bit hackish. The heartbeat exception should probably be an internal exception.
  We used a similar hack at `Exception.isMaxRecDepth` -/

[Thomas Murrills]

Or maybe adding a constructor to Exception—or an extra field to error— would be a better, if more radical, solution. I'm not really sure about the "not meant to be seen by users" part, especially since we do see "stuck at universe constraint" errors...my main point is merely that we can already structure errors to some degree, and we could indeed change the behavior of tryCatch and orElse in the relevant monads fairly easily to see it and implement "high priority" signals.