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

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.

The issue names no repository files or tests. Start by tracing how Dune handles Coq builds and how coqchk accepts .vo library paths; done means Dune can trigger checking for built .vo files, with any intended incremental behavior defined and covered by tests.