Stream: Coq devs & plugin devs

Topic: make validate axioms


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Mar 06 2023 at 12:20):

-norec module check module but admit dependencies without checking

view this post on Zulip Gaëtan Gilbert (Mar 06 2023 at 12:20):

or -admit the stdlib modules

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Mar 06 2023 at 12:23):

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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Mar 06 2023 at 12:27):

I guess -norec doesn't disable axiom reporting

view this post on Zulip Karl Palmskog (Mar 06 2023 at 12:29):

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

view this post on Zulip 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")

view this post on Zulip Gaëtan Gilbert (Mar 06 2023 at 12:31):

IDK

view this post on Zulip Karl Palmskog (Mar 06 2023 at 12:33):

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

view this post on Zulip Karl Palmskog (Mar 06 2023 at 12:42):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jun 09 2023 at 08:01 UTC