If we want the platform to be dependable, it might be warranted to introduce tooling to analyze and summarize what axioms different libraries use, right? For example, one could run
make validate or some custom
coqchk command for each project in CI before a release and process output into a Markdown report. However, this output is currently not very fine-grained, as I describe here.
I have little experience with this (short of Print Assumptions on my high level results). I am not sure I understand what you suggest. Are there tools which print axioms recursively used in a .v file?
make validate does this to an extent. Let me illustrate on 8.14.0:
~/src/coq/coq-community/reglang$ make -j3 ... ~/src/coq/coq-community/reglang$ make validate make: Entering directory '/home/palmskog/src/coq/coq-community/reglang' "coqchk" -silent -o -Q theories RegLang theories/misc.vo theories/setoid_leq.vo theories/languages.vo theories/dfa.vo theories/nfa.vo theories/regexp.vo theories/minimization.vo theories/myhill_nerode.vo theor ies/two_way.vo theories/vardi.vo theories/shepherdson.vo theories/wmso.vo CONTEXT SUMMARY =============== * Theory: Set is predicative * Axioms: Coq.micromega.ZifyInst.ltac_gen_subproof9 Coq.micromega.ZifyInst.ltac_gen_subproof8 Coq.micromega.ZifyInst.ltac_gen_subproof7 Coq.micromega.ZifyInst.ltac_gen_subproof6 Coq.micromega.ZifyInst.ltac_gen_subproof5 Coq.micromega.ZifyInst.ltac_gen_subproof4 Coq.micromega.ZifyInst.ltac_gen_subproof3 Coq.micromega.ZifyInst.ltac_gen_subproof2 Coq.micromega.ZifyInst.ltac_gen_subproof1 Coq.micromega.ZifyInst.ltac_gen_subproof0 Coq.micromega.ZifyInst.ltac_gen_subproof22 Coq.micromega.ZifyInst.ltac_gen_subproof21 Coq.micromega.ZifyInst.ltac_gen_subproof20 Coq.micromega.ZifyInst.ltac_gen_subproof19 Coq.micromega.ZifyInst.ltac_gen_subproof18 Coq.micromega.ZifyInst.ltac_gen_subproof17 Coq.micromega.ZifyInst.ltac_gen_subproof16 Coq.micromega.ZifyInst.ltac_gen_subproof15 Coq.micromega.ZifyInst.ltac_gen_subproof14 Coq.micromega.ZifyInst.ltac_gen_subproof13 Coq.micromega.ZifyInst.ltac_gen_subproof12 Coq.micromega.ZifyInst.ltac_gen_subproof11 Coq.micromega.ZifyInst.ltac_gen_subproof10 Coq.micromega.ZifyInst.ltac_gen_subproof * Constants/Inductives relying on type-in-type: <none> * Constants/Inductives relying on unsafe (co)fixpoints: <none> * Inductives whose positivity is assumed: <none>
in a tentative scenario where one does "axiom evaluation" for the Platform,
coqchk would probably be tweaked with
-norec and similar options, to avoid checking things we already know are axiom free...
we should fix those subproof axioms though
Until that's fixed, one could also add a blacklist to
coqchk itself (or to postprocessing in platform CI), since everybody sees _these_ specific names?
Isn't it so that coqchk has issues e.g. with heavy module stuff? Afair @Xavier Leroy once told me that CompCert doesn't run through coqchk with reasonable memory resources (32 GB or so).
I agree that it may be impractical to run
coqchk regularly on all platform projects. But setting up tooling/CI for
coqchk and then having a "white list" of projects to run it on would still be nice in my opinion, and could lead to input to Coq devs on how to improve
coqchk. For example, if we assume there is a Platform Docker image, you already have all the
.vo files done, so axiom auditing becomes a separate step.
I was trying to push for the Dune equivalent of
make validate before, but it may have stalled due to lack of developer time: https://github.com/ocaml/dune/issues/2197
Many coqchk performance bugs also seem fixed these days (at least, all those affecting iris)
the functor issue hasn't changed though
it's the difference between checking
(fun x => body) term and the beta-reduced result (coqc gets the first, coqchk gets the second, replacing lambda by module functor)
Last updated: Jan 30 2023 at 11:03 UTC