Error in CI poss related to new doc-gen setup

Stream: FLT

[Kevin Buzzard]

A PR from a fork FLT#312 which is working locally for me, is failing in CI, with errors which seem to be related to docgen.

* Run MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update FLT || true
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: leanprover/doc-gen4: checking out revision 'f4d724054cac3c910ff00390b21dbe0f7105edac'
info: updating toolchain to 'leanprover/lean4:v4.17.0-rc1'
info: restarting Lake via Elan
info: downloading https://github.com/leanprover/lean4/releases/download/v4.17.0-rc1/lean-4.17.0-rc1-linux.tar.zst
info: installing /home/runner/.elan/toolchains/leanprover--lean4---v4.17.0-rc1
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: Cli: URL has changed; deleting '././../.lake/packages/Cli' and cloning again
info: Cli: cloning https://github.com/mhuisi/lean4-cli
info: Cli: checking out revision 'a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision 'd890360c960358a42965bdc15defa3fd09feba38'
info: BibtexQuery: cloning https://github.com/kim-em/BibtexQuery
info: BibtexQuery: checking out revision '2411c47ee06f2fc986d929e22731c77e61eaadb6'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision '7cf25ec0edf7a72830379ee227eefdaa96c48cfb'
info: mathlib: running post-update hooks
error: ././../.lake/packages/doc-gen4/lakefile.lean:159:16: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module

error: ././../.lake/packages/doc-gen4/lakefile.lean:160:38: error: invalid field notation, type is not of the form (C ...) where C is a constant
  imports
has type
  ?m.11550 mod exeJob bibPrepassJob modJob __do_lift✝

error: ././../.lake/packages/doc-gen4/lakefile.lean:198:13: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
has type
  Array Module
...

Any ideas?

[Yaël Dillies]

What's the toolchain in FLT and is it 4.17.0-rc1?

[Kevin Buzzard]

What worries me is that I'm seeing updating toolchain to 'leanprover/lean4:v4.17.0-rc1' in those messages, but the PR has lean-toolchain on leanprover/lean4:v4.16.0-rc2 and indeed I haven't bumped to v4.17.0-rc1 yet -- it's on my TODO list but I wanted to get some PRs merged first because I felt that I'd be better equipped to fix up errors than the people making the PRs.

[Kevin Buzzard]

The toolchain on the branch is 4.16-rc2 and I am not sure that it's reasonable to tell people making PRs "oh and by the way you must bump mathlib yourself in your PR every time mathlib is bumped to a new Lean version", that's certainly not how mathlib PRs work whenever Lean changes.

[Yaël Dillies]

You can temporarily pin the doc-gen version you're using by replacing the last paragraph in docbuild/lakefile.toml with

[[require]]
scope = "leanprover"
name = "doc-gen4"
rev = "v4.16.0-rc2"

[Kevin Buzzard]

Yes but are you saying "the new doc-gen setup which Kim has encouraged us to switch to has a bunch of unforseen consequences which are going to make all FLT contributors' lives more complicated going forward" or is there some kind of robust fix for this?

[Yaël Dillies]

Longer term, we could do what I offered you just before I left London: Always pin the toolchain version in lakefile.toml and have scripts/bump.sh update it whenever lean-toolchain changes.

[Yaël Dillies]

Alternatively, don't have docbuild/lakefile.toml and instead generate the file on the fly from lean-toolchain

[Kevin Buzzard]

All of this is gobble-de-gook to me, I just want it to work for everyone easily.

[Kevin Buzzard]

I am in no position to choose between these alternatives.

[Kevin Buzzard]

All I know is that it used to work and now it doesn't work

[Yaël Dillies]

I will fix it

[Kevin Buzzard]

But will Kim be happy with your fix? My understanding was that our position was that we wanted to make the FRO happy with our set-up.

[Kevin Buzzard]

(got to go, giving a talk)

[Yaël Dillies]

