Online docs

Stream: mathlib4

[Yaël Dillies]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Henrik Böving]

I'll add it in the evening

[Sebastian Ullrich]

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]

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

[Heather Macbeth]

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

[Henrik Böving]

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

[Sebastian Ullrich]

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]

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]

Oh, I see

[Henrik Böving]

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

[Jireh Loreaux]

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]

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]

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]

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]

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?