how to generate html documentation for new lean file

Stream: lean4

[Yufei Liu]

Hi everyone,

I've created a new .lean file with new theorems using existing theorems from Mathlib's linear algebra section only in proof. Now, I'm looking to document this theorem in HTML format, similar to the existing Lean Mathlib Documentation.

Is there a way to generate this specific documentation?

[Marcus Rossel]

https://github.com/leanprover/doc-gen4

[Yufei Liu]

Marcus Rossel said:

https://github.com/leanprover/doc-gen4

thanks, ive come across this, but when i run:
lake -R -Kenv=dev build Test:docs
it has an error:
error: unknown short option '-R'

what does it mean?

[Henrik Böving]

That your lean version is too old most likely.

[Yufei Liu]

how do i check my lean version and how do i update?

[Henrik Böving]

It's in the lean-toolchain file of your projct

[Yufei Liu]

thanks, it's leanprover/lean4:v4.0.0, how do i update

[Ruben Van de Velde]

Do you use mathlib as a dependency?

[Yufei Liu]

nope i just clone the whole repo

[Yufei Liu]

should i use it as dependency?

[Ruben Van de Velde]

Either could work, but the advice will depend on your situation

[Ruben Van de Velde]

Can't check right now, but you should be able to find how mathlib generates documentation and just use that

[Yufei Liu]

i just cloned a whole brand new branch from master branch
and i try to run
lake -Kdoc=on build Mathlib:docs
but got error:
error: unknown library facet docs``
why is that?

[Henrik Böving]

The R flag is missing

[Yufei Liu]

thanks, that fixed the problem

another question i have is what if i only want to build part of mathlib?

for example: lake -R -Kdoc=on build Mathlib/LinearAlgebra:docs
is that the right thing to do (seems like not, it'll return unknown target error)

[Brendan Seamas Murphy]

Henrik Böving said:

The R flag is missing

Ah it looks like it's missing in the mathlib github readme. What does adding this flag do?

[Henrik Böving]

As per a design decision made a little while back the -K stuff is not a one time CLI thing but instead a cmake style configuration flag. That means that you explicitly have to reconfigure (that's -R) the lake project with that flag.

[Mario Carneiro]

I think I managed to convince @Mac Malone to change that a while ago, although I think nothing has happened to the implementation yet. Probably there should be an issue tracking it if there isn't already

[Yufei Liu]

still have this quesion:

1. what do i do if i only want to build part of mathlib?

for example: lake -R -Kdoc=on build Mathlib/LinearAlgebra:docs
is that the right thing to do (seems like not, it'll return unknown target error)

and also i have some new problems:

2. I simply add a new .lean file inside the Mathlib folder, and after I run lake -R -Kdoc=on build Mathlib:docs, seems like the new .lean file does not appeer in the doc folder, why is that?

thanks

[Kim Morrison]

You specify the targets as module names, e.g. lake build Mathlib.LinearAlgebra.Basic

[Kim Morrison]

If you add a new Lean file, you must also import it in Mathlib.lean.

[Yufei Liu]

thanks, that solved the problem