@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.

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

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

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