Documentation

Stream: general

[Damiano Testa]

Dear All,

for the purpose of lecturing about Lean, I have prepared commented Lean code, explaining some of the concepts that appear in Mathlib. I wonder if this could be useful to document the code, especially for mathematicians learning Lean.

Would it be useful if I PRed some of the comments as doc-modules?

A quick estimate shows that over 2700 files contain exactly one doc-module string, which, thanks to the linter, is almost certainly the one at the beginning.

What I am thinking about is adding doc-modules (the ones introduced by /-!), not doc-strings, surrounding the few definitions and lemmas that I covered in my lectures.

For those who are curious, this is the repository of the module.

Any type of comment is very welcome!

[Damiano Testa]

For reference, here is a breakdown of number of doc-module per files in Mathlib.

Number of files	Number of module docs
2768	1
322	2
195	3
100	4
67	5
38	6
39	7
26	8
13	9
12	10
10	11
7	12
6	13
5	14
4	15
3	16
1	17
3	18
4	19
3	21
1	24
1	28
1	29
1	53
1	63

[Ruben Van de Velde]

Curious what the 63 is

[Ruben Van de Velde]

I'm guessing pretty much any documentation is going to be welcome

[Damiano Testa]

I think it was a mathport file, let me dig it up!

[Damiano Testa]

The files with 20 or more doc-modules:

     21 Mathlib/Analysis/Asymptotics/Asymptotics.lean
     21 Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
     21 Mathlib/Geometry/Manifold/ContMDiff.lean
     24 Mathlib/Data/Multiset/Basic.lean
     28 Mathlib/Data/Finset/Basic.lean
     29 Mathlib/Data/Set/Basic.lean
     53 Mathlib/Data/List/Basic.lean
     63 Mathlib/Init/Align.lean

[Ruben Van de Velde]

Maybe that's mostly a sign of files that should be split up, actually :sweat_smile:

[Kevin Buzzard]

I'm all for more module docstrings in mathlib files!

[Damiano Testa]

Ok, I'll make a selection of the comments that look more helpful and will slowly PR them.

[Patrick Massot]

@Damiano Testa it looks like your course does not appear on our courses list. Do you mind PRing a description to https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/data/courses.yaml?

[Damiano Testa]

Patrick, thanks for the link: I had briefly looked into this, but had difficulty finding the actual file to edit.

#406

[Won Seong]

How are the lean4 documentation generated? Are they all community work? The documentation should be made as soon as possible so that people don't get lost with al the library codes.

[Henrik Böving]

Won Seong said:

How are the lean4 documentation generated? Are they all community work?

The Lean 4 documentation is entirely community work (sometimes people from the community get paid by companies for individual things though).

The documentation should be made as soon as possible so that people don't get lost with al the library codes.

Well...yes that's a general truth about documentation, what's your point?

[Mauricio Collares]

Won Seong said:

How are the lean4 documentation generated? Are they all community work? The documentation should be made as soon as possible so that people don't get lost with al the library codes.

Just in case you haven't stumbled upon it yet, the available documentation is at #docs

[Mauricio Collares]

There are also a few books listed at https://leanprover-community.github.io/learn.html

[Won Seong]

Henrik Böving 말함:

The Lean 4 documentation is entirely community work

I got it. Then are people studying the lean4 implementation to renew the documentation? If that's true, I feel it's just best for me to go through some implementation rather than waiting for the complete documentation, because it would not be done very soon.

[Moti Ben-Ari]

I would like to modify the documentation at
https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/templates/learn.md.
I cloned the repo, made the change and committed locally and now I want to create a PR.
When I click New pull request, I get a webpage Compare changes and don't know what to do.

[Yaël Dillies]

You should not open PRs from forks. @maintainers, can motib get mathlib access?

[Riccardo Brasca]

Except for mathlib itself, PRs from forks are totally fine (since one doesn't need CI). @Moti Ben-Ari don't you see a "create pull request button" or something like that?

[Yaël Dillies]

Whoops sorry, brain was clearly busy on something else

[Moti Ben-Ari]

From the word "fork" it just occurred to me that I need to fork a branch, which I have done and successfully created a PR.

Please take into account that I grew up writing programs for mainframes on punched cards, so I don't have much experience with these newfangled tools :upside_down: . If anyone wants to know how to "insert character" into a punched card, I'm an expert!

[Riccardo Brasca]

No problem!

[Eric Wieser]

(the result is at https://github.com/leanprover-community/leanprover-community.github.io/pull/439/files)

[Filippo A. E. Nuccio]

I have added a line suggesting to create a fork in this PR.

[Patrick Massot]

In many cases making a fork is not necessary. Markdown files can easily be edited on GitHub. Technically this will create a fork but you don't need to do it in advance.

[Filippo A. E. Nuccio]

Well, but I think that for the sake of someone willing to change "something" (perhaps not just a md file) reading "just create a PR against lean4" would make them believe that, as for mathlib the usual procedure is to ask for pull rights. Since creating a fork does not cause any harm, I find the instruction more useful. But of course, this is up to you and the maintainers team.

[Moti Ben-Ari]

Eric Wieser said:

(the result is at https://github.com/leanprover-community/leanprover-community.github.io/pull/439/files)

@Eric Wieser Am I supposed to review my own PR?? Or just wait for someone to approve it?

[Eric Wieser]

The latter; that comment was for everyone except you, since I know you already know where the PR is!

[Patrick Massot]

It will probably take some time since someone needs to find time to read your text.

[Moti Ben-Ari]

Patrick Massot said:

It will probably take some time since someone needs to find time to read your text.

No problem!