New recommended default setup for doc-gen4

Stream: lean4

[Henrik Böving]

Given that people seem to be struggling with the previously recommended doc-gen setup and converging to the one that we've been using to build mathlib for a while I changed the recommended doc-gen default setup: https://github.com/leanprover/doc-gen4?tab=readme-ov-file#usage.

This is probably of interest to at least @Pietro Monticone for blue prints and potentially @François G. Dorais who is working on something like this in batteries somewhere afaik?

[Yaël Dillies]

Amazing! Will try it out

[Kim Morrison]

@François G. Dorais, when you have a moment would you mind comparing your batteries#1028 against Henrik's linked write up above?

[François G. Dorais]

@Kim Morrison They're essentially the same. The only difference I additionally use the build directory "." to avoid moving the doc directories before deploying to github pages.

[Pietro Monticone]

Thank you. I’ll integrate it in LeanProject and LeanBlueprint when I find the time.

[Pietro Monticone]

Working on these draft PRs that needs to be compatible:

• LeanBlueprint: https://github.com/PatrickMassot/leanblueprint/pull/60
• LeanProject: https://github.com/pitmonticone/LeanProject/pull/11

[Pietro Monticone]

@Henrik Böving @Kim Morrison would this docbuild setup imply 10GB per Lean project?

With two nested projects we are doubling the memory required, right? Am I missing something?

[Henrik Böving]

We're not doubling anything. The nested project automatically reuses build artifacts from its parent. The only change is that if you actually decide to build the nested project you pull in doc-gen etc and put the docs there. As long as a user doesnt build docs locally this is a noop

[Pietro Monticone]

But it would be a problem for github actions, right?

[Pietro Monticone]

I'm saying this because I tested the new setup on a project, adapted the blueprint workflow accordingly and I got no space left on device indicating that the Docker container does not have sufficient disk space to complete the pull and extraction of the texlive-full image in the "Build blueprint and copy to home_page/blueprint" step of the "Compile Blueprint" workflow.

image

[Henrik Böving]

Afaict nothing in that CI screen shot is even close to do anything with doc-gen?

[Pietro Monticone]

I will investigate it better later today. Thanks.

[Pietro Monticone]

I followed the instructions here.

However, when I run lake update within the docbuild directory, it generates a .lake folder containing mathlib which is approximately 5 GB in size.

[Henrik Böving]

Hm, let's see. @Mac Malone if we have nested lake projects to the child projects properly reuse build artifacts from the other ones?

[Mac Malone]

@Henrik Böving Different workspaces do not share dependencies, no. (There is, after all, no guarentee they use they same version of the dependencies.)

[Henrik Böving]

Mac Malone said:

Henrik Böving Different workspaces do not share dependencies, no. (There is, after all, no guarentee they use they same version of the dependencies.)

Is there a way we could make them share build artefacts if they are common easily?

[Henrik Böving]

I imagine we might be able to just symlink .lake?

[Mac Malone]

One could use symlinks for .lake/packages/<shared-package>.

[Henrik Böving]

Great

[Henrik Böving]

@Pietro Monticone in that case the CI script should create docbuild/.lake/packages on it's own and then generate a symlink from .lake/packages/<package-name> to docbuild/.lake/packages/<package-name> and you'll get the desired sharing effects.

[Henrik Böving]

I'll add a note for that in the docs

[Pietro Monticone]

Ok, I'll take a look at it later. Thanks.

[Pietro Monticone]

What should I do locally?

[Henrik Böving]

@Pietro Monticone I updated the notes in doc-gen's README, it worked for me locally with mathlib and its dependencies, please do tell if it doesn't in your setup

[Pietro Monticone]

Yes, it worked locally for me too. Thanks.

[Pietro Monticone]

I have just tested on the project mentioned above and everything works as expected.

[Pietro Monticone]

Tested on Carleson too :check:

[François G. Dorais]

@Mac Malone What goes wrong if the parent package directory is used for both? Since the main is required by path ".." there shouldn't be any conflicts?

[François G. Dorais]

I've had success using:

name = "docbuild"
reservoir = false
buildDir = "."
packagesDir = "../.lake/packages"

[[require]]
name = "doc-gen4"
git = "https://github.com/leanprover/doc-gen4"
rev = "main"

[[require]]
name = "my-lib"
path = ".."

That way both the main and docbuild packages share the same packages directory, avoiding any duplication.

The buildDir = "." puts doc and doc-data directly in the docbuild directory and results in no .lake directory at all in docbuild.

[François G. Dorais]

@Mac Malone does this seem sound?

[Mac Malone]

@François G. Dorais Looks reasonable to me. I honestly forgot that configuring the packages directory is one way to share packages.

[François G. Dorais]

Thanks @Mac Malone! Also, should the require order be my-lib first and then doc-gen4 or the other way around? I always forget which one gets priority...

[Mac Malone]

@François G. Dorais Currently the first gets priority, in the next release it will be the last. It probably doesn't matter in this case.

[Henrik Böving]

Ah great, I shall change the doc-gen setup in the README to that then

[Henrik Böving]

Okay I pushed another update to the README, there is one thing to keep in mind with respect to lake update that I noted there. @François G. Dorais @Pietro Monticone

[Pietro Monticone]

Great, I will adapt the workflows accordingly later today.

[Pietro Monticone]

I followed the instructions here, but when I run lake update within docbuild I get the following error:

uncaught exception: no such file or directory (error code: 2)
  file: .lake/packages/mathlib/lakefile.lean
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4 to '././../.lake/packages/doc-gen4'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean to '././../.lake/packages/MD4Lean'
info: BibtexQuery: cloning https://github.com/dupuisf/BibtexQuery to '././../.lake/packages/BibtexQuery'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic to '././../.lake/packages/UnicodeBasic'
info: mathlib: running post-update hooks
error: mathlib: failed to fetch cache

[Henrik Böving]

Ah this is for one a bug in the mathlibs cripts

[Henrik Böving]

but also a bug in the guide, you probably only want to run lake update doc-gen4

[Henrik Böving]

Then mathlib should not get touched I guess?

[Pietro Monticone]

I did lake update MyLib and it worked.

[Henrik Böving]

What is MyLib and where did you run it

[Pietro Monticone]

No, sorry. It didn't...

Let me try with lake update doc-gen4

[Henrik Böving]

If you are in docbuild and only run lake update doc-gen4 it should hopefully not touch mathlib?

[Pietro Monticone]

Nope, same error:

uncaught exception: no such file or directory (error code: 2)
  file: .lake/packages/mathlib/lakefile.lean
info: docbuild: no previous manifest, creating one from scratch
info: mathlib: running post-update hooks
error: mathlib: failed to fetch cache

[Henrik Böving]

Yeah then that's a bug mathlib has to fix

[Henrik Böving]

At least that is my best guess

[Henrik Böving]

I assume a mathlib script here has hardcoded the access path to the lakefile.lean and that is wrong

[Henrik Böving]

Hm though I don't see it through immediate grep, though it is quite suspicious that it only affects mathlib. just doing this docbuild setup within mathlib doesn't break any of its dependencies in this way

[Henrik Böving]

so it is certainly something specific to the mathlib setup

[Henrik Böving]

@Pietro Monticone can you reproduce the issue when doing this inside of a mathlib checkout? I can't

[Henrik Böving]

If not it is related to some mathlib script that is running and someone that knows those scripts should probably look at it

[Pietro Monticone]

No, inside a mathlib checkout I don't get any errors:

Decompressing 9 file(s)
Unpacked in 2980 ms
Completed successfully!
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4 to '././../.lake/packages/doc-gen4'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean to '././../.lake/packages/MD4Lean'
info: BibtexQuery: cloning https://github.com/dupuisf/BibtexQuery to '././../.lake/packages/BibtexQuery'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic to '././../.lake/packages/UnicodeBasic'
info: mathlib: running post-update hooks

[Henrik Böving]

Right, in that case it is most likely a location in mathlib that does not respect packagesDir and instead blindly grabs into .lake/packages

[Henrik Böving]

Hm, maybe https://github.com/leanprover-community/mathlib4/blob/master/Cache/IO.lean#L81-L82 but I don't have any insight into what mathlib runs upon a lake update

[Henrik Böving]

