Zulip Chat Archive
Stream: triage
Topic: issue #1260: documenting mathlib
Random Issue Bot (Jan 13 2021 at 14:45):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 01 2021 at 14:20):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 20 2021 at 14:18):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 06 2021 at 14:19):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 24 2022 at 14:13):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 06 2022 at 14:13):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 24 2022 at 14:20):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (May 18 2022 at 14:24):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (May 18 2022 at 14:50):
Other than tactics/meta stuff, there seem to be only 32 files without module docstrings:
src/category_theory/limits/cones.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/creates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/types.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/monad/adjunction.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/monad/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/control/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/control/monad/cont.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/control/monad/writer.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/control/traversable/derive.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/analysis/filter.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/analysis/topology.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/bitvec/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/buffer/basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/qpf/multivariate/basic.lean : line 73 : ERR_LIN : Line has more than 100 characters
src/data/qpf/univariate/basic.lean : line 35 : ERR_LIN : Line has more than 100 characters
src/data/rbmap/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/rbmap/default.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/default_lt.lean : line 6 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/find.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/init.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/insert.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/main.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/min_max.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/seq/computation.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
and a lot of those files are not files which "mathematician end users" look at. If the community could make module docstrings for just the following files:
src/category_theory/limits/cones.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/creates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/types.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/monad/adjunction.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/monad/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/analysis/filter.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/analysis/topology.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
then I would regard this as a major success.
Kevin Buzzard (May 18 2022 at 14:51):
In fact I'll do the two deprecated ones now, these are easy, and no time like the present!
Patrick Massot (May 18 2022 at 14:52):
You can put src/data/analysis/filter.lean and src/data/analysis/topology.lean in the category "not for mathematicians end users'
Kevin Buzzard (May 18 2022 at 14:52):
Oh OK! I was just going by the names, I didn't look at the files.
Kevin Buzzard (May 18 2022 at 15:19):
#14224 . If someone does those category theory files then the maths docstrings are essentially done, and the CS guys can just read the code to figure out what those other files do :-)
Scott Morrison (May 19 2022 at 00:43):
Random Issue Bot (Jun 25 2023 at 14:07):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help-wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 08 2023 at 14:07):
Today I chose issue 1260 for discussion!
documenting mathlib
Created by @Rob Lewis (@robertylewis) on 2019-07-24
Labels: help-wanted, long term, needs-documentation
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC