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