cat import_only.v Require Import Classical.
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
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: Oct 01 2023 at 19:01 UTC