https://leanprover-community.github.io/mathlib_docs/

Stream: general

[Riccardo Brasca]

Is https://leanprover-community.github.io/mathlib_docs/ working for you? I tried on Firefox and Chrome but the pages are displayed like this
image.png
The links seem also to be broken... they give something like https://%244.github.io/$5/algebra/algebra/basic.html :thinking:

[Rémy Degenne]

Same issue for me.

[Damiano Testa]

I also see it like this.

[Eric Wieser]

There's a lot of changes in flight at the moment, https://github.com/leanprover-community/doc-gen/commits/master

[Adam Topaz]

Same issue here -- looks like the CSS files are not being downloaded

[Adam Topaz]

From the html source of https://leanprover-community.github.io/mathlib_docs/:

    <link rel="stylesheet" href="https://$4.github.io/$5/style.css">
    <link rel="stylesheet" href="https://$4.github.io/$5/pygments.css">
    <link rel="shortcut icon" href="https://$4.github.io/$5/favicon.ico">

[Adam Topaz]

That doesn't look right, does it?

[Gabriel Ebner]

https://github.com/leanprover-community/doc-gen/pull/114

[Gabriel Ebner]

Context: Rob has been adding an amazing new CI feature to the doc-gen repo today. You* can now comment #deploy on a doc-gen PR and it will automatically deploy the docs generated by the PR to https://leanprover-community.github.io/mathlib_docs_demo so you can try them out.
(* for very limited values of you. For security reasons, we've limited access to admins.)

[Rob Lewis]

@Gabriel Ebner I think the problem in the demo repo is a main/master confusion?

[Gabriel Ebner]

I believe so... I think I've switched everything to master now, like we have on the other repos.

[Rob Lewis]

Have a look at https://leanprover-community.github.io/mathlib_docs_demo/ and see if you find any suspicious formatting, especially having to do with latex and especially if it's different from the main doc pages

[Bryan Gin-ge Chen]

There are a few fixes I've made which haven't been committed yet, so later tonight might be better.

[Bryan Gin-ge Chen]

I'm planning to change the LaTeX / markdown setup so that it's more consistent with how it works on math.stackexchange.com / mathoverflow.net. See this comment.

Any objections?

[Bryan Gin-ge Chen]

I've finished my changes, please check the demo now: https://leanprover-community.github.io/mathlib_docs_demo/

See the secret LaTeX test page (source) for a bunch of LaTeX + markdown examples which now work.

Note that some of the LaTeX we currently have in the docs will break, since some of the workarounds we had to use before are no longer necessary.

Here's the corresponding PR: doc-gen#110

[Rob Lewis]

I've been spot checking and don't see much breakage at all!

[Rob Lewis]

Here's one: https://leanprover-community.github.io/mathlib_docs_demo/analysis/analytic/basic.html#changing-origin-in-a-power-series

[Rob Lewis]

I guess it's the \\sum

[Rob Lewis]

git grep '\\\\' turns up a few more

[Rob Lewis]

(These are things to fix in mathlib after the doc changes are merged)

[Sebastien Gouezel]

Yes, I had changed the \sum to \\sum because of the \-eating bug in https://github.com/leanprover-community/doc-gen/issues/62. It's great if it is fixed!

[Eric Wieser]

Bryan Gin-ge Chen said:

I'm planning to change the LaTeX / markdown setup so that it's more consistent with how it works on math.stackexchange.com / mathoverflow.net. See this comment.

Any objections?

I'm a little worried that mistletoe has become abandonware, but I guess if the actively developed markdown2 is broken, mistletoe is still the better choice.

[Bryan Gin-ge Chen]

doc-gen#117 is a PR that creates a "references" page so that the citations in mathlib doc strings are now finally links:

Please check out the demo here and let me know if there are any obvious bugs:

http://leanprover-community.github.io/mathlib_docs_demo/references.html

Like I say in the PR, I didn't do much with the styling; I more or less just copied the code that generates the "papers about Lean" page from the community website, so I'm open to any suggestions.

[Eric Wieser]

The back references are great!

[Eric Wieser]

Can we get those for library notes too?

[Bryan Gin-ge Chen]

Ooh, good idea! Yes, I think that should be doable.

[Ruben Van de Velde]

There's some css that makes the links move to the next line, like here: https://leanprover-community.github.io/mathlib_docs_demo/topology/sheaves/sheaf_condition/opens_le_cover.html#references

[Ruben Van de Velde]

(And "Paul Halmos, Measure theory. 1950." is there twice, though that's not doc-gen's fault)

[Bryan Gin-ge Chen]

Ruben Van de Velde said:

There's some css that makes the links move to the next line, like here: https://leanprover-community.github.io/mathlib_docs_demo/topology/sheaves/sheaf_condition/opens_le_cover.html#references

Yeah, that's coming from a hack we were already using to make sure the link doesn't end up underneath the header when you click on the backreferences (see this part of the diff).

Hmm, but it seems the link is still hidden by the header if I navigate to https://leanprover-community.github.io/mathlib_docs_demo/topology/sheaves/sheaf_condition/opens_le_cover.html#backref1 :sad:

edit: Hmm... the header only seems to cover up the link in Firefox? I tested Safari and Chrome and the backref1 link was OK.

[Kevin Buzzard]

I've had problems with headers in Firefox from day one. Whenever I click on a link in Zulip i have to scroll down a bit

[Bryan Gin-ge Chen]

A few more updates: the extra line breaks and covered up link targets should be fixed now, at least in Firefox and Chrome. There will still be extra line breaks in Safari, until they release an update where this bug is fixed.

I also added backrefs to the Library Notes page: https://leanprover-community.github.io/mathlib_docs_demo/notes.html

And turned raw URLs into links: https://leanprover-community.github.io/mathlib_docs_demo/linear_algebra/quadratic_form.html

[Heather Macbeth]

This is really nice. One suggestion, only if you are looking for more projects ... the reference tags at
https://leanprover-community.github.io/mathlib_docs_demo/references.html
currently seem to follow the convention of the person who added them, producing both slight variations in the obvious style ([ahrens2017], [Vaisala_2003], [ghys87:groupes], [EinsiedlerWard2017], [MM92]) and some of radically different style ([MR1237403], [Elephant]). We could just leave out these tags? Or we could fix a convention and have it auto-generated (I'm partial to alpha).

[Bryan Gin-ge Chen]

It's easy to hide the tags if they're too distracting. It seemed natural to me to leave them in so that we could put something in the space on the right.

Autogenerating nice tags might be possible too, I'm not sure.

[Eric Wieser]

Showing the file name (eg mathlib : data.list.basic) in the hover text of backrefs would be a nice touch, assuming you haven't already done so

[Bryan Gin-ge Chen]

Yes, adding titles with the filenames should be doable. I think I found pybtex's functions to format the bibtex keys with the alpha style here too.

Keep the ideas coming!

[Damiano Testa]

I really like this: thanks Bryan!

One thing that I used often and saw "referenced" is the Stacks project:

https://stacks.math.columbia.edu/

I think that it inspired many proofs, especially in the commutative algebra/algebraic geometry side of mathlib. Is there a way of making it appear in the references?

[Damiano Testa]

With an easy grep, it seems to be referenced 101 times at least in mathlib.

[Bryan Gin-ge Chen]

If the Stacks project is being cited in a consistent and easy-to-parse way then it should be no problem.

[Bryan Gin-ge Chen]

Aha, it looks like most of the Stacks project citations are just raw URLs. I can definitely work with that. Though maybe the "commutative algebra / algebraic geometry team" should first decide whether that will be the convention going forward (and then add it to our style guide).

[Damiano Testa]

Ok, the Stacks project is an entirely online resource, so I think that it will be pretty easy to agree that it is always cited via URLs! What should be decided? To always include a citation to the "front page"?

Maybe, every time the stacks project is cited, there should be the URL https://stacks.math.columbia.edu/ and then the specific page/tag that is more appropriate.

Would this work for you?

Would this work for the people who cite the stacks project?

[Johan Commelin]

Some time ago @Scott Morrison suggested to make this a bit more structural. This might be a good time to push in that direction again. The idea was that we could have a new attribute

@[stacks "01X6"]
lemma foobar yadda : yadda :=

[Johan Commelin]

Of course there will also be references to Stacks that aren't directly linking a mathlib result to a Stacks tag, but maybe we can agree that either

• those will all be full URLs to a tag, or
• those will all be of the form [Stacks, 01X6]

[Johan Commelin]

The benefit of the attribute is that it will be easy to generate a json file that creates a partial dictionary between mathlib and Stacks

[Johan Commelin]

The people from Stacks (Johan de Jong, Pieter Belmans) have expressed interest in linking back to mathlib, as soon as we have a sizable dictionary (I think ~200 results)

[Bryan Gin-ge Chen]

Yep, basically any convention that is easy to detect via regex would be easy for me; that's basically how the references and notes links work now.

Scott's idea of using attributes could work too; but it would require someone with metaprogramming ability to help...

Once we have the data, it won't be difficult to add the tags to a special section of the references page, or even a separate Stacks project page, depending on what we want.

[Bryan Gin-ge Chen]

I could certainly have doc-gen export a stacks.json file from data collected via the regex approach, if we wanted that.

[Damiano Testa]

I personally am happy to go with either approach. I like the attribute, but I also think that sometimes there will be sections that are inspired by the stacks project, even if then the implementation will not actually prove a specific result from it. Would it be reasonable/desired to have a generic reference and then specific attribute tags?

[Johan Commelin]

Yeah, we'll need a mix.

[Scott Morrison]

I think Rob actually did a stacks export script for us a while back when we first considered this.

[Scott Morrison]

Perhaps there is a stacks branch?

[Johan Commelin]

not on my copy :sad:

[Scott Morrison]

branch#stacks has scripts/stacks_tags.lean

[Scott Morrison]

https://github.com/leanprover-community/mathlib/blob/stacks/scripts/stacks_tags.lean

[Mario Carneiro]

There is a broken link at https://leanprover-community.github.io/mathlib_docs_demo/notes.html#classical%20lemma

[Kevin Buzzard]

I don't know if it's related, but at https://leanprover-community.github.io/archive/stream/116395-maths/index.html there is a broken link to the ∀ᶠ (x : α) in F, P x and ∃ᶠ thread (which was a shame yesterday because Jordan Ellenberg (of Ellenberg-Gijswijt) was asking about it on Twitter two days ago and I couldn't figure out how to link to the conversation).

[Rob Lewis]

I remember talking about official Stacks integration a while back. The @[stacks] attribute is easy enough and creating a json dump that the Stacks site can use is also pretty simple. What I was and still am worried about is that it could become a one-off thing that gets implemented and forgotten and never maintained.

[Rob Lewis]

Putting a bunch of effort into a misaligned and incomplete crossref with Stacks is worse than no crossref at all. It needs to be someone's baby and they need to put time into making sure new things get tagged and old tags stay correct.

[Rob Lewis]

(More on topic, @Bryan Gin-ge Chen your changes look fantastic!)

[Kevin Buzzard]

Yes, this is difficult. Tags never change on the stacks project by the way. The stacks people have been keen to align with us but somehow nobody seems to know the way forward.

[Johan Commelin]

I think the chance that old tags rot is very small. So the main issue is that new things should get tagged. This will have to be a community effort. But I think it's ok if we do it in bursts.

[Johan Commelin]

We could have occassional Stack sprints, where we add 30 new @[stacks] or so.

[Johan Commelin]

And possibly, we could have a bot that greps for Stacks urls in the diff of a PR. If it finds a URL, it can post a comment to the PR asking whether the URL should really be a @[stacks] tag.

[Heather Macbeth]

I think the undergrad page has been pretty well-maintained -- new things have been added as they appear.
https://leanprover-community.github.io/undergrad.html
It helps that there is a "missing" list, so people get a feeling of accomplishment from ticking things off -- would it be possible to compile a "missing" list for the "top" (traffic?) 200 (?) Stacks tags?

[Scott Morrison]

Not really. There are a lot of stacks tags

[Johan Commelin]

7175 pages
719099 lines of code
20318 tags
3151 sections
114 chapters
229 slogans

https://stacks.math.columbia.edu/

[Johan Commelin]

Of course we can select 200 tags, but if we rank them by how "impressive" the result is, then 198 of them will be quite far out of reach :sad:

[Kevin Buzzard]

It would be better to have "target" stacks tags.

[Johan Commelin]

That's what Heather means, I suppose?

[Heather Macbeth]

But
https://stacks.math.columbia.edu/statistics
there is a "most-referenced tag", https://stacks.math.columbia.edu/tag/00DV

[Heather Macbeth]

You could get them to compile the 200 most-referenced tags?

[Johan Commelin]

yup, I guess we can ask Pieter to do that. Probably he already has that lying around.

[Johan Commelin]

I'll send him an email in a moment

[Johan Commelin]

In fact, let me check their scripts/ folder first (-;

[Johan Commelin]

This script is probably relevant: https://github.com/stacks/stacks-tools/blob/master/query/count_references.py#L25

[Johan Commelin]

I love how there are still dutch variable names in these scripts, after so many years :rofl:

[Johan Commelin]

Aahrg! I don't have Python 2 installed :head_bandage:

[Heather Macbeth]

Don't risk it, Johan.

[Kevin Buzzard]

You should upgrade to Ubuntu :-/

[Kevin Buzzard]

$ python --version
Python 2.7.17

[Johan Commelin]

The 200 most referenced tags are:
[('00DV', 119), ('01ZM', 69), ('02KH', 64), ('06Z0', 61), ('03H4', 57), ('01XB', 48), ('00NX', 47), ('01UA', 46), ('00DS', 41), ('0149', 41), ('00E0', 40), ('01LC', 40), ('00MB', 39), ('00EU', 37), ('01T6', 36), ('00U2', 36), ('00XR', 36), ('03H6', 34), ('00NQ', 34), ('01W6', 34), ('01Z4', 33), ('001P', 32), ('00HN', 32), ('08J5', 31), ('00KW', 31), ('01T2', 31), ('015J', 29), ('07SK', 29), ('01WM', 29), ('01U9', 29), ('0052', 28), ('00GU', 28), ('04XB', 28), ('00HL', 28), ('00HI', 28), ('01WN', 28), ('04KF', 28), ('00ON', 27), ('02WW', 27), ('02GL', 26), ('01KU', 26), ('00HR', 26), ('071Q', 26), ('01W4', 26), ('005C', 25), ('089W', 25), ('015E', 25), ('01TH', 25), ('04XH', 25), ('00DB', 25), ('02KB', 25), ('00HT', 25), ('0658', 25), ('08EU', 24), ('015Z', 24), ('00MA', 24), ('01PB', 24), ('01XZ', 24), ('0BRA', 24), ('04XD', 24), ('01I1', 24), ('079P', 23), ('0133', 23), ('00EO', 23), ('00IN', 23), ('0BUG', 23), ('03JH', 23), ('03FX', 23), ('00FV', 23), ('00F4', 23), ('03KL', 23), ('08DQ', 23), ('0519', 22), ('02JO', 22), ('04S6', 22), ('01Z6', 22), ('02M1', 22), ('00PD', 22), ('01W3', 22), ('00RU', 22), ('00TT', 22), ('081F', 21), ('08DR', 21), ('00IV', 21), ('01R8', 21), ('04NX', 21), ('01XC', 21), ('0BK0', 21), ('0AIM', 21), ('03PU', 21), ('01Q3', 21), ('08E7', 20), ('01JA', 20), ('0152', 20), ('00KJ', 20), ('01PS', 20), ('01PG', 20), ('00S2', 20), ('000R', 20), ('031S', 20), ('03XH', 20), ('00HS', 20), ('014A', 20), ('0A9E', 20), ('045G', 20), ('0038', 20), ('02FY', 20), ('03M9', 20), ('00XS', 20), ('08EB', 19), ('03A0', 19), ('0B91', 19), ('03GI', 19), ('01JY', 19), ('00GQ', 19), ('00IP', 19), ('04WP', 19), ('00KQ', 19), ('01LA', 19), ('03QP', 19), ('064B', 19), ('05GG', 19), ('03HV', 19), ('01T4', 19), ('01ZA', 19), ('00FR', 19), ('00FN', 19), ('01ON', 19), ('00JB', 19), ('05QT', 19), ('0262', 19), ('01S4', 19), ('08D5', 19), ('07RP', 18), ('07RB', 18), ('00S1', 18), ('01TS', 18), ('02X1', 18), ('01XJ', 18), ('07QM', 18), ('01K5', 18), ('03XG', 18), ('00HQ', 18), ('014Z', 18), ('01S8', 18), ('02FX', 18), ('09YQ', 18), ('02YO', 18), ('0A6H', 18), ('0132', 17), ('02LX', 17), ('03GN', 17), ('01J7', 17), ('023T', 17), ('0754', 17), ('064U', 17), ('064R', 17), ('03BZ', 17), ('02GE', 17), ('072W', 17), ('01KT', 17), ('00HD', 17), ('00J6', 17), ('0040', 17), ('00VH', 17), ('03C4', 16), ('01FF', 16), ('0804', 16), ('0A6A', 16), ('05TC', 16), ('03CG', 16), ('07D9', 16), ('0462', 16), ('01RG', 16), ('01PV', 16), ('00QO', 16), ('01V0', 16), ('01VB', 16), ('01T8', 16), ('01TQ', 16), ('00U7', 16), ('01ZR', 16), ('09XI', 16), ('0315', 16), ('01E8', 16), ('01KP', 16), ('01KO', 16), ('09T5', 16), ('082Z', 16), ('0AI7', 16), ('00LD', 16), ('0245', 16), ('041J', 16), ('03II', 16), ('00RC', 16), ('03KG', 16), ('01YB', 16), ('04GG', 16), ('08BJ', 16), ('06LJ', 15)]

[Johan Commelin]

https://github.com/stacks/stacks-project/blob/master/tags/tags contains the latex labels of all those tags

[Johan Commelin]

The adapted script can be found at https://github.com/stacks/stacks-tools/tree/sorted-ref-count

[Heather Macbeth]

Johan Commelin said:

Of course we can select 200 tags, but if we rank them by how "impressive" the result is, then 198 of them will be quite far out of reach :sad:

So how many are out of reach? Any estimate? :)

[Rob Lewis]

I moved the stacks derail to a new topic: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/stacks.20tags

[Bryan Gin-ge Chen]

Mario Carneiro said:

There is a broken link at https://leanprover-community.github.io/mathlib_docs_demo/notes.html#classical%20lemma

#6321 fixes that and another broken Zulip archive link in data.tree.

[Bryan Gin-ge Chen]

Another update on doc-gen#117 (hopefully final, unless some bugs are discovered), which addresses the following two issues:

Eric Wieser said:

Showing the file name (eg mathlib : data.list.basic) in the hover text of backrefs would be a nice touch, assuming you haven't already done so

You can now see filenames if you hover over the backrefs on the demo notes and demo references pages.

Heather Macbeth said:

This is really nice. One suggestion, only if you are looking for more projects ... the reference tags at
https://leanprover-community.github.io/mathlib_docs_demo/references.html
currently seem to follow the convention of the person who added them, producing both slight variations in the obvious style ([ahrens2017], [Vaisala_2003], [ghys87:groupes], [EinsiedlerWard2017], [MM92]) and some of radically different style ([MR1237403], [Elephant]). We could just leave out these tags? Or we could fix a convention and have it auto-generated (I'm partial to alpha).

The references page now uses auto-generated "alpha"-style tags.

[Heather Macbeth]

Very nice! :)

[Stefan Sterea]

Hi, I have no idea where to write this, but, could anyone help me? I've installed lean binaries and set the extension path in VS Code to the lean executable. I followed the instructon to install mathlibtools via pip and now I'm stuck. When I want to create a project and write leanproject new my_project in Git Bash it gives the error [WinError 2] The system cannot find the file specified.

[Stefan Sterea]

(deleted)

[Kevin Buzzard]

Start a new thread in #new members or #general

[Scott Morrison]

@Bryan Gin-ge Chen, I've noticed that there are links to items in the bibliography in a "short format", e.g. at https://leanprover-community.github.io/mathlib_docs/category_theory/abelian/basic.html#category_theory.abelian.epi_pullback_of_epi_f, which uses Proof from [aluffi2016, IX.2.3], cf. [borceux-vol2, 1.7.6]

[Scott Morrison]

These currently don't get linkified to references.bib. Can/should they?

[Bryan Gin-ge Chen]

Ah, interesting. They certainly could. Do we want to allow this, and if so, how do we want to display it? If we're not able to come up with some standard, easily-parsable format for chapter references, it might be easier just to change all those to something like Proof from [Aluffi 2016 IX.2.3][aluffi2016], cf. [Borceux Vol 2 1.7.6][borceux-vol2].

[Scott Morrison]

I think having a single standard way to link to references.bib is preferable, and probably these should be updated.

[Scott Morrison]

I'm not entirely sure how one would grep for all of them.

[Rob Lewis]

I agree, I think we should remove the short format links completely.

[Rob Lewis]

We've already made up our own markdown syntax for the bib references, let's not get even crazier

[Eric Wieser]

What is our made-up syntax?

[Rob Lewis]

[Aluffi 2016 IX.2.3][aluffi2016]

[Eric Wieser]

That's legal in CommonMark

[Eric Wieser]

example

[Eric Wieser]

Zulip doesn't accept that example though.

[Rob Lewis]

Hmm, less made up than I thought then. I remember lots of proposals when we set this standard a while back

[Eric Wieser]

[aluffi2016][] is legal in CommonMark too, from the same page

[Eric Wieser]

I mean, who knows what mistletoe considers legal

[Bryan Gin-ge Chen]

Mistletoe has a fairly comprehensive set of CommonMark tests, but it looks like they’re pinned to CommonMark version 0.28 (CommonMark 0.29 is the current one).

[Bryan Gin-ge Chen]

This looks to be the example that Eric linked: https://github.com/miyuchina/mistletoe/blob/master/test/commonmark/commonmark.json#L4282

[Eric Wieser]

In the process of writing https://github.com/leanprover-community/doc-gen/pull/166, I found out that mistletoe is not re-entrant (and therefore not thread-safe, asyncio-safe, or I'll-just-cache-this-renderer-globally-safe).

Did we ever look at https://github.com/executablebooks/markdown-it-py?
It's developed by some people who forked mistletoe then gave up because its maintainer never responded.

[Bryan Gin-ge Chen]

Hmm, I've never looked at it. How compatible is it with mistletoe? i.e. will the hacky mathjax scripts I wrote have to be rewritten if we switch over?

[Eric Wieser]

I guess I'll try it and see at some point; just wanted to check it hadn't already been dismissed

[Eric Wieser]

One argument in favor of markdown-it-py; it's a translation of javascript's markdown-it, which is what vscode uses internally.

The math support is slightly different (it fails some of the latex tests), but I've filed a fix upstream at https://github.com/executablebooks/markdown-it-dollarmath/pull/6