@Mario Carneiro if we run a lake update in a project that depends on mathlib, does that automatically trigger a lake exe cache or some other mathlib script that could potentially blindly grab into .lake/packages instead of respecting the packagesDirentry in the lake-manifest.json in the directory that it is being called in?

[Pietro Monticone]

Oh, yes. It does.

[Pietro Monticone]

I remember seeing it once a few months ago.

[Ruben Van de Velde]

Yes, this is in mathlib's lakefile.lean

[Ruben Van de Velde]

/--
When a package depending on Mathlib updates its dependencies,
update its toolchain to match Mathlib's and fetch the new cache.
-/
post_update pkg do
  let rootPkg ← getRootPackage
  if rootPkg.name = pkg.name then
    return -- do not run in Mathlib itself
  /-
  Once Lake updates the toolchains,
  this toolchain copy will be unnecessary.
  https://github.com/leanprover/lean4/issues/2752
  -/
  let wsToolchainFile := rootPkg.dir / "lean-toolchain"
  let mathlibToolchain := ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
  IO.FS.writeFile wsToolchainFile mathlibToolchain
  if (← IO.getEnv "MATHLIB_NO_CACHE_ON_UPDATE") != some "1" then
    /-
    Instead of building and running cache via the Lake API,
    spawn a new `lake` since the toolchain may have changed.
    -/
    let exitCode ← IO.Process.spawn {
      cmd := "elan"
      args := #["run", "--install", mathlibToolchain.trim, "lake", "exe", "cache", "get"]
    } >>= (·.wait)
    if exitCode ≠ 0 then
      logError s!"{pkg.name}: failed to fetch cache"

[Henrik Böving]

right

[Henrik Böving]

https://github.com/leanprover-community/mathlib4/blob/master/Cache/IO.lean#L81-L82 then this line needs to be fixed to respect the lake manifest.

[Henrik Böving]

I'm feeling a little uncertain about recommending this setup publicly now tbh, it seems the eco system is not at the point yet where we can just do fancy things like this in the lakefile without breakages :/

[Henrik Böving]

Ruben Van de Velde said:

/--
When a package depending on Mathlib updates its dependencies,
update its toolchain to match Mathlib's and fetch the new cache.
-/
post_update pkg do
  let rootPkg ← getRootPackage
  if rootPkg.name = pkg.name then
    return -- do not run in Mathlib itself
  /-
  Once Lake updates the toolchains,
  this toolchain copy will be unnecessary.
  https://github.com/leanprover/lean4/issues/2752
  -/
  let wsToolchainFile := rootPkg.dir / "lean-toolchain"
  let mathlibToolchain := ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
  IO.FS.writeFile wsToolchainFile mathlibToolchain
  if (← IO.getEnv "MATHLIB_NO_CACHE_ON_UPDATE") != some "1" then
    /-
    Instead of building and running cache via the Lake API,
    spawn a new `lake` since the toolchain may have changed.
    -/
    let exitCode ← IO.Process.spawn {
      cmd := "elan"
      args := #["run", "--install", mathlibToolchain.trim, "lake", "exe", "cache", "get"]
    } >>= (·.wait)
    if exitCode ≠ 0 then
      logError s!"{pkg.name}: failed to fetch cache"

Thinking some more about this. It would most likely be even better if the specific lake update in question here just doesnt trigger this post update hook as it doesnt actually update mathlib. But I guess that requires additional lake support

[François G. Dorais]

Maybe a temporary patch for packages that depend on mathlib is to add a symlink from .lake/build pointing to ../.lake/build?

[Henrik Böving]

What's the issue with fixing the cache script? That sounds doable doesn't it?

[François G. Dorais]

I think so but I don't really have the bandwidth right now. Something like how I patched doc-gen4 should work.

[François G. Dorais]

(In other words, have the get functions take an optional --build argument specifying the build directory.)

[François G. Dorais]

Or adding instructions to set MATHLIB_NO_CACHE_ON_UPDATE=1 before building docs?

[Mac Malone]

Henrik Böving said:

I'm feeling a little uncertain about recommending this setup publicly now tbh, it seems the eco system is not at the point yet where we can just do fancy things like this in the lakefile without breakages :/

