docs4 not updated

Stream: mathlib4

[Jireh Loreaux]

It seems like docs4 hasn't updated in 2 weeks (cf. https://github.com/leanprover-community/mathlib4_docs/actions). Is there a reason? It would be nice for it to be up-to-date.

[Heather Macbeth]

I'll guess that it's this:

Mario Carneiro said:

Shouldn't the build be using compatible versions of std4 and mathlib4?

building std4:master against mathlib4:master is likely to be frequently broken

docs4 only builds on Thursdays in months containing "r" ... er, I mean, on days when mathlib is compatible with the latest version of Std.

[Jireh Loreaux]

So we need to bump to the latest std4 in mathlib?

[Heather Macbeth]

Yes ... I don't know if it needs the latest Lean nightly, too.

[Heather Macbeth]

Oh, Gabriel is working on it anyway: !4#2709

[Gabriel Ebner]

And it's green.

[Jireh Loreaux]

Thanks!

[Henrik Böving]

Heather Macbeth said:

Yes ... I don't know if it needs the latest Lean nightly, too.

Generally speaking I try to keep the nightly in sync with mathlib4...the mathlib4 vs std4 master thingy is an unfortunate side effect caused by the lake update I run on mathlib to pull in the latest doc gen

[Heather Macbeth]

I'd love for us not to have this problem. I really miss the mathlib3 docs which updated every couple of hours, even if every maintainer was on holiday for a month.

Why do we need the latest doc-gen4? Can we set it up so that the docs are generated from whatever version of doc-gen is currently in the mathlib manifest? And then just do PRs to mathlib when we want to update the doc-gen version?

[Eric Wieser]

In mathlib3 we always build against the latest doc-gen

[Eric Wieser]

But also, we generate a project file with the exact versions of everything in CI, rather than using whatever is committed

[Heather Macbeth]

If we don't require the latest version of doc-gen, the worst that can happen is that the docs build with an old version of doc-gen. If we do require the latest version of doc-gen, the worst that can happen (and it indeed happens frequently) is that the docs don't build at all!

[Henrik Böving]

Right let me lay out the issue fully:

1. Why do you have to use the latest doc-gen4? You don't actually have to do that, however you want to. This is because doc-gen4 uses Lean compiler internals to figure things out. If a compiler API changed behavior in the lean nightly that mathlib is using compared to the version that your pinned version of doc-gen4 that you are using it can (and has in the past) blown up. I would expect this to change once the compiler finally stabilizes :tm: So no the worst is not that your docs build with maybe not the latest feature set, the worst is actually that it might just not work at all as well :(

2. Why is what is happening right now actually an issue? The issue is not that I pull doc-gen4 to the latest version, in fact I try to always keep doc-gen4 latest compatible to mathlib4 latest. The issue is mostly the way I do it. Basically the CI will substitute the https source for doc-gen4 with a hard file path to the current doc-gen4 checkout and run lake update to make sure it is using the latest version (and also the latest versioon of the dependencies). However as a side effect all dependencies of mathlib4 get updated as well. This is not something that has to happen. Technically speaking lake could support only updating one dependency and all its transitive deps instead of all project dependencies, it just doesn't (yet).

[Sebastian Ullrich]

Why do you need to substitute the doc-gen4 source and run lake update?

[Henrik Böving]

Because lake just uses the pinned commit in lake-manifest.json otherwise

[Henrik Böving]

I could of course start hacking on lake-manifest.json direclty but that would also mean figuring out doc-gen's dependency chain and updating those in the manifest accordingly if I did an update...which feels like something lake should do?

[Sebastian Ullrich]

Ok, I wasn't sure on what level you do the substitution. But in the end, updating doc-gen4 sounds like something that should be up to the mathlib4 maintainers and recorded in the manifest like any other dependency. Mathlib4 itself is, perhaps just as much, a consumer of compiler internals as well.

[Henrik Böving]

Ah fair enough I was only thinking about it as a library but of course it has tactics as well.

In that case I'll update the doc-gen4 CI as follows:

• it will periodically (8 hour periods right now, one build is almost at 3h by now) build mathlib4 docs with the doc-gen4 that is in mathlib4 right now
• it will use std4 with the same approach as right now for its own test instead instead since std4 does indeed not have dependencies

[Jireh Loreaux]

Two things:

1. Why is the build so much longer than for mathlib 3? (Curious)
2. Would you mind adding the commit it's building against to the index page?

[Henrik Böving]

Okay I've found another issue while doing this. the manifest.json of mathlib4 does not contain doc-gen4. most likely because you ran lake update without -Kdoc=on so if you want lake to run the doc-gen4 facet against mathlib4 you have to run lake -Kdoc=on right now to even get lake to recognize it as a depnedency. However if doc-gen4 was in the manifest it would be downloaded by every mathlib4 user even if 99.9% don't need it. How do you want to deal with this? Its either add it to your manifest.json and have people download useless data or what you have right now /o\

[Henrik Böving]

Jireh Loreaux said:

