Stream: Coq users

Topic: make validate / coqchk lists axioms that were not used

Ana de Almeida Borges (Nov 04 2022 at 13:32):

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)?

Ana de Almeida Borges (Nov 04 2022 at 13:33):

Oh. I just realized it is checking the assumptions of everything in the Classical file. :woman_facepalming:

Ana de Almeida Borges (Nov 04 2022 at 13:40):

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.

Karl Palmskog (Nov 04 2022 at 13:58):

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

Paolo Giarrusso (Nov 06 2022 at 12:59):

"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

Paolo Giarrusso (Nov 06 2022 at 13:01):

currently, I just eschew Require Import Program and have more granular imports (just those from stdpp: From Coq.Program Require Import Basics Syntax.).

Paolo Giarrusso (Nov 06 2022 at 13:03):

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.

Ali Caglayan (Nov 08 2022 at 23:49):

You can do coqchk -norec to check only the module passed after norec.

Ali Caglayan (Nov 08 2022 at 23:49):

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

Ali Caglayan (Nov 08 2022 at 23:50):

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

Ali Caglayan (Nov 08 2022 at 23:50):

Oh I missed that -norec was mentioned already oops.

Last updated: Oct 01 2023 at 19:01 UTC