After upgrading some dependencies, I started seeing some unexpected axioms in the output of `make validate`

. I'd like to better understand why we (started to) depend on these axioms. Due to `opam`

's version constraint resolution, there are many version changes all at once, so I cannot easily single out a specific dependency as the root cause. I checked `coqchk --help`

and `coq_makefile --help`

, but didn't spot anything that seemed helpful. What's the best way to track down which module/lemma/dependency introduces an axiom?

You might want to give a look at https://github.com/coq-community/coq-dpdgraph, which gives you tooling to look at the recursive dependencies of a Coq object, in particular on axioms

we have some really hacky shell scripts / make tasks here precisely for tracking down axioms showing up unexpectedly in `make validate`

:

- https://github.com/runtimeverification/vlsm/blob/master/scripts/axiom-diagnostics.sh
- https://github.com/runtimeverification/vlsm/blob/master/Makefile.coq.local#L34-L36

Thanks a lot for the pointers! I’ve poked around a bit with dpdgraph, a very cool utility! I will certainly find good use for this in the future.

Unfortunately, for the problem at hand, I’m confused by what I’m seeing. Or, rather, not seeing.

To start, I selected a small, very simple module (a nat utility definition plus some lemmas). I ran coqchk on just this module, and as before it listed all the unexpected axioms (related to primitive ints and floats). (Aside: Why would a file on natural numbers depend on floating point axioms in the first place…!?)

Then I ran dpdgraph on some of the lemmas: it does _not_ mention any of the axioms, as I would expect.

To confirm, I checked with Print Assumptions each (simple) lemma in the module. They are all closed under the global context, ie axiom-free as I would expect them to be.

Why would coqchk report a dependency on any axioms then?

coqchk reports the axioms present in the files it loaded

it is not about them being used

Ah, I see, so any opam dependencies gaining new features or rearranging how imports are organized can cause “false positives” for all downstream clients, irrespective of actual use. Thanks for the clarification. I somehow had the misconception that coqchk would be precise (eg, in analogy to how closing a section will disregard unused hypotheses).

Unfortunately, this is nonideal for my use case, which is to check in CI that we haven’t accidentally started _using_ any new axioms.

Is there an easy way to get a precise equivalent of “make validate”?

Found the link: mathcomp -> hierarchy builder -> elpi

No way to avoid that. :-/

see this issue for a description of some problems with what `coqchk`

reports on axioms: https://github.com/coq/coq/issues/17345

Thanks for raising the issue. That’s exactly it. It’s a bit discouraging that there has not been follow-up discussion, at least not visibly on GitHub.

Björn Brandenburg said:

Is there an easy way to get a precise equivalent of “make validate”?

