Stream: coq-community devs & users

Topic: Common criteria guidelines in coq-community projects


view this post on Zulip Karl Palmskog (Sep 24 2020 at 14:23):

@Christian Doczkal given that Proof using. is now officially best practices for Coq evaluations in France, do you still have the same view about merging my add-proof-using branch in RegLang? It seems likely we will adopt similar guidelines as they did for Common Criteria for inclusion in the Coq Platform.

view this post on Zulip Bas Spitters (Sep 24 2020 at 14:27):

It would be great to have such guidelines, and hopefully a linter that helps following them.

view this post on Zulip Karl Palmskog (Sep 24 2020 at 14:33):

not all points will be possible to automate/lint, but I think a lot comes from coq-community project maintainers having the long-term goal to be compliant with guidelines like the ones for Common Criteria

view this post on Zulip Karl Palmskog (Sep 24 2020 at 14:43):

one point in particular is that we currently have no way to tell what the "main lemmas" of a Coq project are (which one should run Print Assumptions on,etc.). We could adopt some convention that "all non-main lemmas must use Lemma, while main lemmas must use Theorem". This could make automation more feasible


Last updated: Feb 04 2023 at 02:03 UTC