Two things:

1. Why is the build so much longer than for mathlib 3? (Curious)
2. Would you mind adding the commit it's building against to the index page?

1. Because doc-gen4 uses LeanInk to render the source code of the page in an interactive/explorable way, this takes up a large time of the build time. If i was to disable this it would go down drastically.
2. Which commit? doc-gens? Or the one of the repo it is working in?

[Henrik Böving]

Henrik Böving said:

Okay I've found another issue while doing this. the manifest.json of mathlib4 does not contain doc-gen4. most likely because you ran lake update without -Kdoc=on so if you want lake to run the doc-gen4 facet against mathlib4 you have to run lake -Kdoc=on right now to even get lake to recognize it as a depnedency. However if doc-gen4 was in the manifest it would be downloaded by every mathlib4 user even if 99.9% don't need it. How do you want to deal with this? Its either add it to your manifest.json and have people download useless data or what you have right now /o\

Oh and...this issue would also be resolved if lake update supported the "only one dep and its transitives" feature^^

[Jireh Loreaux]

2. Maybe both? We have mathlib, Lean, and doc-gen here: https://leanprover-community.github.io/mathlib_docs/index.html

[Henrik Böving]

Okay...I'm not 100% certain how to obtain the commit of doc-gen4 yet but i'll figure it out :thumbs_up:

[Jireh Loreaux]

I'm okay with just mathlib for now, that's what I was originally thinking.

[Henrik Böving]

image.png you'll have it once the build works again then!

[Eric Wieser]

Including the commit of doc-gen4 is probably more useful for you when debugging than it is for mathlib users

[Mario Carneiro]

Henrik Böving said:

Okay I've found another issue while doing this. the manifest.json of mathlib4 does not contain doc-gen4. most likely because you ran lake update without -Kdoc=on so if you want lake to run the doc-gen4 facet against mathlib4 you have to run lake -Kdoc=on right now to even get lake to recognize it as a depnedency. However if doc-gen4 was in the manifest it would be downloaded by every mathlib4 user even if 99.9% don't need it. How do you want to deal with this? Its either add it to your manifest.json and have people download useless data or what you have right now /o\

Would it work to just always build mathlib4:master with doc-gen:master? As mentioned earlier this is what we do in lean 3. Obviously this can still blow up but it should be less often since doc-gen changes less frequently than mathlib/std4

[Henrik Böving]

That's what is currently happening, as outlined above this can work in principle and is merely broken because of the behavior of lake update

[Sebastian Ullrich]

Do we have a Lake issue for that yet?

[Henrik Böving]

Yes its #148 from January

[James Gallicchio]

as far as I remember, the reason we removed doc-gen4 from mathlib's lakefile is because it was forming a circular dependency between doc-gen4 (which relies on mathlib for its test CI) and mathlib (which relied on doc-gen4 as a lake package), which was making it very difficult to update doc-gen4. is my memory right there?

[Henrik Böving]

doc-gen4 is a dependency of mathlib4 it does just not show up in the manifest due to the way it is getting upgraded.

And I also do not rely on it as a dependency , the CI will checkout mathlib4 and update its manifest in such a way that it shows up again and just use the docs facet directly.

[Henrik Böving]

So your memory is doubly wrong :P it is still a dependency you can pull in and the thing you describe is not an issue

[James Gallicchio]

Workaround proposal: have the CI make a new, mostly empty lake project with dependency on mathlib4 and doc-gen4. Then lake update will not update all of mathlib's dependencies :P

[James Gallicchio]

I guess the other workaround would be to inject the necessary doc-gen4 entry in the lake manifest. But that's more annoying/fragile

[Henrik Böving]

James Gallicchio said:

Workaround proposal: have the CI make a new, mostly empty lake project with dependency on mathlib4 and doc-gen4. Then lake update will not update all of mathlib's dependencies :P

Hah, that would probably work out quite nicely indeed...the only issue with this would be that of course the feature that @Jireh Loreaux asked for regarding the commit would break. This is because doc-gen4 is obviously not looking for some dependency named mathlib4 while generating the docs side (after all it is supposed to be general purpose) but instead takes the commit of the repository it is in right now. But if people are fine with not having the commit of matlhib4 on the main page until the lake thing is fixed I can try it like that and hopefullly not stumble upon something that breaks its again while implementing.

[James Gallicchio]

I was thinking this could be just for the testing CI

[James Gallicchio]

but I see now that the issue persists for the actual mathlib docs too...

[James Gallicchio]

It feels like https://github.com/leanprover/lake/issues/148 should not be too hard to fix. I can try to put a PR together this week

[James Gallicchio]

