Stream: Coq Platform devs & users

Topic: axiom auditing of Platform

view this post on Zulip Karl Palmskog (Nov 27 2021 at 11:43):

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.

view this post on Zulip Michael Soegtrop (Nov 27 2021 at 12:48):

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?

view this post on Zulip Karl Palmskog (Nov 27 2021 at 12:52):

coqchk via 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[1]: 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>

view this post on Zulip Karl Palmskog (Nov 27 2021 at 12:55):

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

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 13:00):

we should fix those subproof axioms though

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 13:00):

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

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 14:54):

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?

view this post on Zulip Michael Soegtrop (Nov 29 2021 at 10:25):

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

view this post on Zulip Karl Palmskog (Nov 29 2021 at 10:30):

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.

view this post on Zulip Karl Palmskog (Nov 29 2021 at 10:34):

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

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 12:54):

Many coqchk performance bugs also seem fixed these days (at least, all those affecting iris)

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:01):

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: Jun 03 2023 at 03:01 UTC