Documentation build failing on master

Stream: sphere eversion

[Ruben Van de Velde]

Thanks!

I noticed the documentation build is broken on master, but it seems to have been broken since https://github.com/leanprover-community/sphere-eversion/commit/0092b9e50b431cef132e884b03f8022c1d7cca2c

[Michael Rothgang]

Indeed, that build has been broken for three months.

[Michael Rothgang]

Help fixing it is welcome, but not high priority for me.

[Ruben Van de Velde]

Oh, I think I'd need to revert your change to move to lakefile.toml in 9567b65a5232380502b6f0041ce6452decf80823

[Michael Rothgang]

So doc-gen doesn't support a lakefile.toml? That's a shame, is there an issue about this already? In any case, feel free to go ahead.

[Patrick Massot]

Really? That sounds very weird.

[Ruben Van de Velde]

We used to have an optional dependency; I don't know if that's possible with toml

[Ruben Van de Velde]

Maybe there is a way that I just don't know, though

[Ruben Van de Velde]

I also don't know how important it is for the dependency to be optional

[Notification Bot]

9 messages were moved here from #sphere eversion > What is ready for upstreaming? by Ruben Van de Velde.

[Kim Morrison]

Ruben Van de Velde said:

We used to have an optional dependency; I don't know if that's possible with toml

It's not possible. We are hoping that everyone will move away from relying on optional dependencies.

[Kim Morrison]

For doc-gen, one solution (besides just making it a standard dependency, which is a bit clunky), is to have a 2nd repo which depends on main one, and doc-gen, and handles generating the documation separately without interfering with "normal" users.

[Ruben Van de Velde]

Also kinda clunky :)

[Kim Morrison]

Just crosslinking to the discussion of this approach at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/How.20does.20build.20.26.20deploy.20document.20for.20Mathlib4.20currently.3F/near/476591680

[Filippo A. E. Nuccio]

(I have moved my message to a more appropriate stream).

[Michael Rothgang]

I have finally opened https://github.com/leanprover-community/sphere-eversion/pull/91 to fix this. The CI changes are shamelessly copied from the carleson CI workflow. @Pietro Monticone Would you like to double-check this part looks alright?

[Pietro Monticone]

Sure, I’ll take a look at later today (probably during LT2025 social time).

[Pietro Monticone]

Just a quick comment: it might be better to copy the latest docbuild-based version of the Carleson workflow without symlinks.

[Pietro Monticone]

Could you please add the current one? Then I’ll take a look later.

[Michael Rothgang]

Done. (By the way: the setup_lake_package_symlinks.sh script in Carleson is unused: is that safe to delete?)

[Pietro Monticone]

Yes

[Pietro Monticone]

This

uses: actions/checkout@v2

should be upgraded to the latest action version (i.e. v4).

[Pietro Monticone]

This one

actions/deploy-pages@v1

should be upgraded to the latest version (i.e. v4).

[Pietro Monticone]

The following config files are superfluous and should be removed:

• docbuild/lean-toolchain
• docbuild/lake-manifest.json

Everything should be configured and hosted by the workflow runner.

[Pietro Monticone]

Ok, now it looks good to me.

[Michael Rothgang]

Merged the PR: let's see if it works!

[Michael Rothgang]

For those following along: it failed, but Pietro already proposed a fix. Merged that; we'll see if that suffices.

[Pietro Monticone]

Yes, it worked. There is a remaining unrelated checkdecls issue

[Michael Rothgang]

Pushed a fix for that (I think)

[Pietro Monticone]

Fine, it worked.