coqchk happily accepts admitted proofs. And I can’t find any command line
option to tell Coq to complain about such unsafe features. Any help is welcomed!
I’m not sure how future-proof this is but it works now:
coqchk --output-context file.vo 2>&1 | grep "* Axioms: <none>" && echo "Success\!"
I’m happy to learn a better solution!
Certainly we should have an issue about this, adding a
coqchk -axiom-free that returns a non-zero return code if some Axioms/Unsafe features are used.
I opened an issue as you suggested: https://github.com/coq/coq/issues/10372
You could use SerAPI [or your custom coqtop talking device] to actually query for status of lemmas, assumptions, etc…
But in the end, the issue of guaranteeing you got the right proof is a bit more complicated than what it looks.
Anyways, adding a flag that would bar
Admitted proofs if pretty easy, but you also need to take into account primitives for example.