This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
documenting mathlib #1260
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: