Stream: Coq devs & plugin devs

Topic: make validate axioms

Karl Palmskog (Mar 06 2023 at 12:17):

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?

Gaëtan Gilbert (Mar 06 2023 at 12:20):

-norec module check module but admit dependencies without checking

Gaëtan Gilbert (Mar 06 2023 at 12:20):

or -admit the stdlib modules

Karl Palmskog (Mar 06 2023 at 12:22):

wait, so if my project has m1.v, m2.v, m3.v I would want to do this?

"coqchk" -silent  -o  -norec m1.vo m2.vo m3.vo

Gaëtan Gilbert (Mar 06 2023 at 12:23):

no, -norec m1.vo -norec m2.vo -norec m3.vo

Karl Palmskog (Mar 06 2023 at 12:25):

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

Gaëtan Gilbert (Mar 06 2023 at 12:27):

I guess -norec doesn't disable axiom reporting

Karl Palmskog (Mar 06 2023 at 12:29):

OK, might this be considered a bug or at least strange behavior worth an issue/fix?

Karl Palmskog (Mar 06 2023 at 12:30):

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

Gaëtan Gilbert (Mar 06 2023 at 12:31):

IDK

Karl Palmskog (Mar 06 2023 at 12:33):

I guess I'll at least write a short issue to make my case

Karl Palmskog (Mar 06 2023 at 12:42):

https://github.com/coq/coq/issues/17345

Paolo Giarrusso (Mar 06 2023 at 13:14):

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

Karl Palmskog (Mar 06 2023 at 13:19):

maybe axiom reporting should be thought of as separate from checking, so there is -axioms bla.vo or similar, that doesn't affect checking

Matthieu Sozeau (Mar 08 2023 at 17:15):

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