mathlib map

Stream: general

[Patrick Massot]

Is there anyone familiar with https://github.com/leanprover-community/doc-gen/ and CI that would like to make sure every matlib docs build generates a publicly available file giving the url (relative to https://leanprover-community.github.io/mathlib_docs/) corresponding to each declaration fully qualified name? That would be very helpful, in particular for the sphere eversion project. Any file format would do, this is really a list of pairs. One pair per line separated by a space would be enough.

[Bryan Gin-ge Chen]

That sounds pretty doable. If no one beats me to it, I'll try to do it this weekend.

[Patrick Massot]

Amazing, thanks.

[Bryan Gin-ge Chen]

I think the scripts may already be generating such a JSON file, but it's not published to the website.

[Patrick Massot]

Yes the lean file generates some json.

[Patrick Massot]

https://github.com/leanprover-community/doc-gen/blob/master/print_docs.py#L701

[Patrick Massot]

which probably consumes the output of https://github.com/leanprover-community/doc-gen/blob/master/gen_docs#L40

[Bryan Gin-ge Chen]

On a second look, that JSON still needs to be processed. It contains the Lean filenames, but not the final HTML filenames + anchor links.

[Rob Lewis]

This is easy enough to do. The catch is: it should also include the type of the declaration. This is slightly trickier just because of how auxiliary things are handled in the docs right now. If you have a top level declaration, the arguments are stored in a list, with names and binder types. This is so we can print them left of the colon. For structure fields, inductive constructors, etc, we don't print them as top level decls but as part of the corresponding main decl. Their type info isn't stored with the same level of granularity, I think it's just a string. So either this needs to be refactored or we have a non-uniform export.

[Rob Lewis]

This can get done soon enough. The type export is needed for the Freek 100 page. But that part of it is a little more than trivial.

[Rob Lewis]

In the meantime, if you're in a hurry, the location info you need can be scraped from the raw html at https://leanprover-community.github.io/mathlib_docs/find/manifold . The redirect link gives you the url you want.

[Rob Lewis]

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

[Rob Lewis]

I guess I missed the conversation this week, but I really hate the blue links in the docs :(

[Patrick Massot]

Thanks Rob! I think the blue links was a compromise to make you happy. My opinion is there should be no decoration at all.

[Reid Barton]

The blue is not meant to be permanent, just better than the underlines from before. Please feel free to submit a PR!

[Rob Lewis]

What about making it a slightly lighter grey than the surrounding non-linked text?

[Rob Lewis]

It's a hint that the links are different, without being intrusive

[Reid Barton]

Sounds good to me. Note that the arguments of a theorem that come before the colon are already a slightly lighter color than the rest--so slight that I didn't notice it until I started looking at how to change the underlines.

[Jalex Stark]

(deleted)

[Johan Commelin]

Did your cat jump on your keyboard?

[Jalex Stark]

my laptop fell on my keyboard... sorry

[Johan Commelin]

I hope your laptop and your keyboard are ok...

[Jalex Stark]

they are!

[Rob Lewis]

image.png ? The links get a little lighter (and underlined) when you mouse over.

[Reid Barton]

Now in nat.cases_succ you can't see (at least I can't) that the \Ns are links but the rest is not.

[Reid Barton]

I think getting rid of the separate color for arguments before the colon would be fine.

[Johan Commelin]

How about we underline everything that is not a link? [/jk]

[Rob Lewis]

Oh, I see what you mean there.

[Rob Lewis]

image.png ?

[Johan Commelin]

Should all the arguments be bold?

[Johan Commelin]

Or only lemma/theorem/def the_name

[Rob Lewis]

image.png ?

[Johan Commelin]

I think I like that.

[Mario Carneiro]

These colors are too subtle for me to see clearly, and I don't think my eyesight is below average

[Mario Carneiro]

what was wrong with the blue?

[Mario Carneiro]

some more saturation would be good to distinguish it from the various shades of grey in the text itself (especially with things like blackboard bold which have their own effective color)

[Mario Carneiro]

oh wait, is it literally gray? No wonder it looks desaturated

[Rob Lewis]

The blue was really glaring, since a lot of decls were almost completely blue. I think it's much easier on the eyes with a more subtle color for the links. Yes, it's literally gray, hopefully just enough to slightly distinguish it from the surrounding black. If you mouse over it changes more.

[Rob Lewis]

It's live now btw.

[Patrick Massot]

The docs export is nice, but it would even nicer if there could be a version containing only what I asked for. Here I'm downloading a 37Mo file and then do

with open('test', 'w') as test:
     for k, v in json.items():
         test.write(f"{k} {v['docs_link'][52:]}\n")

to get down to a 3.5Mo that zip then compresses to 705Ko.

[Rob Lewis]

I mean, I can zip it if the size is a problem, but it seems unnecessary to generate a bunch of custom maps when they're all subsets of this big one.

[Patrick Massot]

The download size is the issue.

[Patrick Massot]

What does it cost to generate the basic info? You're not even keeping old versions, right?

[Rob Lewis]

Just future proofing mostly. What if you decide in the future that you want links to GH source too? It's less effort to strip info from the big database now than to add it to the small one later.

[Patrick Massot]

Links to the GH source can also be reconstructed from what I extract above.

[Rob Lewis]

Can they? You need line numbers and Lean and mathlib versions (to make sure you direct to the right commits), no?

[Rob Lewis]

And this is running in CI, right? Does the extra 10 second download matter?

[Patrick Massot]

Indeed we don't get line number, only the file.

[Patrick Massot]

Right now there is no CI, but I should work on this.

[Rob Lewis]

It's now uploading export_db.json.gz which is ~4mb.