documentation

Stream: general

[Kevin Buzzard]

We're in VU talking about documentation. Here's a gist containing a preliminary documentation attempt for group_theory/quotient_group.

https://gist.github.com/kbuzzard/0b5a31f5a362cb32d787bc5059ed4b9d

[Johan Commelin]

I think the summaries at the top are useful. On the other hand, I feel like many of the docstrings don't add too much value. Their content can usually be inferred from the name of the declaration, can't it?

[matt rice]

@Kevin Buzzard mostly formatting nitpicks, in the summary at the top there is some expressions not wrapped in e.g. φ : G → H, where in the docstrings below the same expression wrapped in φ : G → H. The main thing of note is that in the first case G and H are going to possibly end up using different fonts for G and H.

The only other thought deals with the References section in the summary, I don't believe i have implemented it yet, but in lumpy it shouldn't be too difficult to enable the footnotes extension, I'd probably do so by changing the comment_format field to comment_format = "cmark+footnotes" or comment_format=["cmark", "footnotes"]. It is a simple addition to implement. The main issue being deciding on whether we should accept the format, and diverse tooling issues e.g. would vscode tooltip's handle it gracefully?

[Alex Kontorovich]

I would like to make a pitch for more and better documentation. As we begin a new semester and have brand new people joining our Lean group, I'm reminded of just how difficult it still is (in my humble opinion) to get started. Yes, zulip exists and is great, but people are shy and don't really know where to go to get started or how to phrase their questions correctly, etc etc. Even once you have a bit of experience with Lean/mathlib, if you start interacting with a new library, it can be again rather difficult to figure out the "right" way to do things without having someone explicitly guide you through it. Perhaps this is just my experience; I'm too lazy to read lots and lots of instructions, and with something like this, I just want to watch like 5 mins of a video of someone actually coding up a proof of something in real time, to see how they do it, what they try that fails, when they look at docs vs exact? vs some other tactic, etc. That way, I can jump right in and start trying to get the hang of it myself.

This rant is the result of finally getting around to watching Oliver Nash's great lecture at the ICERM meeting about how the manifolds library works, what decisions were made along the way and why, what the key ideas are, etc etc. I think we should have lots more of that, perhaps as youtube videos, or blog posts (or a journal, ahem); something where, without asking on here, someone can go and find out not just what's there and the names of theorems, but how people actually write the code, what they're thinking as they do it, what issues they overcome, etc. Again, perhaps this all exists already and I'm just ignorant? Would be happy to hear some thoughts...

[Martin Dvořák]

I definitely like the idea of creating video tutorials. That said, the lack of a good documentation is a symptom of having recently moved to a new Lean version. Things change very fast these days.

[Patrick Massot]

I totally understand where this is coming from, but the problem with videos is there is no way to update them. We very often see people on Zulip completely confused by an ancient video, where ancient typically means more than one month old.

[Patrick Massot]

Latest instance here.

[Riccardo Brasca]

We definitely need to update all the documentation (for example we are missing the mathlib4 version of this I think).

[Alex Kontorovich]

Patrick Massot said:

I totally understand where this is coming from, but the problem with videos is there is no way to update them. We very often see people on Zulip completely confused by an ancient video, where ancient typically means more than one month old.

Yes that's a good point. I suppose one way to update old videos is to get into the habit of regularly making new ones? Then older ones can point in their "description"s to the newer ones. This would create a chain, the end of which could be the most recent version...? And maybe there can be a website that documents where to jump to the "latest" video (but also have backwards pointers to the historical ones, in case one is interested in how a topic got developed to the state it has)?... I'm just thinking out loud...

[Kevin Buzzard]

my impression is that you need more than that: you actually have to go around deleting old versions, because people just find links on reddit or whatever

[Ioannis Konstantoulas]

Riccardo Brasca said:

We definitely need to update all the documentation (for example we are missing the mathlib4 version of this I think).

Haruhisa Enomoto compiled this:
https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md

[Alex Kontorovich]

On this topic, we kept having new people come to the Rutgers Lean seminar and needing to start them from scratch. So in an attempt to save us all some time, I recorded a mini "speed run" of some parts of the Natural Numbers Game. In case it may be of use to others, it's available here: https://youtu.be/5GkisJ0OImg
(Comments/criticisms/suggestions welcome!... I'm sure I'm doing many things suboptimally...)

[Martin Dvořák]

I'd call it "let's play" rather than "speed run".

That said, I haven't watched your video yet.

[Alex Kontorovich]

Ok so obviously I don't know this gamer terminology... (I thought I was rushing through it quickly while trying to explain to people what I was doing...) [Meme removed, as requested...]

[Bolton Bailey]

Discussing natural number game speedruns: Yet another great application for a Lean Discord.

[Kevin Buzzard]

I'll let you know when the new version drops and you can have a competition :-)