Docs not updated

Stream: mathlib4

[Anatole Dedecker]

How often is the Mathlib4 Documentation supposed to auto-update itself? It looks like it's currently using a ~1 weel old commit

[Heather Macbeth]

cf

Heather Macbeth said:

I also noticed that recent "build and deploy docs" actions on doc-gen4 seem to have failed:
https://github.com/leanprover/doc-gen4/actions
Is this expected or does something need to be fixed?

[Siddhartha Gadgil]

Indeed doc-gen4 is on an older toolchain (I cannot use it somewhere else for the same reason).

[Anatole Dedecker]

Oh sorry I missed https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Online.20docs
Is there anyone to ping about that? (And is it urgent enough to ping them during the Christmas holiday?)

[Siddhartha Gadgil]

I hope @Henrik Böving won't mind our alerting him to this, in case he had not noticed. Though the lack of lean-toolchain update seems to be upstream in leanink.

[Henrik Böving]

Hah and I was thinking its currently broken because latest std4 doesnt build with latest mathlib4 right now. But I can push a toolchain update of course.

[Henrik Böving]

https://github.com/leanprover/doc-gen4/actions/runs/3758689853/jobs/6387328659 we shall see in half an hour or so then.

[Siddhartha Gadgil]

I did try updating on a fork and leanink failed. The toolchain in leanink seems antique

[Henrik Böving]

Yeah I don't touch LeanInk. But that doesn't matter, lake will use the tool chain of your project to compile everything including your dependencies.

[Siddhartha Gadgil]

What I mean is that some change in lean has broken leanink.

[Siddhartha Gadgil]

Specifically the infoview

[Siddhartha Gadgil]

This has now become more structured where leanink expects a pair

[Siddhartha Gadgil]

Here is the error I am getting after pull

error: > LEAN_PATH=././lake-packages/CMark/build/lib:././lake-packages/lake/build/lib:./build/lib:././lake-packages/Cli/build/lib:././lake-packages/leanInk/build/lib:././lake-packages/Unicode/build/lib LD_LIBRARY_PATH=/home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/lib:/home/gadgil/software/z3/build::./build/lib /home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/bin/lean ./././DocGen4/Process/Base.lean -R ././. -o ./build/lib/DocGen4/Process/Base.olean -i ./build/lib/DocGen4/Process/Base.ilean -c ./build/ir/DocGen4/Process/Base.c
error: stdout:
./././DocGen4/Process/Base.lean:169:6: error: type mismatch
  (fmt, infos)
has type
  ?m.9943 × ?m.9946 : Type (max ?u.9949 ?u.9948)
but is expected to have type
  FormatWithInfos : Type
error: external command `/home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/bin/lean` exited with code 1

[Henrik Böving]

Oh indeed, that gets swallowed by the rest of the compiler output for me, lets see

[Henrik Böving]

Fixed.

[Henrik Böving]

https://github.com/leanprover/doc-gen4/actions/runs/3758972373/jobs/6387964570 and wait again!

[Siddhartha Gadgil]

It worked locally for me.

[Siddhartha Gadgil]

More precisely, it built. I didn't check with another project as there are multiple dependencies all to be updated.

[Siddhartha Gadgil]

Thanks a lot for the fix though.

[Siddhartha Gadgil]

When I try to build docs in a project I am getting a similar error:

Building LeanInk.Analysis.InfoTreeTraversal
error: > LEAN_PATH=././lake-packages/CMark/build/lib:././lake-packages/lake/build/lib:././lake-packages/doc-gen4/build/lib:./build/lib:././lake-packages/Cli/build/lib:././lake-packages/mathlib/build/lib:././lake-packages/Qq/build/lib:././lake-packages/aesop/build/lib:././lake-packages/leanInk/build/lib:././lake-packages/Unicode/build/lib:././lake-packages/std/build/lib:././lake-packages/leanaide/build/lib LD_LIBRARY_PATH=/home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/lib:/home/gadgil/software/z3/build::././lake-packages/leanInk/build/lib /home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/bin/lean ././lake-packages/leanInk/././LeanInk/Analysis/InfoTreeTraversal.lean -R ././lake-packages/leanInk/./. -o ././lake-packages/leanInk/build/lib/LeanInk/Analysis/InfoTreeTraversal.olean -i ././lake-packages/leanInk/build/lib/LeanInk/Analysis/InfoTreeTraversal.ilean -c ././lake-packages/leanInk/build/ir/LeanInk/Analysis/InfoTreeTraversal.c
error: stdout:
././lake-packages/leanInk/././LeanInk/Analysis/InfoTreeTraversal.lean:69:10: error: type mismatch
  (fmt, infos)
has type
  ?m.6795 × ?m.6798 : Type (max ?u.6801 ?u.6800)
but is expected to have type
  FormatWithInfos : Type
././lake-packages/leanInk/././LeanInk/Analysis/InfoTreeTraversal.lean:298:31: warning: unused variable `contextInfo` [linter.unusedVariables]
error: external command `/home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/bin/lean` exited with code 1

