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


* Theory: Set is predicative

* Axioms:

* 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):

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:

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: Jan 30 2023 at 11:03 UTC