Stream: Coq devs & plugin devs

Topic: Maintaining a library of formal mathematics

Théo Zimmermann (Jul 29 2020 at 20:42):

A great talk by Gabriel Ebner from mathlib, at CICM 2020, where he talks about maintaining mathlib, and in particular about linters and about documentation: https://www.youtube.com/watch?v=5HDlgsjO8-w
Lots of interesting ideas to steal from them :stuck_out_tongue_wink:
The associated paper (by Floris van Doom, Gabriel Ebner and @Rob Lewis) is here (I haven't read it yet): https://arxiv.org/abs/2004.03673

Karl Palmskog (Jul 29 2020 at 20:44):

right, I've highlighted that paper before (but the video link is useful, thanks!) and Enrico said some of what they do can be implemented on top of Coq-Elpi. However, implementing similar linters for Coq would not have the same (relative) value as for Lean+Mathlib, since the audience will likely be small (no two Coq projects typically have the same conventions). On the other hand, a type/interface for linting rules could be useful for Coq to allow users to handpick tens of rules for their projects (which could also be used to enhance learning-based formatting).

Bas Spitters (Jul 29 2020 at 21:04):

Perhaps no two projects have the same rules is due to the lack of a linter ?
Such an interface seems useful.

Théo Zimmermann (Jul 29 2020 at 21:28):

There use cases for linting seemed pretty consensual (verify that there are no useless arguments, verify that hints are not redundant) or ambitious (ensure that typeclass resolution does not blow up).

Last updated: May 31 2023 at 15:01 UTC