Docs navigation

Stream: mathlib4

[Heather Macbeth]

In an issue on the doc-gen4 repo, @Henrik Böving and I have been discussion how to deal with the left sidebar display of names which are both a folder and a file. For instance
Mathlib the folder vs Mathlib the file
Mathlib.Tactic.Linarith the folder vs Mathlib.Tactic.Linarith the file
Usually the situation is that the file represents the default things from the folder that one would want to import somewhere else.

Currently these are displayed in the left sidebar of the docs by making the folder name a hyperlink to the associated file. This has the problem that the screen real-estate to click through to the contents of the folder becomes very small: just the tiny ▸ next to the folder name. This is particularly awkward in the case of Mathlib itself and other top-level folders, because it means that navigating to any file in Mathlib requires first finding the tiny ▸ on the homepage and clicking it.

I proposed just deleting the docs pages associated to folder-namesake files, but Henrik points out that

• in small projects, the repository-namesake file might actually contain content
• even in the typical situation where a folder-namesake file is just a list of imports (and therefore the associated docs page is completely empty), that list of imports still generates useful information in the right sidebar (Imports/Imported by)

So let's discuss. I would like a solution in which the folder gets more screen real estate than the file. The best display I can currently think of is

▸ Mathlib (file)

Maybe we could also systematically put comments in such files, like we did in default files in mathlib3, so that they don't show up completely empty in the docs.

Another issue I opened would help a little bit here, by circumventing this problem in the case I encounter most often (Mathlib itself).

[Eric Wieser]

Is it sufficient to make the file doc always expand the folder in the sidebar?

[Eric Wieser]

That way if you misclick you still get the expanded thing

[Henrik Böving]

I was planning to implement Heather's solution once std4 and mathlib4 are compatible again but we can also do that if the majority thinks it would be better.

[Heather Macbeth]

I think Eric's solution would be fine, but in that case we should have a convention of writing documentation in import-only files, so that users don't get confused by the blank pages that turn up in these cases.

I also still think that it would be fine to drop any import-only file from the documentation, even though technically this results in a loss of information (its imports and what it's imported by). Compare linarith in mathlib3: as far as I can tell there's no docs page for
https://github.com/leanprover-community/mathlib/blob/master/src/tactic/linarith/default.lean
and so it's not documented anywhere what you get when you import tactic.linarith.

[Eric Wieser]

I was working on a lean 3 patch to fix the missing default files in doc-gen; right now we cant detect files from within lean that dont have either docstrings or declarations.