Feature request: support for running standalone checker on Coq .vo files

[palmskog]

The .vo files produced by coqc when building a Coq project contain proof objects. However, a user has to trust the implementation of coqc, which is tied into the whole implementation of Coq, to trust that these proof objects are well-formed according to Coq's underlying theory (which is proven by pen-and-paper to be relatively consistent with ZFC set theory).

An alternative standalone checker for Coq proof objects is coqchk, which takes a list of library paths for .vo files as argument, recursively processing the libraries they depend on. coqchk has a smaller trusted base than coqc and currently avoids some potential pitfalls in coqc, such as trusting Coq sections.

If a user could trigger a coqchk checking pass via dune, this could improve user trust in the build. Dune could also potentially figure out how to do minimal recursive checking when files are changed, by passing only impacted .vo files as library paths to coqchk.

[ejgallego]

We could add a rule .vo -> .chk so users could indeed request for checking such files; that could be integrated into the test target somehow.

On the other hand, the utility of coqchk is fairly limited, as of today it is almost an exact copy of the common kernel and in 8.11 problems such as the one with sections should be solved in a different way, thus I am not sure how prioritary this is.

[palmskog]

The same ideas would apply to a potential checker produced by MetaCoq, so even though this may not be a priority, I think it's good to have it recorded somewhere.

[ejgallego]

Given that running coqchk 🐓 produces no objects, indeed this could be covered by the plug-in API which I hope to use for example to implement Coq's test suite .

[Alizter]

I also need something like this. @ejgallego have you got any ways to pull this off right now?

Also would it make sense to put this under the @check target?

[Alizter]

FTR the workaround is the following:

(rule
 (alias runtest)
 (deps
  (glob_files_rec ./*.vo))
 (action
  (run coqchk -R ./theories HoTT -Q contrib HoTT.Contrib %{deps} -o)))

This will glob all the vo files in a directory recursively and pass them to coqchk (you should adjust the flags). It is also possible to write singluar per vo rules that use coqchk -norec module but this is much slower than doing it all at once.

I don't think it is a priority to support coqchk in Dune at the moment, and the workaround is pretty much what you want anyway. What could be improved is the flags the user will have to setup.