Zulip Chat Archive

Stream: mathlib4

Topic: Online docs


Yaël Dillies (Dec 12 2022 at 16:01):

Could we restore the view we had with Lean 3 docgen? I see that the file prefix is repeated on subfolders.

Heather Macbeth (Dec 12 2022 at 20:38):

100% agree, note that this was also suggested recently by @Winston Yin.

Heather Macbeth (Dec 13 2022 at 01:01):

I opened an issue for this, I hope the doc-gen4 maintainers don't mind.

Henrik Böving (Dec 13 2022 at 07:12):

I'll add it in the evening

Sebastian Ullrich (Dec 13 2022 at 09:07):

It would also be great to preserve the expansion state of the tree like docgen does, which I guess is done by the saveExpanded JS function

Sebastian Ullrich (Dec 13 2022 at 09:07):

Sorry for piling on when you'd rather work on the compiler :upside_down:

Heather Macbeth (Dec 13 2022 at 09:08):

@Sebastian Ullrich Great minds :)
https://github.com/leanprover/doc-gen4/issues/96

Henrik Böving (Dec 13 2022 at 09:28):

@Sebastian Ullrich well Im still no frontend dev so who knows what's broken really /o\

Sebastian Ullrich (Dec 13 2022 at 09:29):

I don't think there's anything broken, this requires extra code https://github.com/leanprover-community/doc-gen/blob/125e62aea5d95c5991f96599693b4ad1dc0da44b/nav.js#L1

Henrik Böving (Dec 13 2022 at 09:34):

https://github.com/leanprover/doc-gen4/blob/main/static/nav.js but that file does already exist. I also recall it working at some point.

Sebastian Ullrich (Dec 13 2022 at 09:34):

Oh, I see

Henrik Böving (Dec 13 2022 at 19:04):

Fixed both, should deploy in an hour or so, build times are skyrocketing since the port got started for real :tada:

Jireh Loreaux (Dec 13 2022 at 23:05):

Personally, I actually hate the preserved expansion state. Is there a way to either (a) toggle it, or (b) provide a button to close all expanded nodes?

Winston Yin (Dec 13 2022 at 23:07):

Henrik Böving said:

Fixed both, should deploy in an hour or so, build times are skyrocketing since the port got started for real :tada:

Is it already deployed? I'm still seeing the long names

Heather Macbeth (Dec 14 2022 at 02:44):

Jireh Loreaux said:

Personally, I actually hate the preserved expansion state. Is there a way to either (a) toggle it, or (b) provide a button to close all expanded nodes?

@Jireh Loreaux Before Henrik's fix, it didn't even expand the path to the file that you were currently looking at. Is that indeed what you would want, or do you want that one to be kept open and the others closed?

Jireh Loreaux (Dec 14 2022 at 02:48):

I would be fine if they were all closed, although I could see some advantage to having the nodes to the current file open. Mainly I just hate having to scroll or else close a bunch of nodes that I had opened within the past week in order to navigate to a file I care about. I guess a Shift + F5 to reload the page might do what I want. But it would be nice if there were a button. It's not pressing or important though.

Heather Macbeth (Dec 16 2022 at 11:49):

I opened a couple more issues relating to the docs. Perhaps other people could look at them and see if they agree, before Henrik or others sink any time into them.
https://github.com/leanprover/doc-gen4/issues/99
https://github.com/leanprover/doc-gen4/issues/100

I also noticed that recent "build and deploy docs" actions on doc-gen4 seem to have failed:
https://github.com/leanprover/doc-gen4/actions
Is this expected or does something need to be fixed?


Last updated: Dec 20 2023 at 11:08 UTC