Safe mode checking nothing was admitted?

Using Coq
1

Apparently 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!

2

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!

1 Like
3

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.

3 Likes
4

I opened an issue as you suggested: https://github.com/coq/coq/issues/10372

1 Like
5

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.