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: May 08 2021 at 04:14 UTC