Improving documentation

Stream: general

[Yaël Dillies]

So I've been reading and watching this explanation on documentation principles and I'm trying to identify where we stand in each component. So far, I've identified:

• Tutorials: We have quite a good deal of them: NNG, LFTCM, Kevin's workshops, Tactic writing in Lean...
• How-to guides: There are : The equation compiler and using_well_founded, How to use calc mode, The conversion tactic mode, my guide on how to use Zorn's lemma. Maybe we have so little because we provide the how-toes live on Zulip?
• Reference: This is the API documentation, but more precisely the definition docstrings and part of the module docstrings.
• Explanation/Discussion: Those are quite spread out: Theory docs, Library overviews, module docstrings...

I don't know where to fit Simp, The Hitchhiker's Guide to Logical Verification.

[Yaël Dillies]

What steps do we want to take to more closely follow this four-categories standard? My biggest concerns are:

• module docstrings. We should decide how the reference and explanation parts intermingle. In retrospective, all the module docstrings I wrote were roughly structured as

/-!
# Something

Explanation

## Main declarations

Reference

## Implementation

Explanation
-/

I'm happy to hear any suggestion.

• the website organization. Documentation, Library overviews and Theory docs overlap in their purpose, and in particular mix the "doing maths" and "doing Lean" parts. I think we could merge the "doing maths" part into one big Documentation folder with the four Tutorials How-to guides, Reference, Explanation subfolders, and let the "doing Lean" part live its life in another folder.

[Kevin Buzzard]

For module docstrings we have this (which you might well know about, I'm just mentioning it because you didn't link to it)

[Kevin Buzzard]

Both Jeremy and I have one eye on mathematics in Lean which I would like to have in some kind of preliminary shape by January because I am teaching an undergraduate Lean course Jan-Mar. I've spent some time recently asking undergraduates how they learn nowadays, and it really is very different to when I was learning material. In particular when learning programming languages like python, if a student is stuck on some basic thing they don't even read the materials which the lecturer has made available, they just google for their problem, and because python is such a popular language they find some stackoverflow question with 1000 upvotes. We cannot offer this service; right now, as you say, we are countering it by relying on the fact that we are a sufficiently small community (in comparison to something like python) that individual queries can be answered here, but of course the fact that we are small means that now is the time to get it right. @Rob Lewis has thought seriously about documentation.

[Alex J. Best]

I think we should start a FAQ or some other list of canonical answers to common questions we can link to. Zulip is great but I don't think its easy for newcomers to find previous questions here, so these questions get re-asked and re-answered a lot. Whereas in stackexchange-type question boards its easier for search engines to find those questions it seems and people invest effort into editing and improving old answers in addition to answering new questions, an FAQ might be a nice compromise for us.

[Yaël Dillies]

With @Julian Berman we also had to idea of a glossary for mathlib jargon like 'orange bar hell", "olean", "non-terminal simp"...

[Yaël Dillies]

(I already find it worthy of existence for the sole purpose of documenting linguistic processes in a mathematics community :innocent:)

[Julian Berman]

Oh, you found my WIP page too :D yeah I still would love to get back to that.

[Yaël Dillies]

I am more than happy to help/take over it!

[Julian Berman]

That would be awesome -- I am still drowning in making course materials oy, so judging by what I see is your speed elsewhere for docs you may finish the whole thing before I even do anything useful ha, but maybe I'll open a draft PR on the repo and we can collaborate on it that way

[Julian Berman]

I put a PR here: https://github.com/leanprover-community/leanprover-community.github.io/pull/208/files (if you have access to the leanprover-community repo you can already push commits to that, if not I sent you a separate invite so you can push to my fork). And yeah I'll try to put it back on my own TODO list :D

[Yaël Dillies]

Great! I'll work on it.

[Yaël Dillies]

And no I currently don't have access to the website repo. Can anybody invite me maybe?

[Yaël Dillies]

Or is the PR process rather through forks anyway?

[Yaël Dillies]

Can I link to another glossary entry?

[Julian Berman]

I think for non-mathlib repos either is fine (which is normal outside of lean as well, either a fork or a branch if you have write access are equally fine)

[Julian Berman]

Can I link to another glossary entry?

Yeah, on the same page it's like this: https://github.com/Julian/leanprover-community.github.io/blame/4964a9d599194131595fa7b59259a7f8abf90e54/templates/glossary.md#L11 i.e. #nameofotherentry

[Julian Berman]

and with a hyphen if there are spaces

[Bryan Gin-ge Chen]

Julian Berman said:

I think for non-mathlib repos either is fine (which is normal outside of lean as well, either a fork or a branch if you have write access are equally fine)

