docPrime hell

Stream: mathlib4

[Patrick Massot]

Moving the discussion here to avoid cluttering the other thread: is it known that docPrime will flood lake build output for downstream project if there is nothing to build? I mean nothing in Mathlib and nothing in the downstream project.

[Patrick Massot]

Note that this happens in a situation where I don’t have oleans for all files in Mathlib, only for the files that are imported in my project.

[Patrick Massot]

Maybe I could un-xy this to: could we simply turn this linter off until it behaves properly?

[Jireh Loreaux]

If you are building Mathlib from scratch, can you not just update the lakefile to disable the linter?

[Jireh Loreaux]

oh nevermind, you're getting a partial cache, not building from scratch.

[Patrick Massot]

You mean the Mathlib lakefile?

[Patrick Massot]

To be honest the partial cache thing seems randomly half-broken so I’m actually half building from scratch.

[Eric Wieser]

"nothing to build" happens here because you flooded the build logs when you built it the first time, and lake now regurgitates these on a noop build.

[Patrick Massot]

And why does it feel the need to do that? It takes forever too.

[Eric Wieser]

The initial flooding is a linter bug

[Patrick Massot]

I feel closer and closer to simply switching back to Lean 3 and hope things will get usable next year.

[Eric Wieser]

The regurgitation of all messages is a feature, because it means you don't miss the previous warnings

[Patrick Massot]

Is there any way to switch off this “feature”?

[Eric Wieser]

That's a question for @Mac Malone I think

[Patrick Massot]

It seems the VSCode extension is less paralyzed than lean.nvim by this behavior, so there is some hope for my students.

[Julian Berman]

Yes I'm aware that docPrime basically makes lean.nvim fall over.

[Julian Berman]

(The fix is we need to restore the backoff behavior we used to have -- because what happens now is basically the LSP spams us with responses as it goes through the compilation.)

[Damiano Testa]

This came up already several times. I think that one of the reasons the linter complains is that it looks for allowed exceptions in the path where the exceptions file exists in mathlib. However, if you have mathlib as a dependency, that path is incorrect. I thought that there were plans to make the searchpath for dependencies be aware of this.

[Damiano Testa]

If that is not the case, then I can try to see if I can tease out of lake what the correct path for the exceptions file it: the file will be in rootDir/.lake somewhere, rather than in rootDir/scripts. The main issue is to get the right pathseparators/special names for everything right.

[Patrick Massot]

Can I insist that we simply deactivate this linter until the issue is fixed?

[Patrick Massot]

I don’t see this linter as being so much mission-critical that it warrants inflicting this pain on any downstream project.

[Damiano Testa]

Personally, I am not too attached to the linter: I like the idea of documenting mathlib, but it is unclear whether this linter is achieving it in a reasonable way.

[Damiano Testa]

#20559, in case anyone feels strongly enough about this to merge the PR! :smile:

[Patrick Massot]

Thanks Damiano. I’ll wait a couple of minutes to see if someone complains before borsing this.

[Patrick Massot]

Note this won’t help me because I’m stuck with Lean 4.14.0 anyway…

[Eric Wieser]

I delegated modulo opening a tracking issue for actually fixing it

[Damiano Testa]

#20560 is the tracking issue.

[Damiano Testa]

I'll wait for CI to go green on the PR and merge it.

[Kim Morrison]

@Patrick Massot, we can backport #20559 to a version of Mathlib that still uses v4.14.0

[Kim Morrison]

e.g. as well as simply having the v4.14.0 tag of Mathlib, we make a releases/v4.14.0 branch of Mathlib (initially starting at that tag), and we can backport critical fixes to that branch.

[Eric Wieser]

And them make a v4.14.0-mathlib1 tag on that branch?

[Eric Wieser]

Or just tell people to put releases/v4.14.0 in the lakefile if they want "almost v4.14.0 but with future fixes"?

[Patrick Massot]

Having this fix and the cc bug fix on a 4.14 Lean would definitely help me.

[Patrick Massot]

Or maybe I should forget about using a released Lean, push to remove the on notation from Mathlib master and try to upgrade to 4.16.

[Patrick Massot]

I don’t know. I must confess I’m kind of panicking here. My course starts in one week and a half and my two colleagues teaching with me still haven’t tried Lean 4 at all, they are waiting for me to give them instructions about installing Lean 4. During lunch I told one them I had installation size issues and he jokingly answered by asking me how many Gigabytes they needed to allocate. I had to answer that it would indeed be measured in Gigabytes…

[Patrick Massot]

Of course for my colleagues the big install is not a real issue, but he simply couldn’t imagine the multiplicative factor from Lean 3 size to Lean 4 size would be 50.

[Eric Wieser]

Patrick Massot said:

Or maybe I should forget about using a released Lean, push to remove the on notation from Mathlib master and try to upgrade to 4.16.

Another option is for you to just create a branch of mathlib with whatever quick fixes you need, and run your course from that.

[Eric Wieser]

(by pointing to the branch instead of master in the lakefile)

[Kim Morrison]

@Patrick Massot, I've just pushed a tag v4.14.0-patch1, which contains

• #20559 (disabling docPrime linter)
• #20422 (cc panic issue)

This tag is on the releases/v4.14.0 branch, and we can backport further fixes to that if needed.

[Kim Morrison]

@Patrick Massot there's also now v4.15.0-patch1, which contains

• #20559 (disabling docPrime linter)
• #20562 (scoping on notation)

[Patrick Massot]

Thanks, this is really great. All this boring work with the on notation is really appreciated. I think removing the notation entirely is probably a better idea, but the current patch is enough for me.