Given:

```
cat import_only.v
Require Import Classical.
```

then:

```
coqchk -silent -o import_only.vo
[...]
* Axioms:
Coq.Logic.Classical_Prop.classic
```

This surprises me. I expected it to behave like `Print Assumptions`

, which actually looks for the axioms that were used instead of simply the axioms that exist in the context.

Why is this? Is there some way to do the equivalent of `Print Assumptions`

for every "leaf" of the development (or, more bruteforcy, for every lemma/definition)?

Oh. I just realized it is checking the assumptions of everything in the `Classical`

file. :woman_facepalming:

Gah, this is annoying! Maybe not for `Classical`

, which I only import if I want to use classical logic, but I originally noticed this with `Program.Wf`

. You can use it without functional extensionality, but since it includes the line `Require Import FunctionalExtensionality.`

in order to prove a specific lemma, the functional extensionality axiom appears in `coqchk`

from then on.

if you want to avoid checking modules depended on by your modules, then I think you need to use the `-norec`

option for `coqchk`

. However, this is discouraged by for example the Common Criteria eval recommendations

"Program imports more axioms than you'd like" is a known annoyance, and e.g. https://github.com/coq/coq/issues/15408#issuecomment-1014275290 suggests PRs are welcome

currently, I just eschew `Require Import Program`

and have more granular imports (just those from stdpp: `From Coq.Program Require Import Basics Syntax.`

).

while I do use `Program`

, I don't recommend its well-founded recursion support. Robust use of WfRec requires proving unfolding lemmas, which Equations (and Function) generate but `Program`

doesn't.

You can do `coqchk -norec`

to check only the module passed after norec.

That can be combined with an incremental check where you do this for all files.

Or you could pass all the files you want to check at once each with a -norec.

Oh I missed that -norec was mentioned already oops.

Last updated: Jun 15 2024 at 08:01 UTC