Stream: Coq users

Topic: ✔ Good coding practices for coq


view this post on Zulip walker (Sep 24 2022 at 22:12):

This first of few posts on this topic (the next will be request for code review for stuff I wrote)

For most programming languages, there is good coding practices/patterns that developers should stick to,
(stuff that goes into the linting of any programming language).

Is there similar good/bad practices for Coq, I am looking at things that include stuff to avoid, stuff to adhere to, naming conventions (especially lemma naming conventions, I don't know a good strategy to pick good names for theorems, lemmas). Any thing in general that makes code more readable for coq in particular (aside from commenting the code).

view this post on Zulip walker (Sep 24 2022 at 22:14):

bonus points for any coq linters.

view this post on Zulip Karl Palmskog (Sep 24 2022 at 22:34):

view this post on Zulip walker (Sep 24 2022 at 22:43):

thanks a lot, I will see the styles referenced in the paper, but the third document is almost the thing I am looking for as a starting point.

view this post on Zulip Notification Bot (Sep 24 2022 at 22:50):

walker has marked this topic as resolved.

view this post on Zulip Ana de Almeida Borges (Sep 25 2022 at 13:24):

Some additions:

Note that what is an anti-pattern in one style can be a pattern in another. If you're relying heavily on a given set of libraries (MathComp, Iris, etc), it might be a good idea to try to emulate its style. From what I understand the standard library doesn't have much of a fixed style.

view this post on Zulip Karl Palmskog (Sep 25 2022 at 13:32):

the Stdlib has multiple styles. Sometimes consistent across a subset of files.


Last updated: Jan 29 2023 at 01:02 UTC