docs archive

Stream: general

[Yaël Dillies]

Is the stuff under archive available anywhere in the docs?

[Eric Wieser]

I don't think so, but it would be great if it could be made to be

[Eric Wieser]

In principle it wouldn't be too hard to have it appear as a separate project in the sidebar like the docs I build for lean-ga

[Eric Wieser]

All it would need is a separate leanproject.toml generated by CI, probably

[Alex J. Best]

+1 for this, I just made https://github.com/leanprover-community/doc-gen/issues/147 to track this idea, feel free to improve what I wrote there and add details

[Eric Wieser]

Done, see https://leanprover-community.github.io/mathlib_docs_demo/imo/imo2001_q6.html (in an hours time it will be under the correct sidebar heading).

PR is https://github.com/leanprover-community/doc-gen/pull/176

[Eric Wieser]

This is going to pollute the search results a bit if we're not careful though

[Floris van Doorn]

Oh, this is really nice! (after it gets its own header in the sidebar)
Yeah, pollution of search results might be an issue; archive often uses short names. Maybe we can let the docs think that all declarations in the archive are actually in the archive namespace (i.e. it will pretend that imo1959_q1 is archive.imo1959_q1). Then it will at least be easy to see that you're looking at an archive result in the search page.

[Eric Wieser]

Sidebar is fixed

[Eric Wieser]

A bigger problem is things like lower_bound, which really ought to be namespaced

[Eric Wieser]

Going through all the archive files and adding appropriate namespaces would help a lot

[Eric Wieser]

Such as how https://leanprover-community.github.io/mathlib_docs_demo/imo/imo1960_q1.html has everything under the imo1960_q1 namespace

[Eric Wieser]

How about this solution:

image.png

[Reid Barton]

Over on the right it's not very obvious, considering where the user will be looking

[Reid Barton]

Maybe it can show something like :scroll: lower_bound

[Eric Wieser]

Note that this also displays core or mathlib-counterexamples or lean-ga (if run in downstream projects)

[Eric Wieser]

Another reasonable option would be to group the results by project

[Eric Wieser]

Another version:

image.png

[Eric Wieser]

And another:

image.png

[Floris van Doorn]

It would be nice if something like this is also shown on find 404 pages like docs#lowerbound (which is the search I use most commonly).

[Floris van Doorn]

But these look really good. I like the second option.

[Eric Wieser]

I'm out of time for a few days anyway; maybe I'll wait for people to :+1: / :-1: the messages / images above

[Eric Wieser]

Majority vote seems to be for the first option with the project names on the right

[Eric Wieser]

I added the project names on the find page too, https://leanprover-community.github.io/mathlib_docs_demo/find/lowerbound

[Eric Wieser]

:ping_pong: on doc-gen#176

[Eric Wieser]

:ping_pong:

[Eric Wieser]

An unexpected side-effect: because docs#e exists, lots of code snippets of the form 0 < e now randomly link to it

[Gabriel Ebner]

Also docs#ε, and docs#f, and docs#g. :scream:

[Eric Wieser]

Presumably, in the long term the fix is to cleanup the archive to put things in namespaces? Or is that not a desirable place to end up either?

[Johan Commelin]

I think that makes sense

[Patrick Massot]

Yes, in this new context everything in that file should be in a namespace.

[Eric Wieser]

Are things bad enough that we need to restrict the linkifier to ignore archive/counterexamples (or more extremely, revert the change) in the meantime?