(@ zulip maintainers, why does lake#148 link to leanprover-community/lake instead of leanprover/lake? :thinking:)

[Eric Wieser]

(Because no one added a special rule for lake like we did for lean4, so it's falling back on the default. Ask in #Zulip meta > Linkifiers or a similar thread to get it fixed)

[Heather Macbeth]

How often are the docs supposed to be updated nowadays? Currently they seem to be on a four-day-old commit.

[Henrik Böving]

It should be on an 8 hour basis but it appears the CI has been failing with some funky panic for the past few tries. However since we moved the build to mathlib4 I don't get emails when that happens anymore so someone has to tell me. I'll bump doc-gen and see if that helps

[Henrik Böving]

That did not help...

[Henrik Böving]

Okay so we seem to be getting a ginormous panic that starts with:

Inking: Mathlib.Tactic.Ring.Basic
stderr:
PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:839:14: unknown metavariable
backtrace:
./lake-packages/doc-gen4/build/bin/doc-gen4(lean_panic_fn+0x9e)[0x558bc5f1280e]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_SynthInstance_MkTableKey_normLevel+0x3b0)[0x558bc37455a0]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_List_mapM_loop___at_Lean_Meta_SynthInstance_MkTableKey_normExpr___spec__2+0x15d)[0x558bc374677d]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x104)[0x558bc37469c4]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x3fa)[0x558bc3746cba]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_SynthInstance_mkTableKey___at_Lean_Meta_SynthInstance_main___spec__1+0xdc)[0x558bc378168c]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_SynthInstance_main___lambda__1+0xd9)[0x558bc3781f79]
./lake-packages/doc-gen4/build/bin/doc-gen4(lean_apply_3+0x3d4)[0x558bc5f1e864]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Core_withCurrHeartbeats___at_Lean_Meta_SynthInstance_main___spec__3+0x29)[0x558bc3781d49]
./lake-packages/doc-gen4/build/bin/doc-gen4(lean_apply_5+0x3a0)[0x558bc5f20300]
./lake-packages/doc-gen4/build/bin/doc-gen4(l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___rarg+0x461)[0x558bc3dfe721]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_withNewMCtxDepth___at___private_Lean_Meta_WHNF_0__Lean_Meta_toCtorWhenK___spec__1___rarg+0x20)[0x558bc3695130]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_Lean_Meta_synthInstance_x3f___lambda__6+0x1474)[0x558bc37919c4]

....anyone has an idea on what we could do to debug here?

[Kyle Miller]

I got as far as seeing that it's something that _resolveTacticList calls while processing (I think) Mathlib.Tactic.Ring.Basic.

This line seems suspicious since future lines don't always use ctx? rather than ctx. Getting this context right is needed to get the correct metavariable context, which is consistent with an "unknown metavariable" error

[Kyle Miller]

Maybe let some ctx := info.updateContext? ctx | return aux instead? (while making sure to change the ctx? on the following line to ctx)

[Kyle Miller]

I can confirm that generating the docs for Mathlib.Tactic.Ring.Basic panics, but this let some ctx := ... doesn't fix it. (Also, replacing the body of _resolveTacticList with return aux prevents the panic, so that localizes it a little.)

[Kyle Miller]

Maybe if someone has time to try to minimize this, what I've found so far is it seems that there's some have expression in Mathlib.Tactic.Ring.Basic whose binding value contains a metavariable at some point, and the panic occurs when pretty printing the binding value. (There's a delabLetFun delaborator in the panic trace)

[Mario Carneiro]

I'm testing out the following patch:

    match info.updateContext? ctx? with
    | some ctx => do
      let resolvedChildrenLeafs ← children.toList.mapM (_resolveTacticList ctx aux)

but I've never run leanink before so I'm not sure what to expect

[Mario Carneiro]

I get a crash without an error report

[Mario Carneiro]

I'm not getting any successful runs

[Henrik Böving]

Great news we have two issues now!

1. The runner seems to be running out of disk space?! I am guessing this is because it isn't cleaning up after itself properly? Either way this is no bueno
2. I have still not been able to figure out what the heck is going on with the original issue /o\

[Jireh Loreaux]

Do we know if this is a LeanInk problem? If so, disabling LeanInk to have docs that build would be worth it IMHO.

[Henrik Böving]

The stack trace seems to indicate it is at least related. I'll try that once I'm home.

[Henrik Böving]

Wait what

[Henrik Böving]

image.png
it just...passed?

[Henrik Böving]

I hadn't touched a thing when this started running

[Henrik Böving]

I...guess I'll just revert the disabling change and we see if it remains stable? But this is very strange.

[Henrik Böving]

image.png
well I guess it is working stable again! You are welcome :P

[Pol'tta / Miyahara Kō]

Recently, building docs always fails in RingTheory.ClassGroup. What's the problem in this file?

[Henrik Böving]

No its failing at Mathlib.Tactic.Ring.Basic as far as I can see. This was what was happening above as well, it is related to some bug in LeanInk most likely but nobody seems too be able to figure out precisely what is going wrong and on top of that for some reason it does not always happen either as the succesful builds in between show...

[Henrik Böving]

There is still the option to just disable LeanInk floating around if it keeps failing though

[Henrik Böving]

I disabled LeanInk for now...this has the positive side effect of doc-gen build times again reducing from 2h and a little bit to a mere 50 min!