This may have already been discussed to oblivion, but the default meaning of axioms in
make validate seems a bit off. In particular, if I do
From Coq Require Import Program.Equality.
I get a report saying I'm using
Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq, since apparently some proofs in
Program.Equality use it, even when I don't in my module with the
From ... Require. Is there an obvious way to restrict axiom reporting to what I actually use in the module names I pass to
coqchk? Or can it be done using some hack?
-norec module check module but admit dependencies without checking
or -admit the stdlib modules
wait, so if my project has
m3.v I would want to do this?
"coqchk" -silent -o -norec m1.vo m2.vo m3.vo
-norec m1.vo -norec m2.vo -norec m3.vo
hmm, this is a bit strange on Coq 8.16.1:
$ cat theories/test.v From Coq Require Import Program.Equality. $ coqchk -silent -o -Q theories Validate -norec theories/test.vo CONTEXT SUMMARY =============== * Theory: Set is predicative * Axioms: Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
I might be missing something
I guess -norec doesn't disable axiom reporting
OK, might this be considered a bug or at least strange behavior worth an issue/fix?
I have several projects that we do regular axiom analysis on, and the proper norec axiom reporting probably makes the most sense ("our code at least doesn't rely on axioms")
I guess I'll at least write a short issue to make my case
Doesn't -norec lets you use libraries failing coqchk? And I agree with Karl overall; I've used Print Assumptions in the past, and I've seen projects just be careful with require, but that's indeed pretty expensive
maybe axiom reporting should be thought of as separate from checking, so there is
-axioms bla.vo or similar, that doesn't affect checking
You probably want a specific axiom check for a given global reference (definition or inductive), like Print Assumptions.
Last updated: Dec 05 2023 at 12:01 UTC