Karl Palmskog (Sep 24 2020 at 14:23): 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.
Bas Spitters (Sep 24 2020 at 14:27):It would be great to have such guidelines, and hopefully a linter that helps following them.
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
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: Jun 03 2023 at 18:01 UTC