Kevin Buzzard said:

But will Kim be happy with your fix?

Yes, Kim wanted Kevin Kenv dead, and Kenv is dead indeed

[Yaël Dillies]

Got a decent fix working. Will PR soon

[Kevin Buzzard]

Basically every PR for FLT now has a red X so development is currently stalled on this issue :-( What is your vision for how this will work? Which option did you choose?

[Yaël Dillies]

I chose the option to make docbuild be created by CI. This way, no one can accidentally introduce a toolchain mismatch error in the repo by modifying/forgetting to modify the pinned toolchain in docbuild/lakefile.toml

[Yaël Dillies]

Bonus point is we get rid of the custom script to bump FLT. Malus point is we now have a custom script to build the docs. Bonus point is that the script-less way to build the docs was not very ergonomic anyway, and we bump the repo more often than we build offline docs for it

[Kevin Buzzard]

OK this sounds fabulous!

I'm minded to start merging some PRs and not caring about the red x because I can see that the only failure in CI is this issue. So master will maybe have a red x soon.

[Yaël Dillies]

If you're willing to wait one or two hours, you'll soon get a PR from me

[Kevin Buzzard]

I'll be in a seminar by then, but I'm confident that I'll be able to pick up the pieces later on!

[Yaël Dillies]

FLT#334

[Kevin Buzzard]

CI has failed. It this expected, because it's running old CI on a project which has changed the CI set-up?

[Julian Berman]

No, it's failing because it's looking for docbuild/scripts/build_docs.sh instead of /scripts/build_docs.sh in the repo root, and the fix will probably be that running ../scripts/build_docs.sh was intended if the working directory really needs to be docbuild (and probably Yael will know all this and fix it when they see the error)

[Patrick Massot]

If this discussion converges, it would be nice to know whether the ci setup created by leanblueprint needs to be updated.

[Yaël Dillies]

Which CI setup do you mean precisely, Patrick? Is it the template one that Pietro maintains, or something else?

[Yaël Dillies]

Kevin Buzzard said:

CI has failed. It this expected, because it's running old CI on a project which has changed the CI set-up?

It's expected because I am stupid

[Yaël Dillies]

(I forgot to remove working-directory: docbuild from an invokation that is now supposed to run from the root directory)

[Pietro Monticone]

Patrick Massot said:

If this discussion converges, it would be nice to know whether the ci setup created by leanblueprint needs to be updated.

I think so. I opened a LeanBlueprint PR for that 2 weeks ago, but maybe we find a better solution.

[Ruben Van de Velde]

Looks like docs are down - https://imperialcollegelondon.github.io/FLT/docs/

[Yaël Dillies]

Uhoh, that's probably my fault. Investigating

[Yaël Dillies]

Ah! At the very end of Build project API documentation in https://github.com/ImperialCollegeLondon/FLT/actions/runs/13370724261/job/37338415705:

mv: cannot overwrite 'docs/docs/doc': Directory not empty

[Yaël Dillies]

This comes from scripts/build_docs.sh. Don't really understand why this happens though

[Yaël Dillies]

Ran out of time for now. Feel free to take the investigation over

[Pietro Monticone]

(Deleted: didn’t read the whole thing, sorry. I’ll be able to take a look at it tomorrow)

[Yaël Dillies]

Ruben Van de Velde said:

Looks like docs are down - https://imperialcollegelondon.github.io/FLT/docs/

@Edison Xie and I peeled our eyes trying to find where the error is, and we couldn't spot it. Can anyone give it another look?

[Yaël Dillies]

Oh! The docs are accessible under docs/doc!

[Yaël Dillies]

Somehow mv docbuild/.lake/build/doc docs/build actually moves the content of docbuild/.lake/build/doc to docs/build/doc (instead of docs/build)!

[Yaël Dillies]

Am I being dense here? Should I be adding more slashes somewhere?

[Bryan Gin-ge Chen]

Don't you want something like mv docbuild/.lake/build/doc/* docs/build?

[Yaël Dillies]

I thought mv moved folders to folders :flushed:

[Bryan Gin-ge Chen]

Ah, right, given how it works on files, you might think that, yeah.

[Yakov Pechersky]

A folder is just a file :)