``Print Assumptions thm.`

more precisely lists all assumptions used in the proof of `thm`

but that's not practically usable on an entire library (except maybe if it's only goal is to prove a handful theorems).

Björn Brandenburg said:

Found the link: mathcomp -> hierarchy builder -> elpi

Out of curiosity, do you remember which axioms? Mathcomp is designed (until now) to be axiom free so I'd consider this at least an annoyance if not a bug.

Björn Brandenburg said:

Thanks for raising the issue. That’s exactly it. It’s a bit discouraging that there has not been follow-up discussion, at least not visibly on GitHub.

Ressources of the development team are limited and although coqchk is maintained, nobody is actually working on it. Pull requests would certainly be considered though.

the shell script referenced above uses the `Print Assumptions`

approach on "every" theorem, so even if fragile and hacky, one could likely build something more robust using the same approach:

https://github.com/runtimeverification/vlsm/blob/master/scripts/axiom-diagnostics.sh#L56-L79

we were able to run `Print Assumptions`

on basically every theorem in a 50k+ LOC library in a few minutes

Yeah, I might end up doing something similar (or repurpose your script), but I don’t like giving up on being able to claim that our trust base is only “official” tooling maintained and “blessed” by the Coq project. The difference in persuasive power between “it’s a script I hacked up; trust me bro” and “it’s the official Coq way” is quite substantial.

Pierre Roux said:

Björn Brandenburg said:

Thanks for raising the issue. That’s exactly it. It’s a bit discouraging that there has not been follow-up discussion, at least not visibly on GitHub.

Ressources of the development team are limited and although coqchk is maintained, nobody is actually working on it. Pull requests would certainly be considered though.

I fully understand. Unfortunately, I’m not fluent in OCaml and the Coq codebase is not the most beginner-friendly there is.

to me, the "new" baseline in the Coq community for what is trustworthy/recommended is what is included in the Coq Platform (it has an editorial board and everything). If there is interest for co-developing a more robust tool for axiom analysis that could be included in the Platform, we are happy to host this in Coq-community. For example, coq-dpdgraph is currently developed in Coq-community and part of the Platform.

Pierre Roux said:

Björn Brandenburg said:

Found the link: mathcomp -> hierarchy builder -> elpi

Out of curiosity, do you remember which axioms? Mathcomp is designed (until now) to be axiom free so I'd consider this at least an annoyance if not a bug.

It’s quite a few. You can see the full list in Prosa’s CI starting here: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/jobs/267686#L362

Here’s the corresponding MR: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/358

With MathComp 1.18, we have no axioms (according to make validate). With MathComp 2.2.0, it’s a long list. As I said, I think this is inherited via elpi.

as Pierre points out above, Coq core team resources are limited, and the rest of us are mostly working on volunteer basis and on specific stuff we need for work/research. Nevertheless, there are quite a few Coq utility tools out there, see https://github.com/coq-community/awesome-coq#tools

the closest one w.r.t. axiom analysis might be https://github.com/JasonGross/coq-tools and we have this proposal https://github.com/coq/platform/issues/378

Björn Brandenburg said:

With MathComp 1.18, we have no axioms (according to make validate). With MathComp 2.2.0, it’s a long list. As I said, I think this is inherited via elpi.

Thanks, the long list seems to all boil down to primitive integers and floats imported there https://github.com/LPCIC/coq-elpi/blob/75b619727c7ae8e22e79b1a70331afa9c47f8eba/theories/elpi.v#L48-L51 . I think the vast majority of coq-elpi users are not using that, so maybe this should come in a separate opt-in file, what do you think @Enrico Tassi ?

Here is an attempt to fix that: https://github.com/LPCIC/coq-elpi/pull/579

not sure why elpi even needs a separate registration for primitives tbh, is there ever a case where they wouldn't be the same as the kernel ones?

No, but I wanted the file so assert the existence of the constants. So the PR of Pierre is not really what we want, I think. I guess I'd prefer to not define my librefs, use the coq one, but if they are not set give a good error message.

actually lib_ref doesn't look at the kernel so we register the primitives eg https://github.com/coq/coq/blob/078eaa3fa0dfe45aca5948b882a0f759db97ad08/theories/Numbers/Cyclic/Int63/PrimInt63.v#L19 `Register int as num.int63.type.`

@gares what do you consider a good error message? If I try removing the `Require Import PrimInt63 PrimFloat.`

in my PR i get error messages like:

```
Error:
File "apps/derive/elpi/eqType.elpi", line 66, column 29, character 3552:
The reference PrimInt63.int was not found in the current environment.
```

or

```
Error:
File "elpi/elpi_elaborator.elpi", line 311, column 76, character 12059:
not found in table: num.int63.type
```

I'd tend to consider those good enough.

The first one is good, but that is probably a locate/quotation mentioning PrimInt63.int.

The second one, Id like it to mention that one has to Require PrimInt63 or something like that.

I guess we have to guard with a try-with a call to `Coqlib.blabla`

Even "you have to require the file in which this Register command is present" would be better (even in Coq, frankly)

last I looked it's pretty hard to get a "not found in table" with stdlib

for instance the syntax from primitive ints is declared in the same file as the primitives are registered, so if you say `0%uint63`

before requiring it you get something like "unknown scope uint63" (and even if you declare the scope 0%uint63 won't try to produce a primitive until you say Number Notation ... where one of the arguments is the `int`

primitive type or depends on it, closing the loop)

the array syntax says `The type array must be registered before this construction can be typechecked.`

if arrays aren't declared

I guess elpi has some syntax to produce a primitive literal or some such thing, that syntax needs to check that the primitive type (int/float/array) is registered and can produce whatever error

Yes, like any random OCaml plugin could look for any nonexistent registration.

@Enrico Tassi now the PR gives

```
Error:
File "elpi/elpi_elaborator.elpi", line 311, column 76, character 12059:
Global reference not found: lib:num.int63.type (you may need to require some .v file with `Register ... as num.int63.type.`).
```

great!

For the particular case of primitives it might be worth putting them in a separate category than axioms for coqchk and the like e.g, trusted built-in types or something like this?

Last updated: Jun 22 2024 at 16:02 UTC