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?

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

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

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

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: Jun 16 2024 at 01:42 UTC