Mathlib directory urls aren't implemented

Stream: mathlib4

[Geoffrey Irving]

Sometimes I am browsing a page of mathlib4 docs, say https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Surreal/Basic.html, and think "I wonder what other files there are under Mathlib/SetTheory/Surreal”. The immediate thing I try is to strip the final filename off the url:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Surreal

But this link doesn't work: it gives a 404 page.

Would it be possible to make directory links show something useful, to enable this kind of browsing?

[Henrik Böving]

If mathlib had Lean files of this name, like for example the Lean compiler does this would work. For example https://leanprover-community.github.io/mathlib4_docs/Lean/Elab.html (the file just happens to be empty but if you check the imports/imported by on the side you will see there is some stuff there.

[Henrik Böving]

The tactic directory does even have such a file: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic.html

[Damiano Testa]

Even just floating to the top of the page the part of the left panel with the folder structure so that you can then see and click the files in the folder could be useful.

[Geoffrey Irving]

Damiano Testa said:

Even just floating to the top of the page the part of the left panel with the folder structure so that you can then see and click the files in the folder could be useful.

Yep, just a file list like that would be great.

[Damiano Testa]

Maybe doc-gen could parse import statements and include links to the explicitly imported files.

[Henrik Böving]

It already does this

[Damiano Testa]

Oh, where?

[Henrik Böving]

image.png

[Henrik Böving]

on every page on the right side

[Damiano Testa]

Ah, I had never noticed this!

[Damiano Testa]

Would it be possible to reproduce browsing like here where clicking on a file takes you to the doc-gen for the file?

[Damiano Testa]

(And by "would it be possible" I meant "is it easy to achieve"!)

[Damiano Testa]

(I guess that this is exactly what Geoffrey had asked about at the beginning of this thread, if I understood correctly.)

[Henrik Böving]

I think printing arbitrary directories as HTML pages is a misrepresentation of what's happening at the Lean level.
If you have a lean file of the same name as the directory it can actually be imported and it can import arbitrary Lean files and do definitions on its own. If you do not have such a file then there is also nothing to import at that point. Currently the web pages are in 1:1 correspondence with "stuff that you can import".

The decision not to show the import tree on the left up to that file when you visit a page was made for the following reason: People also want their import tree state to persist across multiple files. That means if you switch through a few files in rapid succession your left side would look like complete haywire since all of the paths to that file in the tree would be kept open. We can change that to only automatically showing the tree up to the current path but I have the feeling that people will complain about this again because they loose the old behavior.

[Henrik Böving]

And if a directory does have a file on its own that is signified by the file button next to it:
image.png

So as you can see for example ImportGraph does not have a file associated with it while all the other projects do.

[Damiano Testa]

Ok, in fact, that browsing method with the expandable triangles is not my favourite anyway. For me, having a "github like" style browsing of folders with final file-links to doc-gen files would be an improvement.

[Henrik Böving]

https://doc.rust-lang.org/stable/std/alloc/index.html like this?

[Damiano Testa]

Not really, more like this, except happening in doc-gen, so that the files are linked to the doc-gen page, instead of the source code.

[Damiano Testa]

(In fact, I still have not really understood how to navigate folders in https://doc.rust-lang.org/stable/std/alloc/index.html.)

[Damiano Testa]

Basically, reproducing the mathlib folder structure in doc-gen. As Geoffrey points out, this appears to already be the case by looking at the urls for the pages, but the "folder" urls do not work.