Yeah, that's correct. It's only mathlib where the CI setup (which provides oleans to leanproject) makes PRs from branches in the main repo more convenient than PRs from forks.

[Johan Commelin]

@Yaël Dillies Great idea. I had an open tab on that divio website for a long time, but I never got around to actually doing something with it.

[Johan Commelin]

@Julian Berman Thanks for that PR. I think this can become a useful resource.

[Yaël Dillies]

Where does the glossary belong? To the Explanation part?

[Johan Commelin]

I guess so, it doesn't fit the other 3 categories.

[Johan Commelin]

https://documentation.divio.com/_images/overview.png convinces me that it should be Explanation.

[Yaël Dillies]

Johan Commelin said:

Yaël Dillies Great idea. I had an open tab on that divio website for a long time, but I never got around to actually doing something with it.

Me too, actually! You see, that's been a month or so before I watched that video.

[Yaël Dillies]

(deleted)

[Yaël Dillies]

Btw, should we maybe update the maintainers list? Eg Chris is not an undergrad anymore.

[Justin Pearson]

Mathlib could do with more examples. For a newcomer like me, just reading the type of a theorem and the explanation is generally not enough to workout how to use a particular theory in mathlib. I'm a computer scientist so reading type signatures is how I read documentation, but say for somebody who just wants to prove theorems using linear algebra the documentation is not that helpful.

[Rob Lewis]

It's great to see some effort here! I remember talking about these thigns a bunch with @Jasmin Blanchette . I may have mangled these memories, but one thing that stuck was the "cascading level of detail" approach. Ideally everything is documented in multiple levels, say: an overview/refresher/quick reference, a fuller explanation with examples for people who haven't seen the topic before, and a detailed implementation-level description. (Or something like that, those aren't Jasmin's words, but you get the idea.)

[Rob Lewis]

We haven't done a great job at this. Some of the installation/tooling descriptions on the website are probably the best attempts

[Rob Lewis]

Another spot we can really improve is the tactic documentation, which is very non-uniform. (https://github.com/leanprover-community/mathlib/issues/3088#issuecomment-647133040)

[Rob Lewis]

Even just making sure all the tactic entries have examples of the different use cases would be huge

[Jasmin Blanchette]

Yaël Dillies said:

I don't know where to fit Simp, The Hitchhiker's Guide to Logical Verification.

The HG is strictly speaking lecture notes for a university course. But some people use it as what I would call a tutorial (i.e. they read it sequentially to learn Lean).

[Jasmin Blanchette]

Rob hasn't mangled anything. I used the confusing phrase "pyramid principle" for the idea, but I like Rob's cascade. I like to emphasize the fact that the same ideas are expressed multiple times, sometimes 4-5 times (e.g., a title, an abstract, the introduction, and the body of an article; or the first sentence of a para vs. the rest of the para).

[Kyle Miller]

Yaël Dillies said:

I don't know where to fit Simp

At some point I claimed it is mostly explanation but transitions to a reference by the end.

I think module docstrings are almost universally references. Most things that are arguably an explanation are there to help know what's going on -- they are still mainly theoretical knowledge useful while working.

For organizing documentation, I've found the Mathematica's to have nice aspects. There are reference pages for specific functions with multiple levels of detail, there are guides with a hierarchical list of pieces of documentation related to a specific topic, and there are tutorials giving step-by-step examples or explanations of how the system works. One reason I bring up Mathematica is that it shares a goal with Lean/mathlib to be accessible to mathematicians.

[Yaël Dillies]

Kyle Miller said:

At some point I claimed it is mostly explanation but transitions to a reference by the end.

Yup, I had that in mind.

[Rob Lewis]

The Mathematica documentation is something to aspire to. This is what I was thinking of when I wrote my comment about tactic docs

[Rob Lewis]

But it does come at a big time/personnel cost, the people at Wolfram spend a lot of time and energy writing, proofreading, and udpating those pages

[Scott Morrison]

If only there was "jump to source" in their documentation. :-)

[Julian Berman]

I get the closed source joke :) but it's almost the 10 year anniversary of asking for Python to do that uniformly, so small wins! https://bugs.python.org/issue13437

[Johan Commelin]

I came across https://blog.danslimmon.com/2019/07/15/do-nothing-scripting-the-key-to-gradual-automation/ on HackerNews (https://news.ycombinator.com/item?id=29083367). Looks like a useful thing for some (to be written) HOWTOs.

[Johan Commelin]

Tl;dr:

• Usual HOWTO: Write a markdown file with five steps: do this, do that, then do that, etc.
• Proposed alternative: Write a bash script that echos those steps.
• Benefit: There is a very low barrier for someone to step in and automate step 2 or 5. After a couple of months, the entire procedure might be automated.