The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi Timothy,

That sounds great! In the Iris project, we have a more or less ad-hoc style 
guide of sorts that we started writing down at 
<https://gitlab.mpi-sws.org/iris/iris/-/wikis/style-guide>. That list is far 
from complete and very WIP, but it might still be helpful to you. It involves 
not just formatting but also naming conventions. I am sure people will disagree 
on some of these decisions though. ;)
If there was a Coq style guide we could just have copied, that sure would have 
made our life a lot easier.

One aspect that I think is important and often underestimated around style 
guides is automated formatters: consistently using a style guide is *a lot* 
easier if there is a tool you can run that re-formats code to be in line with 
the style guide (at least insofar as spacing and indentation is concerned). Many 
language communities have made that experience (rustfmt and go fmt come to my 
mind). This also enables things like enforcing correct formatting on CI. I think 
this is crucial for adopting a consistent style without making life too hard for 
contributors.

Kind regards,
Ralf

On 01.12.21 16:58, Timothy Carstens wrote:
> Do you have an opinion on how to style Coq code/projects?
>
> I'm currently working on assembling a style guide for Coq projects. The goal is 
> to provide clear recommendations that are informed by experience and guided by 
> relevant use cases/./ I've included a brief FAQ at the bottom with more information.
>
> The project is still in its infancy. I want the output to be relevant to /you/ 
> so I am reaching out to ask:
>
> * Are you interested in joining this effort? It would be great to put together a 
> small group of people who can help set the goals & manage the execution of this 
> project.
>
> * Do you know of any other good Coq style guides or similar resources?
>
> * Do you have any other relevant thoughts/comments/suggestions that you'd like 
> to share?
>
> Kindly yours,
> -t
> //
> /
> /
> /
> /
> /Why adopt a style guide?/
>
> Everyone who interacts with code is impacted by code style. This clearly 
> includes the project’s contributors, but it also includes other interested 
> parties such as users and upstream maintainers. In other words, style is 
> relevant to many different /roles and personas/ engaged in many different /use 
> cases/.
>
> A style is “good” if it has a net-positive impact on those use cases.
>
> Good style does not arise by accident; rather, it is engineered by carefully 
> considering how different idioms & practices impact different use cases.
>
> This is a lot of work to get right. Therefore, many projects adopt a style guide 
> - either in full, or as a starting point for their own style.
>
>
> /What does a good style guide look like?/
> /
> /
> * The Google C++ Style Guide: https://google.github.io/styleguide/cppguide.html 
> <https://google.github.io/styleguide/cppguide.html>
> * Awesome Guidelines: https://github.com/Kristories/awesome-guidelines 
> <https://github.com/Kristories/awesome-guidelines>
>
>
> /How does this relate to /Requirements on the Use of Coq in the Context of 
> Common Criteria Evaluations/?/
>
> /Requirements on the Use of Coq in the Context of Common Criteria Evaluations/ 
> is a requirements document published by ANSSI and INRIA. While most projects are 
> unlikely to be used in a Common Criteria Evaluation, the guidance offered by 
> this document is valuable in other contexts as well.
>
> With respect to coding style, the document says:
>
>      There is no well-established coding style for Coq development. The present 
> document does not attempt to fill this gap, but rather to identify and 
> discourage known bad practices.
>
> This style guide aims to fill this gap.

--
Website: https://ralfj.de/research