haveLet linter crashing under `byAsSorry`

Stream: mathlib4

[Kim Morrison]

Now that we've got the new variable command in, I'm trying to get Mathlib running under byAsSorry. Initial signs are good!

However, the haveLet linter is crashing with a stack overflow. I can work around this for now by putting
⟨`weak.linter.haveLet, .ofNat 0⟩,
in the lakefile. @Damiano Testa, would you be able to take a look at this?

If you checkout branch#byAsSorry, remove that line from the lakefile, and build, you should encounter the stack overflow not too far in!

[Damiano Testa]

Ok, I will take a look!

[Damiano Testa]

I have not gotten to the overflow yet, but I remembered that I had observed an issue during development: https://github.com/leanprover-community/mathlib4/pull/12190#issuecomment-2061005403. I'll try to build these files directly to see if observe the overflow!

[Damiano Testa]

I believe that I found a stack overflow in Mathlib.Data.UInt, which I also think was one of the ones that I noticed earlier.

[Damiano Testa]

Kim, this seems exactly an issue that I had already tried to fix and failed while developing the linter. However, when the byAsSorry option is on, maybe the linter should not run anyway.

[Damiano Testa]

Would it make sense to silence the linter while in byAsSorry mode?

[Damiano Testa]

After all, if you are byAsSorrying everything, you probably do not care about haves that should be lets!

[Kim Morrison]

Yes, I've turned it off on the byAsSorry branch (and in fact I will turn off all linters), just thought you might be interested in the crash. :-)

[Damiano Testa]

I am interested and I had already observed it in 3 commands throughout Mathlib.

Eric thought that it was a consequence of his "hack" and they were fixed by explicitly initializing a MetaM context. However, the "hack" handles the context better, in all cases where it does not crash!

[Sébastien Gouëzel]

I've just hit the overflow in the PFR project, without byAsSorry. You can see it in https://github.com/sgouezel/pfr, commit f428dbcacae0f13d0ac49cb8ec481c7b1bbd586f, in the file PFR.Matlhlib.Probability.Independence.Kernel. It starts with

libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)
interpreter stacktrace:
#1 Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1
#2 Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1

and goes on like that for a long time. I don't see any suspicious line in the proof.

[Damiano Testa]

I think that Kim disabled the HaveLet linter with byAsSorry.

[Damiano Testa]

Since the linter is chatty when there is a sorry, it would flag everything, so I think that the linter should have a mechanism for only enabling itself when byAsSorry is set, but I have not looked into that yet.

[Sébastien Gouëzel]

Note that there is no sorry in this proof, it is a perfectly fine proof that works fine with lake build.

[Damiano Testa]

I have not actually looked at anything with byAsSorry, but could it be that some version of the lemmas with by replaced by sorry are actually elaborated?

[Damiano Testa]

This may mean that the linter is also checking those "invisible, sorried lemmas" and causing trouble,

[Damiano Testa]

If you can point me to a more specific place in the repo, I can try to take a look.

[Mario Carneiro]

why does nonPropHaves have partial? It doesn't seem to be recursive

[Sébastien Gouëzel]

I haven't been clear: there is absolutely no sorry around, it's a complete proof.

[Damiano Testa]

Mario Carneiro said:

why does nonPropHaves have partial? It doesn't seem to be recursive

It might be an indication that it was modified from a version that was really partial to the current version that no longer is.

[Sébastien Gouëzel]

I have fixed the problem in my case, by renaming two unused variables hi and hj to _hi and _hj (this was signalled to me by the unusedVariables linter when compiling on the command line). Once this is done, the stack overflow disappears. Looks like black magic...

[Damiano Testa]

Ah, the warnings for the unused variables made the linter active!

[Sébastien Gouëzel]

If it gives you a clue for how to fix it, that's great!

[Damiano Testa]

The linter is active when the command emits a warning. Typically, this is the presence of a sorry, but, in fact, any warning makes the linter chatty.

[Mario Carneiro]

I'm looking at the implementation of the linter now, and it seems to be doing unnecessary things

[Damiano Testa]

Maybe I should change the HaveLet linter to only be chatty when there is a sorry, not when any warning is present.

[Damiano Testa]

Mario Carneiro said:

I'm looking at the implementation of the linter now, and it seems to be doing unnecessary things

I'm happy to learn about ways of simplifying it! :smile:

[Mario Carneiro]

the implementation strategy I would suggest is:

• Find all have syntaxes in the command
• Get the e in have ... := e
• Look for info tree data on e, see if the type of e is a proposition and lint otherwise

[Sébastien Gouëzel]

What I don't get is why it wanted to talk to me, because there is no have that should be a let in this proof, as far as I can tell!

[Damiano Testa]

I think that it was trying to figure out whether it should be telling you something and got hung up somewhere.

[Mario Carneiro]

also the linter seems to miss that there are two have syntaxes, it only looks for the tactic but there is also an expr

[Damiano Testa]

Mario Carneiro said:

the implementation strategy I would suggest is:

• Find all have syntaxes in the command
• Get the e in have ... := e
• Look for info tree data on e, see if the type of e is a proposition and lint otherwise

This makes me think that you can find the haves first (easy) and then look at the infotrees arising from the have without going through the whole infotree: how do I do that?

[Mario Carneiro]

You have to go through the info tree, but you can limit it to one pass if you find all the syntaxes you want to spot first and look for all of them

[Damiano Testa]

Mario Carneiro said:

also the linter seems to miss that there are two have syntaxes, it only looks for the tactic but there is also an expr

That was deliberate, since I was not comfortable with infotrees and wanted to decrease what I had to keep track of.

[Mario Carneiro]

and of course you can early exit if the proof never uses have syntax

[Damiano Testa]

Oh, you mean that I extract the have syntax, then run through the whole infotree and, whenever the node is one of the syntax bits that I extracted, then dive into it?

[Mario Carneiro]

unfortunately you can't navigate the info tree really, because the tree structure doesn't have any useful invariants

[Mario Carneiro]

so you just have to look at everything

[Mario Carneiro]

but you can set up a hashmap of syntax you care about and skip nodes that aren't talking about one of them

[Damiano Testa]

Looking at the code, why is

    let .ofTacticInfo i := info | return #[]
    let stx := i.stx
    let .original .. := stx.getHeadInfo | return #[]
    unless isHave? stx do return #[]

not already just looking at the have nodes?

[Mario Carneiro]

it is (well, it is looking at have tactic nodes), but the rest of the code is doing things not in my list

[Mario Carneiro]

With my suggestion, you only have to look at expr info nodes, not tactic info nodes

[Mario Carneiro]

because you are looking at the e in have ... := e, not the tactic itself

[Damiano Testa]

Ok, I think that I understand now: I should catch the stuff after the := and just inspect those nodes further -- I had missed this from your initial message, don't know why.

[Mario Carneiro]

right, the algorithm is really "lint if any expression occurring on the RHS of a have term/tactic has a non-prop type"

[Damiano Testa]

Ok, I think that I had given up on that at the time, since there were many syntactic possibilities for the "stuff after :=", but I know more about syntax now and I can probably do this better then.

[Damiano Testa]

In particular, wasn't there some form of have that did not have :=?

[Mario Carneiro]

I suppose that's true, but you can just look at any of the match arms in that case

[Mario Carneiro]

although it's more complicated if you actually want to make a Try this suggestion / autofix

[Damiano Testa]

Try this suggestions are unavailable to linters, though, right?

[Damiano Testa]

Oh, linters could run refactor-like code, though, right?

[Mario Carneiro]

code actions can detect linter warnings and suggest changes

[Damiano Testa]

Ah, ok. I have no experience with code-actions.

[Damiano Testa]

Anyway, I'll try to write a faster implementation of the linter by looking at e in have ... := e and then I will worry about edge cases for have. The code action will wait a bit longer still.

[Damiano Testa]

For me, what ends up being efficient code is not always lined up with what I expect to be efficient, so these suggestions are great, because they give me a better sense of what is cheap and what isn't.

[Michael Rothgang]

Damiano Testa said:

Ah, the warnings for the unused variables made the linter active!

FWIW, #15942 had the same issue - thanks for implicitly telling me how that came about!

[Yaël Dillies]

Oh, maybe that's also why I had to comment out huge chunks of my proof of Kneser's theorem! It timed out for no clear reason

[Mario Carneiro]

I think in this case the issue is actually the way InfoTree.foldInfoM is defined causes large stacks of closures to be constructed, meaning that any sufficiently large proof will produce a deep stack recursion (number of recursive calls equal to the number of nodes in the info tree for a command)

[Damiano Testa]

I will also add a todo to the linter, saying that it should only be active with sorry. Or maybe, inspecting the term e directly, I can simply put a check there if there is a sorry and flag those.

[Yaël Dillies]

Yaël Dillies said:

I had to comment out huge chunks of my proof of Kneser's theorem

It is roughly 400 lines long, for reference, in a single theorem

[Damiano Testa]

Yaël Dillies said:

Yaël Dillies said:

I had to comment out huge chunks of my proof of Kneser's theorem

It is roughly 400 lines long, for reference, in a single theorem

Together with the longLine and longFile linters, it looks like we also need a longProof linter.

[Violeta Hernández]

What is this byAsSorry thing?

[Violeta Hernández]

I noticed this change in the SetTheory/Ordinal/Topology file. Is this really necessary? Using calc in place of a one line proof seems like overkill.
image.png

[Scott Carnahan]

start of byAsSorry:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Running.20Mathlib.20under.20.60set_option.20debug.2EbyAsSorry.60/near/453913575

[Violeta Hernández]

Violeta Hernández said:

Using calc in place of a one line proof seems like overkill.

So, was this change accidental, or deliberate? Does it have anything to do with getting the linter to work?

[Violeta Hernández]

Oh wait I get it, the issue is that by block at the end

[Kim Morrison]

The issue is that the middle term in the calc is not knowable before entering the by block.

[Kim Morrison]

I had thought we would just be doing this everywhere in Mathlib, but it turns out not so much! I'm skeptical of forbidding it, but there are some nice payoffs to avoiding relying on it. (In particular, the potential for fast benchmarking builds of Mathlib, so we can do a better job of optimizing Lean for Mathlib performance.)

[Mario Carneiro]

Kim Morrison said:

The issue is that the middle term in the calc is not knowable before entering the by block.

shouldn't it be the RHS of that TFAE expression?

[Kim Morrison]

One would hope. I dimly remember that there was an unspecified universe or something here, that the by block resolved? We'd have to look at the byAsSorry branch, and restore the old proof and see what goes wrong.