Zulip Chat Archive

Stream: general

Topic: file headers

Patrick Massot (Oct 13 2019 at 08:46):

Does anyone has statistics on the documentation effort? I tried to quickly generate some, but it reports that, out of 562 files in mathlib (excluding all.lean files) only 466 have a toplevel docstring. Is that true?

Rob Lewis (Oct 13 2019 at 09:04):

Toplevel docstring meaning the /-! -/ module doc? I'd believe that. In fact, 466/562 sounds high.

Patrick Massot (Oct 13 2019 at 09:13):

I typed too quickly. 466 is the number of missing docstrings.

Patrick Massot (Oct 13 2019 at 09:14):

And yes I mean module docstrings

Rob Lewis (Oct 13 2019 at 09:42):

Okay, yeah, that sounds about right. The number was close to 0 before the new doc requirements went in, ~3 months ago? And there hasn't been a broad effort to go back and add them everywhere.

Patrick Massot (Oct 13 2019 at 09:57):

I wonder if we could somehow coordinate a huge doc sprint to fix this before the mathlib paper is released.

Last updated: Dec 20 2023 at 11:08 UTC