Priority documentation tracker

Stream: PhysLean

[Joseph Tooby-Smith]

To steal a feature used here, I'm thought might be worth having a go at something similar.

Therefore here is a tracking thread for the priority documentation within PhysLean. (This is related to PhysLean#713 but that is a bit chaotic).

If you want to claim any of the :new: items within the following list (meaning you think you want to have a go at this in the reasonable future , just put a comment here, and I will edit the list with :play: accordingly. Once done they will be replaced with :check:.

Aim

Improve the documentation of the following list of files within PhysLean to match the style given in:

:check: PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
:check: PhysLean.ClassicalMechanics.HarmonicOscillator.Solution

List of files

The following list contains the files I think we should focus on, feel free to suggest others, I may also add new ones as time goes on.

1. :new: Relativity/LorentzGroup/Basic.lean
2. :new: CondensedMatter/TightBindingChain/Basic.lean
3. :new: QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
4. :new: SpaceAndTime/Space/Basic.lean
5. :new: StatisticalMechanics/CanonicalEnsemble/Basic.lean
6. :check: (JTS at PhysLean#743) Particles/StandardModel/HiggsBoson/Basic.lean

[Joseph Tooby-Smith]

Thinking aloud: I think any linters or tools which could help with the documentation would be very useful, e.g. tools which can make tables of contents, or linters which can check for documentation structure (or even spelling)

[Michael Rothgang]

Using verso in documentation can help catch some mistakes (e.g., code samples not compiling any more, or checking that links to identifiers (such as theorems) still work). I believe that's available on the latest release candidate already; I'm not sure how to use verso in doc-strings.

[Michael Rothgang]

(I would love to do the same in mathlib, certainly in the files I care about.)

[Joseph Tooby-Smith]

Michael Rothgang said:

Using verso in documentation can help catch some mistakes (e.g., code samples not compiling any more, or checking that links to identifiers (such as theorems) still work). I believe that's available on the latest release candidate already; I'm not sure how to use verso in doc-strings.

Nice! Thanks for putting this in writing, this is definitely something worth exploring as it would massively help maintain the consistency of the docs.

[Joseph Tooby-Smith]

Michael Rothgang said:

(I would love to do the same in mathlib, certainly in the files I care about.)

I think with PhysLean, and maybe if something similar is done with Mathlib, it would be best to have a file containing those modules which should be linted using such a linter - and then increasing add stuff to that file.

[Joseph Tooby-Smith]

Very rudimentary script for linting module doc headers in line with the style of the examples above here: PhysLean#744

[Joseph Tooby-Smith]

I made the following automatic documentation tracker to replace what I was doing above, along with instructions how to contribute to the documentation. Any feedback welcome.

https://physlean.com/DocumentationTracker