Stream: Coq users

Topic: tracking down source of axiom dependency


view this post on Zulip Björn Brandenburg (Jan 25 2024 at 18:54):

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?

view this post on Zulip Meven Lennon-Bertrand (Jan 25 2024 at 19:19):

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

view this post on Zulip Karl Palmskog (Jan 25 2024 at 19:26):

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

view this post on Zulip Björn Brandenburg (Jan 25 2024 at 21:09):

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?

view this post on Zulip Gaëtan Gilbert (Jan 25 2024 at 21:28):

coqchk reports the axioms present in the files it loaded
it is not about them being used

view this post on Zulip Björn Brandenburg (Jan 25 2024 at 22:12):

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

view this post on Zulip Björn Brandenburg (Jan 25 2024 at 22:25):

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

No way to avoid that. :-/

view this post on Zulip Karl Palmskog (Jan 26 2024 at 06:02):

see this issue for a description of some problems with what coqchk reports on axioms: https://github.com/coq/coq/issues/17345

view this post on Zulip Björn Brandenburg (Jan 26 2024 at 06:26):

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.

view this post on Zulip Pierre Roux (Jan 26 2024 at 07:11):

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

view this post on Zulip Pierre Roux (Jan 26 2024 at 07:13):

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.

view this post on Zulip Pierre Roux (Jan 26 2024 at 07:16):

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.

view this post on Zulip Karl Palmskog (Jan 26 2024 at 07:25):

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

view this post on Zulip Karl Palmskog (Jan 26 2024 at 07:29):

we were able to run Print Assumptions on basically every theorem in a 50k+ LOC library in a few minutes

view this post on Zulip Björn Brandenburg (Jan 26 2024 at 08:16):

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.

view this post on Zulip Björn Brandenburg (Jan 26 2024 at 08:17):

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.

view this post on Zulip Karl Palmskog (Jan 26 2024 at 08:19):

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.

view this post on Zulip Björn Brandenburg (Jan 26 2024 at 08:21):

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.

view this post on Zulip Karl Palmskog (Jan 26 2024 at 08:23):

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

view this post on Zulip Karl Palmskog (Jan 26 2024 at 08:24):

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

view this post on Zulip Pierre Roux (Jan 26 2024 at 08:27):

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 ?

view this post on Zulip Pierre Roux (Jan 26 2024 at 09:01):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 10:03):

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?

view this post on Zulip Enrico Tassi (Jan 26 2024 at 12:37):

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.

view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 12:43):

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.

view this post on Zulip Pierre Roux (Jan 26 2024 at 13:48):

@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.

view this post on Zulip Enrico Tassi (Jan 26 2024 at 13:50):

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

view this post on Zulip Enrico Tassi (Jan 26 2024 at 13:51):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 14:02):

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

view this post on Zulip Pierre Roux (Jan 26 2024 at 14:04):

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

view this post on Zulip Pierre Roux (Jan 26 2024 at 14:29):

@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.`).

view this post on Zulip Enrico Tassi (Jan 26 2024 at 14:34):

great!

view this post on Zulip Matthieu Sozeau (Feb 05 2024 at 17:17):

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