Zulip Chat Archive

Stream: Is there code for X?

Topic: Running doc-gen against an external repository

Eric Wieser (Nov 18 2020 at 18:30):

I'm trying to do this in a github action over at pygae/lean-ga#16, but running into lean failing with no diagnostic. Has anyone set this up successfully in a non-mathlib repo before?

Bryan Gin-ge Chen (Nov 18 2020 at 19:53):

doc-gen is unfortunately still mathlib-specific; one of the goals is to make it more generic, but we haven't made much progress on that yet.

Eric Wieser (Nov 18 2020 at 20:16):

Actually I sort of got it working

Eric Wieser (Nov 18 2020 at 20:17):

At least, I can run doc_gen and generate a massive json file

Eric Wieser (Nov 18 2020 at 20:17):

Although I think the json might be interspersed with errors from stdout...

Bryan Gin-ge Chen (Nov 18 2020 at 20:20):

I'd be amazed if you got something useful without making changes to doc-gen, but maybe things have changed since I last looked at it. In any case, feel free to open issues at the doc-gen repo if there are specific things that can be fixed there to make it more usable for you.

Eric Wieser (Nov 18 2020 at 20:24):

I think what I'll probably end up with is mathlib + my project in the HTML, but that's better than nothing

Eric Wieser (Nov 18 2020 at 20:25):

As expected, the json file is prefaced with compiler output because doc-gen uses stdout to write json. Would it be straightforward to change it to write to a named file? Can lean read argv to obtain a filename?

Eric Wieser (Nov 18 2020 at 20:31):

(this is the offending line: https://github.com/leanprover-community/doc-gen/blob/3f9aa62feecb66062091c3633cab08f2f64f8e24/src/export_json.lean#L396)

Eric Wieser (Nov 18 2020 at 21:01):

Ah, sure enough, it's mathlib-specific: https://github.com/leanprover-community/doc-gen/blob/3f9aa62feecb66062091c3633cab08f2f64f8e24/print_docs.py#L46-L54

Eric Wieser (Nov 18 2020 at 21:06):

Created leanprover-community/doc-gen#100 and leanprover-community/doc-gen#99 to fix those two issues

Eric Wieser (Nov 19 2020 at 15:15):

Got it working: https://pygae.github.io/lean-ga/ (using leanprover-community/doc-gen#102 + github action hacks)

Gabriel Ebner (Nov 19 2020 at 15:24):

The lean-ga links don't work: https://pygae.github.io/lean-ga/lean-ga/geometric_algebra/nursery/instances

Eric Wieser (Nov 19 2020 at 15:24):

Yeah, I'm fixing that right now

Eric Wieser (Nov 19 2020 at 15:24):

Double lean-ga in the URL

Eric Wieser (Nov 19 2020 at 15:24):

Looks like module docstrings might be missing too

Gabriel Ebner (Nov 19 2020 at 15:24):

I like the core/mathlib separation though.

Gabriel Ebner (Nov 19 2020 at 15:25):

Hmmm, none of the links on the left work.

Eric Wieser (Nov 19 2020 at 15:25):

Yeah, all of them have the same problem

Eric Wieser (Nov 19 2020 at 15:25):

core / mathlib was not supposed to be part of the url

Eric Wieser (Nov 19 2020 at 15:25):

Since it's not part of what you type after import

Eric Wieser (Nov 19 2020 at 15:28):

Gabriel Ebner said:

I like the core/mathlib separation though.

That's good, because it would probably be more work to remove it

Eric Wieser (Nov 19 2020 at 15:35):

Links are fixed, but the sidebar rendering is a bit worse

Bryan Gin-ge Chen (Nov 19 2020 at 16:08):

Thanks for the improvements to doc-gen!

Eric Wieser (Nov 23 2020 at 19:13):

New sidebar is live!

Eric Wieser (Nov 23 2020 at 19:13):

image.png

Last updated: Dec 20 2023 at 11:08 UTC