[Siddhartha Gadgil]

Seems the same change is needed upstream in LeanInk

[Henrik Böving]

Yeah upstream ink uses the same mechanism and needs the same patch.

[Henrik Böving]

I'm gonna look into merging my fork upstream in the coming days so that should fix it.

[Henrik Böving]

Anatole Dedecker said:

How often is the Mathlib4 Documentation supposed to auto-update itself? It looks like it's currently using a ~1 weel old commit

Oh also to answer this question, right now CI checks every 6 hours since the build is at like, 60~ min by now and updating more frequent just seems like a waste of computing power to me. And I will probably make it longer and longer (at max 24 h though) as build times increase. That is until the cache that is being worked on eventually comes into effect.

[Mario Carneiro]

I think doc-gen should stop building mathlib4 in its CI as an integration test, and instead use something like std which does not have the goal of increasing compile times indefinitely

[Mario Carneiro]

Mathlib4 CI should be building doc-gen for mathlib4

[Siddhartha Gadgil]

"goal of increasing compile times indefinitely" :grinning:

Currently doc-gen is broken for use in other projects as I reported above.

[Henrik Böving]

How? I mean it compiles std4 perfectly fine so thats another project thats just working out. I fixes the lean ink stuff you just have to upgrade.

[Henrik Böving]

Mario Carneiro said:

Mathlib4 CI should be building doc-gen for mathlib4

We can do this but the idea was to leave the burden of "doc-gen broke omg" to me so your CI isn't always red when I'm doing other stuff.

[Siddhartha Gadgil]

Henrik Böving said:

How? I mean it compiles std4 perfectly fine so thats another project thats just working out. I fixes the lean ink stuff you just have to upgrade.

Thanks. I will try to narrow my error.

[Siddhartha Gadgil]

For some reason my lake-manifest is pointing at an old version of leanInk even after updating. I will fix this and see.

[Siddhartha Gadgil]

Yes, the fix works fine. For some reason lake was adding an older commit to my manifest so things were not working. When I updated the lake-manifest file everything is fine.

[Mario Carneiro]

Henrik Böving said:

Mario Carneiro said:

Mathlib4 CI should be building doc-gen for mathlib4

We can do this but the idea was to leave the burden of "doc-gen broke omg" to me so your CI isn't always red when I'm doing other stuff.

Well ideally it wouldn't be breaking all the time. I would prefer we fix our processes so it can be always-green

[Henrik Böving]

I mean, it almost always breaks because one of the following:

• Mac changed something up in Lake again
• There was actually a breaking change in a Lean API itself (let it be type or semantic based)
• std4 master is not compatible with mathlib4 master (that usually resolves itself)

I don't see how to "fix" the first two, itw ill just happen.

[Mario Carneiro]

they are fixed by having doc-gen get bumped as a group with std4 and mathlib4

[Henrik Böving]

Sure if you want that I can give you the private key to push to the mathlib4_docs repo so you can set that up as a secret in the mathlib4 CI and I can make a PR to build docs there.

[Henrik Böving]

When I run doc-gen4 on mathlib right now I get quite a weird error:

Documenting module: Mathlib.Util.Export
error: > LEAN_PATH=././lake-packages/CMark/build/lib:././lake-packages/lake/build/lib:././lake-packages/doc-gen4/build/lib:././lake-packages/Cli/build/lib:./build/lib:././lake-packages/Qq/build/lib:././lake-packages/aesop/build/lib:././lake-packages/leanInk/build/lib:././lake-packages/Unicode/build/lib:././lake-packages/std/build/lib LD_LIBRARY_PATH=/home/nix/.elan/toolchains/leanprover--lean4---nightly-2022-12-22/lib:./build/lib /home/nix/.elan/toolchains/leanprover--lean4---nightly-2022-12-22/bin/lean -DwarningAsError=true ./././Mathlib/Data/Int/Basic.lean -R ././. -o ./build/lib/Mathlib/Data/Int/Basic.olean -i ./build/lib/Mathlib/Data/Int/Basic.ilean -c ./build/ir/Mathlib/Data/Int/Basic.c
error: stdout:
./././Mathlib/Data/Int/Basic.lean:278:44: error: Declaration Int.toNat_add_toNat_neg_eq_nat_abs not found.
(add `set_option align.precheck false` to suppress this message)
error: external command `/home/nix/.elan/toolchains/leanprover--lean4---nightly-2022-12-22/bin/lean` exited with code 1

Is this expected? Will it just clear itself up with time?

[Gabriel Ebner]

Is this expected?

This is because of the std4 update.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gabriel Ebner]

I think Henrik just did a lake update -Kdoc=on to pick up the new doc-gen4 version and hoped for the best.

[Gabriel Ebner]

But this is going to be fixed real soon now: mathlib4#1191

[Henrik Böving]

Gabriel Ebner said:

I think Henrik just did a lake update -Kdoc=on to pick up the new doc-gen4 version and hoped for the best.

Exactly this /o\

[Henrik Böving]

It would be cool if lake provided an option only to update a certain dependency (and its transitive dependencies)