[Yakov Pechersky]

You might prefer rsync in such situations

[Kevin Buzzard]

How do I test this? At least my rudimentary bash knowledge is enough to understand properly how mv works. My problem is that I don't have a clue what's going on. If I edit scripts/build_docs.sh like this:

@@ -44,7 +44,7 @@ MATHLIB_NO_CACHE_ON_UPDATE=1 # Disable an error message due to a non-blocking bu

 # Move them out of docbuild
 cd ../
-mv docbuild/.lake/build/doc docs/docs
+mv docbuild/.lake/build/doc/* docs/build

then run scripts/build_docs.sh from the root of the project I get

mv: cannot move 'docs/docs' to 'docbuild/.lake/build/doc': No such file or directory
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: checking out revision '1213642a40facc6fa368b55e93ded3c97e3f4486'
info: updating toolchain to 'leanprover/lean4:v4.17.0-rc1'
info: restarting Lake via Elan
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: UnicodeBasic: checking out revision 'd890360c960358a42965bdc15defa3fd09feba38'
info: BibtexQuery: URL has changed; deleting '././../.lake/packages/BibtexQuery' and cloning again
info: BibtexQuery: cloning https://github.com/kim-em/BibtexQuery
info: BibtexQuery: checking out revision '2411c47ee06f2fc986d929e22731c77e61eaadb6'
info: MD4Lean: checking out revision '7cf25ec0edf7a72830379ee227eefdaa96c48cfb'
info: mathlib: running post-update hooks
uncaught exception: Failed to prune ProofWidgets cloud release: no such file or directory (error code: 2)
  file: .lake/packages/proofwidgets/.lake/build/lib
error: mathlib: failed to fetch cache
uncaught exception: Failed to prune ProofWidgets cloud release: no such file or directory (error code: 2)
  file: .lake/packages/proofwidgets/.lake/build/lib
⣿ [?/?] Computing build jobs

which doesn't look good to me but then again I'm not at all sure what I'm supposed to be seeing.

[Ruben Van de Velde]

Who was arguing against the previous working setup again? Was that @Kim Morrison ?

[Damiano Testa]

The bash script seems to create a docbuild dir, but then you move to docbuild/.lake/build/doc.

[Damiano Testa]

Should you be creating a chain docbuild/.lake/build/doc of dirs instead?

[Damiano Testa]

It also says

# Fetch the docs cache if it exists
mkdir -p docs/docs
mv docs/docs docbuild/.lake/build/doc

[Damiano Testa]

The comment suggests "fetching", but I do not see that reflected in the script.

[Kevin Buzzard]

Was that @Kim Morrison ?

Yes, and the argument (which Yael was also in favour of) was that it's best to "stick to the script" as much as possible. For example I argued that a file FLT.lean just containing a list of all other files in the repo was just plain stupid given that a script could generate those files and if the system really needed such a file then it should just generate it on the fly and delete it; my FLT.lean was a statement of FLT and I really liked it that way. But Yael argued that all other projects have this moronic convention and it's good to be consistent, not least because I could not use lake exe mk_all for example. Yael and Kim also both argued that this -Kenv=dev or whatever we had to continually type when we had non-standard doc-gen was bad not because we had to type it but because it was non-standard, and I've just come around to the idea over time that if everyone else is doing something in some way then we should also be doing it in the same way.

[Damiano Testa]

I do not really know what the script should be doing, but I would guess from just looking at it very naïvely that replacing

# Create a temporary docbuild folder
mkdir -p docbuild

with

# Create a temporary docbuild folder
mkdir -p docbuild/.lake/build/doc

has a higher chance of working.

[Ruben Van de Velde]

Yeah, I don't disagree with that in general - it just seems like the new setup is much more complex and brittle, and I'd hoped the proponents would be able to quickly diagnose the issue

[Damiano Testa]

At the very least, it will throw an error later than where it is choking now.

[Ruben Van de Velde]

That doesn't seem to make sense to me, Damiano - the doc build is supposed to drop its output somewhere around there, and putting an empty folder there only masks the fact that there's nothing where there should be something

[Damiano Testa]

I think that docs/docs could be already populated with something.

[Damiano Testa]

As in, a previous run might have filled it with stuff and you are "fetching" whatever it contains, if indeed it contains something.

[Damiano Testa]

But I also do not want to give the impression that I know what the script is supposed to do!

[Ruben Van de Velde]

Oh hmm, now that I look at the script, it seems you're correct. Worth trying, then

[Kevin Buzzard]

Damiano Testa said:

I do not really know what the script should be doing, but I would guess from just looking at it very naïvely that replacing

# Create a temporary docbuild folder
mkdir -p docbuild

with

# Create a temporary docbuild folder
mkdir -p docbuild/.lake/build/doc

has a higher chance of working.

Does the next line

# Equip docbuild with the template lakefile.toml
template > docbuild/lakefile.toml

also need changing then?

[Ruben Van de Velde]

I only have a vague impression of how this GitHub caching business works, but does the way that the script moves docs/docs into docbuild/.lake/build/doc and only moves it back once the build succeeded, mean that a broken build effectively clears the cache?

[Ruben Van de Velde]

No, leave the next line

[Damiano Testa]

Ruben Van de Velde said:

I only have a vague impression of how this GitHub caching business works, but does the way that the script moves docs/docs into docbuild/.lake/build/doc and only moves it back once the build succeeded, mean that a broken build effectively clears the cache?

With CI, anything can happen.

[Kevin Buzzard]

Should I be testing this script by just running it on my computer in the root directory of the project, or is that bound to fail for some reason?

[Damiano Testa]

Do you have a docs/docs dir with something inside it?

[Damiano Testa]

In any case, I think that running the script from the root dir of the project "should" work.

[Kevin Buzzard]

I seem to have an empty docs/docs dir right now

[Damiano Testa]

I also feel that if the script does not work in an environment where you control everything, the chances of it working blindly on a computer who knows where are pretty slim.

[Damiano Testa]

Kevin Buzzard said:

I seem to have an empty docs/docs dir right now

Ok, I think that Ruben and I are not convinced of whether that would always be the case in CI, or whether there is a chance that that dir may contain something sometimes.

[Damiano Testa]

In any case, the script should work even if that dir is empty, it just may take longer to run.

[Kevin Buzzard]

I get fewer errors now:

buzzard@brutus:~/FLT$ ./scripts/build_docs.sh
info: docbuild: no previous manifest, creating one from scratch
info: updating toolchain to 'leanprover/lean4:v4.17.0-rc1'
info: restarting Lake via Elan
info: docbuild: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
uncaught exception: Failed to prune ProofWidgets cloud release: no such file or directory (error code: 2)
  file: .lake/packages/proofwidgets/.lake/build/lib
error: mathlib: failed to fetch cache
uncaught exception: Failed to prune ProofWidgets cloud release: no such file or directory (error code: 2)
  file: .lake/packages/proofwidgets/.lake/build/lib
⣿ [?/?] Computing build jobs

[Damiano Testa]

Ah, ProofWidgets is someone else's problem!!! :octopus:

[Damiano Testa]

So, as far as my understanding goes, the docs/docs dir may contains a previous build of the docs when you start the script.

[Ruben Van de Velde]

Oh, is lake exe cache get failing but not terminating the script because that needs a set line at the top of the script?

[Damiano Testa]

If there is something, you cunningly move it to where the CI step that will create it later would create (the .../.lake/... dir).

[Ruben Van de Velde]

And is it rebuilding all of mathlib?

[Damiano Testa]

Then, you tell lean to create the docs: if they already exist, fine, otherwise they will be build.

[Damiano Testa]

Eventually, you move the newly-built-or-previously-built docs back to where they came from.

[Damiano Testa]

The solution for the ProofWidget was the one found by Mauricio? Removing a trace file somewhere?

[Ruben Van de Velde]

I'm somewhat suspicious of the TOOLCHAIN mangling, but maybe that's a red herring

[Kevin Buzzard]

CI always takes forever to run because it always builds all of mathlib docs even though 9 times out of 10 mathlib didn't change when I merge a PR (we bump mathlib every week or two).

[Damiano Testa]

Maybe #mathlib4 > `lake build` work after a successful `lake exe cache get` @ 💬?

[Ruben Van de Velde]

I don't recall if the cache is supposed to help with that, probably not

[Damiano Testa]

I am not sure that what I linked is relevant.

[Ruben Van de Velde]

Anyway, sleep for me

[Damiano Testa]

Same here.

[Damiano Testa]

Honestly, I think that this might be progress, since ProofWidgets has always caused some headaches...

[Kevin Buzzard]

OK so I just merge Damiano's suggested change and see what happens?!

[Damiano Testa]

I suspect that CI will behave similarly to what it does locally for you, but you never know.

[Kevin Buzzard]

oh wait the build finished and it ends with

info: Documentation indexing
Build completed successfully.
mv: target 'docs/build': No such file or directory
buzzard@brutus:~/FLT$

Is that bad?

[Damiano Testa]

Hmm, I cannot see a step that moves to docs/build in the script...

[Damiano Testa]

Was that the error that you got when you ran the script?

[Damiano Testa]

I am guessing that the Build completed successfully. is the output of

# Build the docs
~/.elan/bin/lake build FLT:docs

[Damiano Testa]

The remaining steps are

# Move them out of docbuild
cd ../
mv docbuild/.lake/build/doc docs/docs

# Clean up after ourselves
rm -rf docbuild

[Damiano Testa]

But the target of the unique mv is docs/docs, not docs/build...

[Kevin Buzzard]

Here is the scripts/build_docs.sh file in full, after Damiano's suggested change.

# Build HTML documentation for FLT
# The output will be located in docs/docs

# Template lakefile.toml
template() {
  cat <<EOF
name = "docbuild"
reservoir = false
version = "0.1.0"
packagesDir = "../.lake/packages"

[[require]]
name = "FLT"
path = "../"

[[require]]
scope = "leanprover"
name = "doc-gen4"
rev = "TOOLCHAIN"
EOF
}

# Create a temporary docbuild folder
mkdir -p docbuild/.lake/build/doc

# Equip docbuild with the template lakefile.toml
template > docbuild/lakefile.toml

# Substitute the toolchain from lean-toolchain into docbuild/lakefile.toml
sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml

# Fetch the docs cache if it exists
mkdir -p docs/docs
mv docs/docs docbuild/.lake/build/doc

# Initialise docbuild as a Lean project
cd docbuild
MATHLIB_NO_CACHE_ON_UPDATE=1 # Disable an error message due to a non-blocking bug. See Zulip
~/.elan/bin/lake update FLT
~/.elan/bin/lake exe cache get

# Build the docs
~/.elan/bin/lake build FLT:docs

# Move them out of docbuild
cd ../
mv docbuild/.lake/build/doc/* docs/build

# Clean up after ourselves
rm -rf docbuild

So it
1) creates a directory docbuild/.lake/build/doc if one isn't already there;
2) dumps a docbuild lakefile.toml into docbuild/ but with rev = "TOOLCHAIN"
3) does a cute sed trick to turn that into rev = "v4.17.0-rc1" or whatever
4) makes docs/docs if it doesn't already exist, and moves it to docbuild/.lake/build/doc/docs
5) changes directory to docbuild and then runs two lake commands both of which fail with errors about Proofwidgets
6) runs ~/.elan/bin/lake build FLT:docs which sits on ⣿ [?/?] Computing build jobs for an absolute age

and apparently I also have to go to bed so I'll leave it there (it's been sitting for 5 minutes)

@Yaël Dillies @Pietro Monticone does any of this look right/wrong so far?

[Damiano Testa]

My final guess before really going to bed is that the toolchain modification introduces an incompatibility between the ProofWidget version and causes one of the steps to fail.

[Damiano Testa]

Good luck and Godspeed. And good night!

[Pietro Monticone]

I should have fixed the script. I'm testing the caching mechanism and the website generation now.

[Pietro Monticone]

Caching mechanism tested :check: (link)

[Pietro Monticone]

Website generation tested :check: (link)

[Pietro Monticone]

Ok, everything is fine now.

[Pietro Monticone]

Ready for review FLT#359

[Ruben Van de Velde]

Thanks! Is there a reason you're not running lake exe cache get anymore?

[Pietro Monticone]

Yes, because it’s unnnecessary since lake update already does that.

[Mauricio Collares]

MATHLIB_NO_CACHE_ON_UPDATE is really confusingly named then

[Pietro Monticone]

Ops, sorry, I replied too quickly without thinking.

I removed it because I believed it was unnecessary given that we run it before and then we have packagesDir = "../.lake/packages" in the docbuild .toml file:

name = "docbuild"
reservoir = false
version = "0.1.0"
packagesDir = "../.lake/packages"
…

but I’m not at all sure I’m right about this.

CC: @Kim Morrison @Mac Malone

[Ruben Van de Velde]

Maybe if you add it back, we can look at the logs and see what, if anything, it does

[Pietro Monticone]

Unfortunately I’m from mobile at the moment

[Pietro Monticone]

But I can push it directly to main.

[Pietro Monticone]

Done :check:

[Pietro Monticone]

Nope, it returns an error precisely for the same reason we need the MATHLIB_NO_CACHE_ON_UPDATE of course… Sorry, I’m a bit tired…

I’m going to remove it once again.

[Yaël Dillies]

Sorry, I thought I had made it clear I had a fix in the work :sad:

[Yaël Dillies]

Yesterday, I had time to fix it on LeanAPAP and PFR, then I ran out of time to copy the fix to FLT

[Pietro Monticone]

Is your fix similar to mine?

[Yaël Dillies]

Not really, no

[Pietro Monticone]

Do we have a semi-reliable way to evaluate which one could be better to keep?

[Yaël Dillies]

The fix I have is already successfully tested on two separate repos. And I am trying to keep the CI of the various repos somewhat in sync

[Ruben Van de Velde]

LeanAPAP is still red, and FLT is green :)

[Ruben Van de Velde]

Or red again after the change in https://github.com/YaelDillies/LeanAPAP/commit/16f61b7761caa9784f17b1b22bfe989f4499afb4

[Yaël Dillies]

Yeah I jumbled something unrelated

[Yaël Dillies]

I just reached a computer for the first time of the day, so I'll fix all of this swiftly now

[Ruben Van de Velde]

I don't know that there's anything to fix at this point

[Pietro Monticone]

When I’ll be back home I could take a look at your solution and I’ll be more than happy to adopt it in FLT if it’s simpler, easier to maintain, etc.

[Jz Pan]

Kevin Buzzard said:

uncaught exception: Failed to prune ProofWidgets cloud release: no such file or directory (error code: 2)
  file: .lake/packages/proofwidgets/.lake/build/lib
error: mathlib: failed to fetch cache
uncaught exception: Failed to prune ProofWidgets cloud release: no such file or directory (error code: 2)
  file: .lake/packages/proofwidgets/.lake/build/lib

My experience is that you need to run lake exe cache get in the script twice... as the first run seems always return an error.