Zulip Chat Archive

Stream: Is there code for X?

Topic: Running doc-gen against an external repository


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 18 2020 at 20:16):

Actually I sort of got it working

view this post on Zulip Eric Wieser (Nov 18 2020 at 20:17):

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

view this post on Zulip Eric Wieser (Nov 18 2020 at 20:17):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:24):

Yeah, I'm fixing that right now

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:24):

Double lean-ga in the URL

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:24):

Looks like module docstrings might be missing too

view this post on Zulip Gabriel Ebner (Nov 19 2020 at 15:24):

I like the core/mathlib separation though.

view this post on Zulip Gabriel Ebner (Nov 19 2020 at 15:25):

Hmmm, none of the links on the left work.

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:25):

Yeah, all of them have the same problem

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:25):

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:25):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 19 2020 at 15:35):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 19 2020 at 16:08):

Thanks for the improvements to doc-gen!

view this post on Zulip Eric Wieser (Nov 23 2020 at 19:13):

New sidebar is live!

view this post on Zulip Eric Wieser (Nov 23 2020 at 19:13):

image.png


Last updated: May 16 2021 at 05:21 UTC