Documentation

[kbuzzard]

The code should somehow be documented. My dream for this would be that the low-level files (like valuation.basic) just get big comment blocks at the top explaining the API of the file, and the higher level files get LaTeX code which could be read using Patrick's formatter. I am a bit unclear about what exactly we can do here, but ultimately now we have the code I think that we should be thinking about trying to make what we have more accessible to mathematicians.

[jcommelin]

The list of files (sorted, somehow) that is not in for_mathlib/:

• Huber_ring/basic.lean
• Huber_ring/localization.lean
• Huber_ring/padics.lean
• Spa/localization_Huber.lean
• Spa/rat_open_data_completion.lean
• Spa/space.lean
• Spa/stalk_valuation.lean
• examples/empty.lean
• examples/padics.lean
• valuation/basic.lean
• valuation/canonical.lean
• valuation/field.lean
• valuation/group_with_zero.lean
• valuation/linear_ordered_comm_group_with_zero.lean
• valuation/localization.lean
• valuation/topology.lean
• valuation/valuation_field_completion.lean
• valuation/with_zero_topology.lean
• Frobenius.lean
• Huber_pair.lean
• Tate_ring.lean
• adic_space.lean
• continuous_valuations.lean
• perfectoid_space.lean
• power_bounded.lean
• valuation_spectrum.lean

[jcommelin]

For the files that are not in sheaves/ or for_mathlib:

• All these files have module docstrings
• All the definitions have docstrings

There is still a list of TODO's, and things can be quite improved. But this list seems to have served it's purpose.

[PatrickMassot]

Thanks for your amazing efforts with this list Johan!

[jcommelin]

I didn't close this on purpose, because Kevin's first post contains a bunch of stuff that hasn't been done yet. (Even though, it's not likely that we'll get to it soon.)