How does build & deploy document for Mathlib4 currently?

Stream: mathlib4

[SnO2WMaN]

According to https://github.com/leanprover-community/mathlib4/pull/14229, I know "meta if" in mathlib's lakefile.lean for doc-gen has veen removed. And we want to remove "meta if" in our project because it's troublesome when we update deps. However, I think if it's removed, we won't generate & deploy the documentation, so I have a question. What is the workflow for build and deploy Mathlib4 documentation currently? As I saw It seems not to be found way in mathlib4 repository.

[Ruben Van de Velde]

@Kim Morrison may have the link on hand; it's in a separate repository

[Henrik Böving]

https://github.com/leanprover-community/mathlib4_docs

[Notification Bot]

SnO2WMaN has marked this topic as resolved.

[Filippo A. E. Nuccio]

Probably related to this problem : I am trying to build an old mathlib doc for a teaching project for which I do not want to update mathlib. @Yaël Dillies 's suggestion was simply to import Mathlib in the main lean fileand then to build the doc for the project, as this will build the doc for every mathlib file in the project, which will be the "right, old" ones. Unfortunately I cannot make this work, although I followed the instructions here
https://github.com/leanprover/doc-gen4

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Filippo A. E. Nuccio]

Are those instructions still up-to-date?

[Henrik Böving]

You don't need to import Mathlib at the top level, doc-gen picks up on the transitive dependencies of all your files on its own.

[Henrik Böving]

And the instructions are correct yes

[Filippo A. E. Nuccio]

Well, but I only want the mathlib doc, so I only import mathlib, no?

[Filippo A. E. Nuccio]

What I mean is that all other files will be classes, and I do not want any doc for them.

[Filippo A. E. Nuccio]

And at any rate I get an error, that begins with

$ lake -R -Kenv=dev build M2Lyon2425:docs
✖ [7/10123] Building DocGen4.Process.Hierarchy
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake/packages\MD4Lean\.lake\build\lib;.\.\.lake/packages\UnicodeBasic\.lake\build\lib;.\.\.lake/packages\BibtexQuery\.lake\build\lib;.\.\.lake/packages\doc-gen4\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\nf51454h\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\lean.exe .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean -R .\.\.lake/packages\doc-gen4\.\. -o .\.\.lake/packages\doc-gen4\.lake\build\lib\DocGen4\Process\Hierarchy.olean -i .\.\.lake/packages\doc-gen4\.lake\build\lib\DocGen4\Process\Hierarchy.ilean -c .\.\.lake/packages\doc-gen4\.lake\build\ir\DocGen4\Process\Hierarchy.c --json
error: .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean:80:23: unknown identifier 'Std.HashSet'
error: .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean:81:2: unknown identifier 'Std.HashSet.ofList'
warning: .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean:111:4: declaration uses 'sorry'
error: Lean exited with code 1

[Ruben Van de Velde]

Sounds like your version of doc-gen doesn't agree with your version of lean

[Filippo A. E. Nuccio]

Indeed, you're right. I was using v4.11.0-rc2 but doc-gen is now based upon 4.13.0-rc1. Now I do not know how to proceed:

1. If I change the lean-toolchainmy project does not build anymore, because I need to lake update and I don't think I want to do this basically for the same reason that put me in this situation: I do not want to update mathlib because all students have already started working on some version that I do not want to touch.
2. I tried changing "https://github.com/leanprover/doc-gen4" @ "main" with "https://github.com/leanprover/doc-gen4" @ "114aabc6f0f8d117eb1a853c0dc1591126d9c559" (pointing to this commit) but this does not seem to work.

Any idea?

[Ruben Van de Velde]

Did you lake update after that?

[Filippo A. E. Nuccio]

Well, as explained in 1. I do not want to do this...

[Yaël Dillies]

lake update with a pinned dependency won't actually update past the pinned version

[Yaël Dillies]

So you should lake update to see what happens. It won't change the toolchain

[Filippo A. E. Nuccio]

Well, but as @Ruben Van de Velde said if my toolchain is not aligned with the lean version in doc-gen I get an error.

[Filippo A. E. Nuccio]

I think that if I change the toolchain and I lake update with a pinned version of mathlib, this could work (I can try, actually, I am on a trial branch)...

[Filippo A. E. Nuccio]

Let me try

[Ruben Van de Velde]

My point is, just changing lakefile.lean doesn't help, you also need to update the json to match the commit you put in the the lakefile

[Filippo A. E. Nuccio]

Ah, I see. But in the json should I update the commit for doc-gen only or for all the other dependencies?

[Ruben Van de Velde]

I guess lake update doc-gen4 might work?

[Filippo A. E. Nuccio]

Let me try

[Kevin Buzzard]

If only there were a lake downdate

[Filippo A. E. Nuccio]

No, unfortunately after lake update although my lake build gives no error, I am still stuck with the following

$ lake -R -Kenv=dev build M2Lyon2425:docs
✖ [7/10123] Building DocGen4.Process.Hierarchy
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake/packages\MD4Lean\.lake\build\lib;.\.\.lake/packages\UnicodeBasic\.lake\build\lib;.\.\.lake/packages\BibtexQuery\.lake\build\lib;.\.\.lake/packages\doc-gen4\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\nf51454h\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\lean.exe .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean -R .\.\.lake/packages\doc-gen4\.\. -o .\.\.lake/packages\doc-gen4\.lake\build\lib\DocGen4\Process\Hierarchy.olean -i .\.\.lake/packages\doc-gen4\.lake\build\lib\DocGen4\Process\Hierarchy.ilean -c .\.\.lake/packages\doc-gen4\.lake\build\ir\DocGen4\Process\Hierarchy.c --json
error: .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean:80:23: unknown identifier 'Std.HashSet'
error: .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean:81:2: unknown identifier 'Std.HashSet.ofList'
warning: .\.\.lake/packages\doc-gen4\.\.\DocGen4\Process\Hierarchy.lean:111:4: declaration uses 'sorry'
error: Lean exited with code 1

[Filippo A. E. Nuccio]

I am still completely stuck. I think I have tried all possible combinations of

1. Manually changing the lakefile
2. running lake update
3. running lake update doc-gen4

and I still get all sort of errors. @Ruben Van de Velde or @Henrik Böving , do you have any idea?

[Filippo A. E. Nuccio]

Well, I realized that after lake update even if I manually change the lakefile to leanprover/lean4:v4.13.0-rc1, it gets reverted immediately to leanprover/lean4:v4.11.0-rc1, probably because I am forcing the mathlib rev to be an old one what used that version of lean. So I do not really know how to follow @Ruben Van de Velde 's suggestion of having lean and doc-gen4 being aligned on the same version.