Stream: coq-community devs & users

Topic: New maintainers of topology and zorns-lemma

Karl Palmskog (Dec 20 2020 at 17:58):

@Columbus I invited you on GitHub to be a member of the coq-community organization. When you accept, I can make you admin of topology and zorns-lemma. We usually recommend people to do proposed changes via pull requests for branches in the repo rather than a fork (making it easier for others to add to a topic branch)

Stéphane Desarzens (Dec 20 2020 at 18:00):

Thanks.

Karl Palmskog (Dec 20 2020 at 18:01):

please take a look at our templates for the general workflow on how to update boilerplate like CI configuration: https://github.com/coq-community/templates

Karl Palmskog (Dec 20 2020 at 18:04):

we also have a recommended project structure that you could consider for your projects: https://github.com/coq-community/manifesto/wiki/Recommended-Project-Structure

Stéphane Desarzens (Dec 20 2020 at 19:47):

Thanks for the links. I haven’t noticed the wiki yet.
Is there a "style guide" or something about the formatting of the code/proofs?

Karl Palmskog (Dec 20 2020 at 19:50):

there is nothing general for Coq style/formatting, but here are some examples of project-specific styles:

• https://gitlab.mpi-sws.org/iris/iris/blob/iris-3.2.0/StyleGuide.md
• https://github.com/math-comp/math-comp/blob/mathcomp-1.9.0/CONTRIBUTING.md

Stéphane Desarzens (Dec 20 2020 at 19:52):

Ok, thanks. I also know of the HoTT Style guide.

Karl Palmskog (Dec 20 2020 at 19:53):

with some colleagues, I'm working on a machine learning based tool that can suggest formatting/style (short abstract with examples https://arxiv.org/abs/2006.16743), but we are quite far from being generally usable yet

Karl Palmskog (Dec 20 2020 at 19:54):

another example: https://github.com/uwplse/verdi-raft/blob/master/STYLE.md

Stéphane Desarzens (Dec 20 2020 at 19:54):

:D that’d be nice

Karl Palmskog (Dec 20 2020 at 19:57):

this is a good guide for best practices which are not style related: https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.0-en.pdf

Stéphane Desarzens (Dec 20 2020 at 20:00):

I remember reading that one.

Karl Palmskog (Dec 20 2020 at 20:00):

there are also tools/plugins that can help with maintenance, e.g., https://github.com/Karmaki/coq-dpdgraph

we try to maintain a list of useful stuff (resources/tools) at https://github.com/coq-community/awesome-coq

Last updated: Jun 06 2023 at 23:01 UTC