Stream: Coq users

Topic: vos/vok and link-time universe check


view this post on Zulip Paolo Giarrusso (Oct 19 2021 at 21:26):

I understand that universe-checking isn't modular but whole world; but could it be done as a link-time check on the whole codebase? Naively, you might have to inspect generated proof terms, but you wouldn't need to rerun the proof search from scratch.

view this post on Zulip Paolo Giarrusso (Oct 19 2021 at 21:28):

say, _if_ vok contained proof terms (and I see it doesn't today), then (abstractly) this step would be very similar to running coqchk on the vok files.

view this post on Zulip Paolo Giarrusso (Oct 19 2021 at 21:29):

I'm sure this is a non-trivial engineering effort, and one could debate its usefulness — but is there some problem in principle?

view this post on Zulip Gaëtan Gilbert (Oct 19 2021 at 21:30):

_if_ vok contained proof terms

that would amount to allowing to load .vos when generating .vo
which is fine as long as you know about the universe caveat imo

view this post on Zulip Gaëtan Gilbert (Oct 19 2021 at 21:31):

we could also imagine dumping just universes in .vok and having something to check global consistency

view this post on Zulip Paolo Giarrusso (Oct 19 2021 at 21:33):

yes — and I mention coqchk because I know its performance is very acceptable :-)

view this post on Zulip Paolo Giarrusso (Oct 19 2021 at 21:34):

there's extra work generating universes of course, but in this "back-of-the-envelope" view, how bad could is possibly be? (j/k, everything I hear on universes is pain)

view this post on Zulip Enrico Tassi (Oct 20 2021 at 05:48):

you want a middle ground between vio and vos/vok... am I reading this right?

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 07:51):

@Enrico Tassi Not sure, but I’d like the global link-time check (not available in the vio->vo path), and I’d like building voks to not destroy information — I guess that was an optimization, but the global check seems a better one if it saves starting over to check universes.

But I know the problem better than the solution — a large codebase where universe inconsistencies seem easy enough to trigger; deferring universe checking to a nightly build seems possible but risky (and maybe we should anyway). Also, our builds spend long on proof search, and redoing that to check universes seems… suboptimal.

So, as a way to get fast parallel builds, it could be useful to have the extra parallelism of vio/vos/… builds, but the same guarantees about universe consistency checking as normal builds.

Side note: before much happens, we should probably start using coqchk — I hope _that_ can be left for nightly. If not, a solution would need to produce vo files that pass coqchk, which seems even harder.

view this post on Zulip Enrico Tassi (Oct 20 2021 at 07:55):

if you vio->vo all files and then Require them all from coqtop, you get your global check on universes.

view this post on Zulip Enrico Tassi (Oct 20 2021 at 07:56):

but this had the drawback of large .vio files, which .vos/vok does not have (but does not store universes either).

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 08:00):

right, so let’s skip the vio — but one could get vos or something vo-like from vos files I guess, without at least the problem of large vio files?

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 08:00):

(okay, I see that’s a sort-of middle ground)

view this post on Zulip Enrico Tassi (Oct 20 2021 at 08:14):

yes, the "easy" thing is to get the .vok contain universes (currently they are empty, IIRC), and then load all of them (not as .vo, but us universe constraints). I believe this would not be super hard to code.

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 08:19):

and to be sure, it’d also be easy to get “full vo”s in vok files I suppose? or is there some challenge?

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 08:21):

OTOH, I bet those vos are different so they wouldn’t pass coqchk as-is — and “fixing them” later would require extra work that might not be worth it.

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 08:23):

Anyway, thanks; I now have some thinking to do on this :-)

view this post on Zulip Gaëtan Gilbert (Oct 20 2021 at 08:30):

it would be very easy to expose a flag -load-vos to coqc, then instead of calling coqc -vok you call coqc -load-vos, it will run the same proofs but produce a .vo that you can check with coqchk
build system support is more complicated

view this post on Zulip Enrico Tassi (Oct 20 2021 at 09:35):

Paolo Giarrusso said:

and to be sure, it’d also be easy to get “full vo”s in vok files I suppose? or is there some challenge?

Yes, but they won't be generated in an env that transitively contains all the universes. So in some corner cases these full vo would be "different".
A tactic can take two different paths depending on a type checking error, which in turn may depend solely on universes...

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 13:56):

The last one is a very good point.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 13:58):

There is a (somewhat artificial) two-liner that creates defines a boolean whose actual value depends on the humour of the STM scheduler. I think I posted it on an issue once.

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 13:58):

If you believe that Coq should approach separate compilation, you could argue that universe checks should really be link-time checks, which should really happen at link time, and the tactic should not backtrack on universe errors, so they should be postponed at least to Qed. Of course that adds errors, but finding the universe inconsistency earlier might be good.

view this post on Zulip Gaëtan Gilbert (Oct 20 2021 at 13:59):

typically things like https://github.com/coq/coq/issues/15049 (if the constraint came from a Qed proof instead of a Constraint command)

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 13:59):

I started designing a way to hide as much as possible the set of Qed-local constraints.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 14:00):

I suspect that most of the time they're 100% local.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 14:00):

and we could warn when this is not the case.

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 14:00):

BTW, I’m not sure I fully buy the argument I just made, but it seems what follows naturally from a certain design.

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 14:01):

@Pierre-Marie Pédrot I’m not familiar with qed-local constraints; do you have pointers to learn about them?

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 15:37):

I see, those are the constraints generated by opaque bodies and missing from .vos files.


Last updated: Sep 23 2023 at 15:01 UTC