doc-gen4 missing declaration

Stream: general

[Patrick Massot]

@Henrik Böving there is a very weird doc-gen bug. If you go to https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Ideal/QuotientOperations.html then you can't see this declaration which is the most important one in the file and is mentioned in the library overview so that building the community website currently fails.

[Henrik Böving]

I'll take a look when I'm home

[Eric Wieser]

I would guess there's a crash when parsing the declaration, so it gets skipped?

[Alex J. Best]

2023-10-17T08:12:17.3612730Z WARNING: Failed to obtain information for: Ideal.quotientInfRingEquivPiQuotient: unknown free variable 'ι' is the log message for that line btw

[Eric Wieser]

If that's the case, I think doc-gen should output a red box saying "error processing declaration Ideal.quotientInfRingEquivPiQuotient" rather than dropping it silently

[Alex J. Best]

and there are many such lines.

[Henrik Böving]

Yeah these ones appear for a bunch of declarations. I haven't been able to figure out where these errors are coming from. If you look at the code that does this error handling I tried to print more verbose messages there but that part never triggers so I dont really know why these are failing or how to narrow it down as it only seems to happen in large complicated files.

Also these errors are not that many compared to the number of declarations :D which is the reason I postponed looking into this after failing to get more information about the errorm

[Henrik Böving]

(deleted)

[Henrik Böving]

(deleted)

[Henrik Böving]

Okay I'm starting to add logging to the doc-gen meta framework and hopefully bisect the failing case out. I'll probably come back whining for meta help soon :P

[Alex J. Best]

The only thing I noticed is that this seems to hapen a lot with things with ⋂ and ⨅ and other big operators in, which made me wonder if it was somehow related to the delaborators for those. But I failed to minimise an example of such a thing

[Henrik Böving]

(deleted)

[Henrik Böving]

Okay after a bit of debug log based bisection it is:
https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/Base.lean#L182 this line that is failing
and in the specific case I have this information from this is happening here:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Order/CompleteLattice.lean#L1100
while printing the type of this theorem using the above function, the missing variable here is the iota:

WARNING: Failed to obtain information for: le_iInf_const: unknown free variable 'ι'

[Henrik Böving]

So it seems that indeed this is a bug in the delaborator of this type:

a ≤ ⨅ _ : ι, a :=

[Henrik Böving]

One more interesting observation: The same unkown free variable error (in this case with "decls") is happening to this declaration in QQ: https://github.com/gebner/quote4/blob/a387c0eb611857e2460cf97a8e861c944286e6b2/Qq/Match.lean#L89-L95 which is completely free of these bigop binders.

This leaves 3 possible conclusions:

1. They both call an underlying API that's buggy
2. They both copied the same mistake into their delaborator
3. The bugs are unrelated and this is a red herring for this particular issue.

[Henrik Böving]

Aha! It's a bug in the way that doc-gen is preprocessing these types

[Henrik Böving]

@Patrick Massot docs#Ideal.quotientInfRingEquivPiQuotient

[Patrick Massot]

Great! Thank you very much for fixing this so quickly.

[Eric Wieser]

Is the fact that docs#AddEquiv.uniqueProd.proof_1 appears (rather than being hidden) a fallout of this change, or is this a change to core?

[Henrik Böving]

Hm, these changes merely influenced how free variables were being handled while rendering expressions, they did not touch the filter for declarations...I have in fact not touched this filter in a long while

[Henrik Böving]

https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/DocInfo.lean#L120-L130 this is the blacklisting algorithm, iirc it is taken from the LSP? I did not call it directly at the time because it was a private function, idk if that is still the reason. It could definitely be improved and it would be super cool if we had some single source of truth for this "is this decl auto generated" idea.

Either way it's been like 10 months since I touched this. In addition to that this name does also not pop up in the logs of old runs so it was not a declaration that previously errored out but doesn't anymore

[Henrik Böving]

https://web.archive.org/web/20230326185341/https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Prod.html#AddEquiv.uniqueProd.proof_1 indeed according to the archive this has existed since at least march @Eric Wieser

[Rob Lewis]

@Henrik Böving the website build has turned up another missing declaration. AddCommGroup.equiv_directSum_zmod_of_fintype exists but docs#AddCommGroup.equiv_directSum_zmod_of_fintype doesn't

[Henrik Böving]

stdout:
WARNING: Failed to obtain information for: AddCommGroup.equiv_free_prod_directSum_zmod: parenthesize: uncaught backtrack exception
WARNING: Failed to obtain information for: AddCommGroup.equiv_directSum_zmod_of_fintype: parenthesize: uncaught backtrack exception

hmmm, that seems to be another pretty printing error, though I am unsure if it is my fault this time :D

[Henrik Böving]

Hmmm, these errors were not around 2 weeks ago: https://github.com/leanprover-community/mathlib4_docs/actions/runs/6593960010/job/17917228824

[Henrik Böving]

So either you introduced super funky new terms that my code isn't use to handling yet or for a change it is not actually my fault.

[Rob Lewis]

The website build failed last night for the first time, and the overview hasn't changed in a month, so this must be related to a change from yesterday

[Rob Lewis]

It could be #8050 ? I don't see any commits from yesterday that explicitly mention delaborators

[Rob Lewis]

Maybe #7964 landed just in time to miss the docs build that was used by Sunday's website build? Nothing's obviously suspicious there, it's just the only delaborator change I see

[Rob Lewis]

Okay, yeah. This doc-gen run at 2023-10-29T04:18:00-04:00 was fine but this one at 2023-10-30T04:19:00-04:00 wasn't. So the culprit is one of these mathlib4 commits, out of which #7964 looks like the only relevant change, unless I'm missing something in the std bump

[Rob Lewis]

This is indeed caused by #7964 (cc @Kyle Miller @Patrick Massot ). On current master this fails to pretty print:

import Mathlib.Data.Set.Pairwise.Basic

#check exists_ne_mem_inter_of_not_pairwise_disjoint

But reverting that commit makes it work again.

[Matthew Ballard]

Other occurrences

[Kyle Miller]

It seems that the new part of #7964 that is causing problems is globally enabling it. I guess there's been a latent bug in the binder merging logic... Commenting out this line causes my tests to succeed:

| `(∃ $group:bracketedExplicitBinders, ∃ $groups*, $body) => `(∃ $group $groups*, $body)

It appears to be merging in cases where it's not meant to and then throwing off the parenthesizer somehow.

[Henrik Böving]

Rob Lewis said:

This is indeed caused by #7964 (cc Kyle Miller Patrick Massot ). On current master this fails to pretty print:

import Mathlib.Data.Set.Pairwise.Basic

#check exists_ne_mem_inter_of_not_pairwise_disjoint

But reverting that commit makes it work again.

Not my fault for the first time! I count this as a win in my book :D

[Kyle Miller]

Here's a fix: #8070