I think there is two sides to this. On one hand, cache will hopefully be eventually integrated with Lake and thus not overassume like this (preventing the breakage). On the other hand, having more packages which do fancy things helps discourage writing tools that overassume structure (as they will break).

[François G. Dorais]

I originally misread your second sentence. Yes, I agree with you.

[François G. Dorais]

Maybe there could be a curated collection of lake scripts somewhere.

[Yaël Dillies]

I am rereading this thread now, and my sentiment of whether I should switch my projects over to the new setup is: "Maybe, maybe not?". Am I right in my analysis? Did I miss any development in the past two weeks or so?

[Mac Malone]

As François hinted at, the Mathlib error can be avoided with the following:

MATHLIB_NO_CACHE_ON_UPDATE=1 lake update

Improvements to Lake / Mahtlib Cache which will remove the need for this workaround will come down the line, but this is currently a quick way to solve the isssue. It is also probably worth noting that the failure of a post-update hook does not actually prevent the underlying update from succeeding (as they are run after the update). So one can also just ignore the error.

[Yaël Dillies]

Could we get instructions for how to bump mathlib with this new setup? I find it hard to get right

[Yaël Dillies]

Here is what I've tried (running in the root folder):

lake update mathlib
cd docbuild
lake update doc-gen4
cd ..

[Yaël Dillies]

In APAP, the second lake update fails with

info: toolchain not updated; already up-to-date
warning: ././../.lake/packages/doc-gen4/lakefile.lean:141:2: warning: `Lake.Job.bindSync` has been deprecated: use `Lake.Job.mapM` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean:142:29: error: type mismatch
  tryJson <|> tryBib <|> tryBibFailed
has type
  JobM (Array String × BuildTrace) : outParam Type
but is expected to have type
  EStateT Log.Pos JobState BaseIO ?m.6450 : Type

error: ././../.lake/packages/doc-gen4/lakefile.lean:143:20: error: invalid field 'mix', the environment does not contain 'Lake.BuildContext.mix'
  exeTrace
has type
  BuildContext

