-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
documenting mathlib #1260
Labels
help-wanted
The author needs attention to resolve issues
long term
needs-documentation
This PR is missing required documentation
Comments
I addressed some of these in #1264. |
I should probably take care of
|
Merged
7 tasks
7 tasks
cipher1024
added a commit
that referenced
this issue
Aug 23, 2019
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this issue
May 15, 2020
…community#1260 (leanprover-community#1286) * docs(category/monad,bitraversable): add module docstrings * more docs * still more doc * doc about traversable
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
help-wanted
The author needs attention to resolve issues
long term
needs-documentation
This PR is missing required documentation
We have instituted new documentation requirements for mathlib additions: #1229
It is a long term effort to bring the existing mathlib code base up to these standards. New pull requests will be responsible for updating parts of the library that they touch, within reason. But we strongly encourage everyone to add documentation for parts of the library they have created or are familiar with.
The following files have no headers at all:
category_theory/sparse.lean
category_theory/elements.lean
category_theory/instances/rel.lean
algebra/Mon/colimits.lean
category/monad/basic.lean
category/bitraversable/lemmas.lean
category/bitraversable/instances.lean
data/stream/basic.lean
tactic/elide.lean
topology/algebra/open_subgroup.lean
But at the moment, nearly all of mathlib needs updating. So pick a random file and there's likely work to be done.
A useful tool: the
#doc_blame
#lint only doc_blame
user command prints all definitions above it in the current file that are missing doc strings.doc_blame!
includes theorems and lemmas.Update, April 4, 2020
#lint
shows missing documentation now, instead of#doc_blame
. All linter failures in the library can be seen here: https://github.com/leanprover-community/mathlib/blob/master/scripts/nolints.txtUpdate, Dec 6, 2021
We've made good progress. Here is a list of style exceptions, including files that are missing module docs. Every file has at least a copyright header.
The text was updated successfully, but these errors were encountered: