docgen: unkown facet `foo:docs´

Stream: general

[Christian Merten]

I am setting up a new lean project on 4.15.0 and want to build documentation pages in the new recommended way as described in the README, but I get the following error message after running lake build foo:docs:

error: unknown executable facet `docs`

To reproduce:

• Run

lake new foo
cd foo
lake update
mkdir docbuild
cd docbuild

• copy the lakefile.toml from the README to a new file lakefile.toml.
• replace Your library name with foo and main with v4.15.0.
• run lake update doc-gen4
• run lake build foo:docs

What am I doing wrong?

[Mauricio Collares]

I wouldn't say you're doing anything wrong per se, but when you do lake new foo (or lake new Foo), lake generates a file with a lean_lib target called Foo and a lean_exe target called foo. docs is a library facet (whatever that means), so you need to run lake build Foo:docs, not lake build foo:docs.

[Mauricio Collares]

That being said, I get a bunch of panics when running lake build Foo:docs on an empty project created via lake new foo.

[Christian Merten]

Thanks, that does something, but indeed, also for me it throws a lot of panics.

[Christian Merten]

Maybe the distinction foo:docs vs Foo:docs could be added to the README.md?

[Mauricio Collares]

I think doc-gen4 doesn't like lean_exe targets at all. If I delete that target, I don't get panics.

[Mauricio Collares]

Easiest way to have a package without lean_exe targets is to create it via lake new foo lib

[Mauricio Collares]

cc @Henrik Böving

[Mauricio Collares]

The panics are fixed in Lean v4.16.0-rc1 (lean4#6374, fixed by lean4#6375), and I think they can be ignored in previous Lean versions (the docs will be generated anyway). Of course, you shouldn't update to v4.16.0-rc1 if you depend on mathlib.

[Christian Merten]

Now I am trying it on a project with mathlib dependency and it has 11690 build targets (roughly two times mathlib + my project) and throws a bunch of WARNING: Failed to calculate equational lemmata for warnings. Is this expected?

[Henrik Böving]

Christian Merten said:

Now I am trying it on a project with mathlib dependency and it has 11690 build targets (roughly two times mathlib + my project) and throws a bunch of WARNING: Failed to calculate equational lemmata for warnings. Is this expected?

Yes, most equational lemmas are too big to be computed in a resonable amount of time.

[Henrik Böving]

Mauricio Collares said:

The panics are fixed in Lean v4.16.0-rc1 (lean4#6374, fixed by lean4#6375), and I think they can be ignored in previous Lean versions (the docs will be generated anyway). Of course, you shouldn't update to v4.16.0-rc1 if you depend on mathlib.

Correct