Paolo Giarrusso (Oct 19 2021 at 21:26): 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.
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.
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?
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
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
Paolo Giarrusso (Oct 19 2021 at 21:33):yes — and I mention coqchk because I know its performance is very acceptable :-)
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)
Enrico Tassi (Oct 20 2021 at 05:48):you want a middle ground between vio and vos/vok... am I reading this right?
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.
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.
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).
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?
Paolo Giarrusso (Oct 20 2021 at 08:00):(okay, I see that’s a sort-of middle ground)
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.
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?
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.
Paolo Giarrusso (Oct 20 2021 at 08:23):Anyway, thanks; I now have some thinking to do on this :-)
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
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
vokfiles 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...
Paolo Giarrusso (Oct 20 2021 at 13:56):The last one is a very good point.
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.
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.
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)
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.
Pierre-Marie Pédrot (Oct 20 2021 at 14:00):I suspect that most of the time they're 100% local.
Pierre-Marie Pédrot (Oct 20 2021 at 14:00):and we could warn when this is not the case.
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.
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?
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: Oct 13 2024 at 01:02 UTC