Handle coqchk error minimization

[JasonGross]

ci-hott was not minimized because no error message was found (fair enough it's in coqchk)

Hm, I guess this is an interesting case (in two ways). With regards to this PR, do we expect that a file can pass coqc but fail coqchk?

And regarding minimizing coqchk invocations... I'll have to think about this one. Do you think coqchk could be made to emit location information about the constant that its failing on? Then I could set up the minimizer to handle calling coqc followed by coqchk.

Originally posted by @JasonGross in coq/coq#16967 (comment)

[SkySkimmer]

coqchk already says something like "check foo.bar.baz" if invoked with sufficiently verbose flags (I don't remember if it's the default)
It has no more information available to print.

[JasonGross]

Is there location information in .vo files where constants have line numbers?

In any case, can it at least specify which part of the constant is the dirpath? Ideally it could also print the file name, which it should be able to do because it needs to load the vo files from disk.

[SkySkimmer]

you can look eg at https://gitlab.com/coq/coq/-/jobs/3460867582 to see what it says
https://gitlab.com/coq/coq/-/jobs/3460867582#L1269

Checking library: Coq.Structures.Equalities
checking module: Coq.Structures.Equalities
checking module type: Coq.Structures.Equalities.Nop
checking module type: Coq.Structures.Equalities.Typ
checking cst:Coq.Structures.Equalities.Typ.t