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
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).
Perhaps no two projects have the same rules is due to the lack of a linter ?
Such an interface seems useful.
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: Feb 05 2023 at 20:03 UTC