warning: ././../.lake/packages/doc-gen4/lakefile.lean:144:16: warning: `Lake.buildFileUnlessUpToDate` has been deprecated: use `Lake.buildFileUnlessUpToDate'` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean:144:16: error: type mismatch
  buildFileUnlessUpToDate outputFile depTrace do
    let __do_lift ← getAugmentedEnv
    liftM
        (proc
          { stdin := IO.Process.Stdio.inherit, stdout := IO.Process.Stdio.inherit, stderr := IO.Process.Stdio.inherit,
            cmd := exeFile.toString, args := #["bibPrepass"] ++ args, cwd := none, env := __do_lift, setsid := false })
has type
  JobM BuildTrace : Type
but is expected to have type
  EStateT Log.Pos JobState BaseIO ?m.7717 : Type

error: ././../.lake/packages/doc-gen4/lakefile.lean:150:11: error: application type mismatch
  pure (outputFile, trace)
argument
  (outputFile, trace)
has type
  FilePath × ?m.7702 : Type
but is expected to have type
  FilePath : Type

error: ././../.lake/packages/doc-gen4/lakefile.lean:154:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.9372
Additional diagnostic information may be available using the `set_option diagnostics true` command.

warning: ././../.lake/packages/doc-gen4/lakefile.lean:158:19: warning: `Lake.BuildJob.mixArray` has been deprecated: use `Lake.Job.mixArray` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:162:2: warning: `Lake.BuildJob.bindAsync` has been deprecated: use `Lake.Job.bindM` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean:163:4: error: invalid field notation, type is not of the form (C ...) where C is a constant
  bibPrepassJob
has type
  ?m.11853 mod exeJob

warning: ././../.lake/packages/doc-gen4/lakefile.lean:176:49: warning: `Lake.BuildJob` has been deprecated: use `Lake.Job` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean:178:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.11995
Additional diagnostic information may be available using the `set_option diagnostics true` command.

error: ././../.lake/packages/doc-gen4/lakefile.lean:182:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  bibPrepassJob
has type
  ?m.13321 exeJob

warning: ././../.lake/packages/doc-gen4/lakefile.lean:195:2: warning: `Lake.BuildJob.mixArray` has been deprecated: use `Lake.Job.mixArray` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:199:19: warning: `Lake.BuildJob.mixArray` has been deprecated: use `Lake.Job.mixArray` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:226:2: warning: `Lake.Job.bindAsync` has been deprecated: use `Lake.Job.bindM` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:227:4: warning: `Lake.Job.bindAsync` has been deprecated: use `Lake.Job.bindM` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:228:6: warning: `Lake.BuildJob.bindSync` has been deprecated: use `Lake.Job.mapM` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean:229:52: error: application type mismatch
  List.cons exeTrace
argument
  exeTrace
has type
  BuildContext : Type
but is expected to have type
  BuildTrace : Type

error: ././../.lake/packages/doc-gen4/lakefile.lean:229:62: error: application type mismatch
  List.cons coreInputTrace
argument
  coreInputTrace
has type
  BuildContext : Type
but is expected to have type
  BuildTrace : Type

warning: ././../.lake/packages/doc-gen4/lakefile.lean:230:20: warning: `Lake.buildFileUnlessUpToDate` has been deprecated: use `Lake.buildFileUnlessUpToDate'` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:243:19: warning: `Lake.BuildJob.mixArray` has been deprecated: use `Lake.Job.mixArray` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:250:2: warning: `Lake.Job.bindAsync` has been deprecated: use `Lake.Job.bindM` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:251:3: warning: `Lake.Job.bindAsync` has been deprecated: use `Lake.Job.bindM` instead

warning: ././../.lake/packages/doc-gen4/lakefile.lean:252:6: warning: `Lake.BuildJob.bindSync` has been deprecated: use `Lake.Job.mapM` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean:253:52: error: application type mismatch
  List.cons exeTrace
argument
  exeTrace
has type
  BuildContext : Type
but is expected to have type
  BuildTrace : Type

error: ././../.lake/packages/doc-gen4/lakefile.lean:253:62: error: application type mismatch
  List.cons coreInputTrace
argument
  coreInputTrace
has type
  BuildContext : Type
but is expected to have type
  BuildTrace : Type

warning: ././../.lake/packages/doc-gen4/lakefile.lean:254:20: warning: `Lake.buildFileUnlessUpToDate` has been deprecated: use `Lake.buildFileUnlessUpToDate'` instead

error: ././../.lake/packages/doc-gen4/lakefile.lean: package configuration has errors

[Yaël Dillies]

Sorry to be annoying, but Kim has repeatedly asked me to switch from a setup that worked (for me) to a setup that doesn't work (for me) and now my projects are broken :sad: What am I supposed to be doing?

[Henrik Böving]

You pinned doc-gen to v4.15 in your lakefile.toml, that version has to be pulled up as you upgrade of course (as noted in the README I might add)

[Henrik Böving]

The error you are observing is just the recent lake refactoring that went down in 4.16 that broke what doc-gen did so far in 4.15 unfortunately

[Yaël Dillies]

Henrik Böving said:

You pinned doc-gen to v4.15 in your lakefile.toml, that version has to be pulled up as you upgrade of course (as noted in the README I might add)

Yeah, I noticed that just now

[Yaël Dillies]

Henrik Böving said:

The error you are observing is just the recent lake refactoring that went down in 4.16 that broke what doc-gen did so far in 4.15 unfortunately

Are you saying that even if I unpin the doc-gen version, my build will fail?

[Henrik Böving]

No it is fixed in the v4.16 on doc-gen

[Henrik Böving]

But you are currently building a v4.15 doc-gen with v4.16 so that burns

[Yaël Dillies]

Got it! And can you confirm that

lake update mathlib
cd docbuild
lake update doc-gen4
cd ..

is the correct set of instructions to update my project from now on (namely, once I have removed the doc-gen version pin)?

[Henrik Böving]

That should work AFAIK yes

[Yaël Dillies]

I assume it will burn if once again we (⊆ FRO ?) forget to bump doc-gen to the latest toolchain?

[Henrik Böving]

But Kim has a script that ensures we don't now!

[Yaël Dillies]

Yes, I saw :eyes: Just wondering if I can myself add an extra failsafe mechanism on top. Or are you saying it should really never ever happen again?

[Johan Commelin]

I hope that more and more of that script will become part of automated workflows.
My impression is that chances that it happens again are really small now.