Paolo Giarrusso (Aug 21 2023 at 12:51): Paolo Giarrusso (Aug 21 2023 at 12:51):https://proofassistants.stackexchange.com/questions/335/what-is-the-state-of-recompilation-avoidance-in-proof-assistants might be of interest to some — @Karl Palmskog comes to mind.
(I found this out from https://mathstodon.xyz/@kha@functional.cafe/110927336989796987 but it seems of more general interest).
Karl Palmskog (Aug 21 2023 at 14:06):in my view, "separate compilation"/"recompilation avoidance" is distinct from what one might call "incremental checking" in Coq. The latter is more similar to "retesting avoidance" (regression test selection) in software engineering
Karl Palmskog (Aug 21 2023 at 14:17):in Coq, there is of course the general confusion that comes from conflation of compile time and runtime
Karl Palmskog (Aug 21 2023 at 14:41):@Paolo Giarrusso if you want to take the lead to write a Coq reply on the PA SE, I can help, but I don't have enough cycles/motivation to write the whole thing myself. Also it might get downvoted due to citing a bunch of my own work
Paolo Giarrusso (Aug 21 2023 at 14:54):That's fine — I don't have enough cycles/motivation to _commit_ to it. I tagged you in part because I know you're the one who's done research on this :-)
As a complementary perspective, I understand the distinction but I'd draw another
Karl Palmskog (Aug 21 2023 at 14:56):at least at large companies like Google, they handle testing and compilation very differently, by different systems (if the last paper on this I saw is still accurate). I don't think they even call the testing part "building"
Karl Palmskog (Aug 21 2023 at 14:57):and potentially, Coq build processes might also do this: producing the binary files with precisely the non-Qed-ed terms separately from checking the Qeded proofs
Karl Palmskog (Aug 21 2023 at 15:00):don't know if you saw the build system (non-proof-assistant) formalizations by Mokhov et al:
Karl Palmskog (Aug 21 2023 at 15:12):I agree that making separate compilation possible is a nice thing to do semantically. SML didn't even specify compilation unit in the language definition, but the module system provided the basis for separate compilation
Karl Palmskog (Aug 21 2023 at 15:13):however, if someone can do competitive research on (practical) SML style module systems (improving on McQueen), then they're probably not going to hang around in the Coq Zulip since there are POPL/PLDI papers to be written
Paolo Giarrusso (Aug 21 2023 at 16:42):what one might call "incremental checking" in Coq
can you spell out what you mean? I thought I got you, but I can't make sense of your other comments
Paolo Giarrusso (Aug 21 2023 at 16:44):I'd want to avoid rerunning proof scripts if their dependencies didn't change, _and_ track dependencies at a smaller granularity than files. But then I don't want to skip just Qed-checking, but the entire proof search.
Paolo Giarrusso (Aug 21 2023 at 16:53):and sure, building binaries and testing them are different, but even after reading your comments, the entire process of building a .vo file remains building. It sounds like you disagree, but AFAICT you're leaving the reasons why as an exercise for the reader?
Paolo Giarrusso (Aug 21 2023 at 16:55):I guess you have some smart reason I fail to see; might be on me. Anyway, we're probably OT from the original question, so you should spend your time better than humoring me :-)
Karl Palmskog (Aug 21 2023 at 16:56):the whole .vo file tolchain thing is one of several possible ways to interact with Coq, we are typically not interested in producing a build artifact so much as getting the Coq checker to certify all our terms
Karl Palmskog (Aug 21 2023 at 16:57):if you only use the .vo toolchain via coqc, then sure, you've reduced everything to running a regular compilation/build process
Paolo Giarrusso (Aug 21 2023 at 17:42):maybe; I'll still need .vos for other reasons (browsing, development, building more proofs, etc). But until now, "whether we call it building or testing or FooBar" remains irrelevant to "how do we make FooBar faster"
Karl Palmskog (Aug 21 2023 at 17:46):I don't think the viewpoint of build-only vs. build+test is irrelevant to performance - if your view is that you have to produce .vo for everything, then this limits you a lot in how you can speed things up
Karl Palmskog (Aug 21 2023 at 17:49):on the other hand, if your view is something more general like: I have to get certification for all my terms+types by Coq's checker (regardless of .vo, regardless of any artifacts on filesystem), then there are a lot of fancy advanced things that can be done, like adapting regression testing techniques
Paolo Giarrusso (Aug 21 2023 at 18:04):That's an easier exercise for the reader, but _in principle_ the idea in https://par.nsf.gov/servlets/purl/10055461 3(a) applies to producing vo files as well.
Paolo Giarrusso (Aug 21 2023 at 18:11):of course _engineering_ that is far from trivial and I don't mean to minimize that — especially because back then Coq itself had no support for updating .vo files. But AFAICT, Emilio plans to do that with Flèche
Karl Palmskog (Aug 21 2023 at 18:22):let's say you can serialize the state of Flèche(+Coq) itself, then you could potentially just use that insert/delete what you need in the Flèche state each CI run and avoid .vo
Paolo Giarrusso (Aug 21 2023 at 18:22):but then with extra engineering I can also get .vo files, right?
Karl Palmskog (Aug 21 2023 at 18:23):I suppose so, but it's not obvious that they are always needed in full, in particular all the big Qeded terms
Paolo Giarrusso (Aug 21 2023 at 18:24):at bedrock we share the build cache from the server to local machines — today that needs .vo files, but I agree in principle you just need the info from .vos files
Paolo Giarrusso (Aug 21 2023 at 18:31):separately, checking the universe graph for consistency remains a global process in Coq (unlike Lean), and that requires more info than vo — you can omit qed bodies but you need their constraints. (I'm not sure how iCoq handles this; like the vos/vok workflow, I think the problem's relevant even when universe polymorphism isn't used). And coqchk needs the full .vos, tho running that is probably less common; you could try to incrementalize that as well, but that's likely to cause a TCB increase.
Karl Palmskog (Aug 21 2023 at 18:41):due to using .vio, iCoq didn't guarantee universe constraint checking (as described in paper) - I don't think .vos does either?
Paolo Giarrusso (Aug 21 2023 at 18:52):yep, same story
Patrick Nicodemus (Sep 04 2023 at 09:11):How does Isabelle do it? I know they don't produce an analogue of *.vo files, they just verify that the script to build the proof term is actually accepted by the type checker, but the proof term is ephemeral.
Karl Palmskog (Sep 04 2023 at 09:13):they have something called "proof promises" and use fine-grained threads provided by the Poly/ML compiler. Since proofs in HOL are entirely outside they system, they aren't even stored, so checking in isolation is even simpler than in Coq (also, no universe checking)
Karl Palmskog (Sep 04 2023 at 09:16):https://link.springer.com/chapter/10.1007/978-3-642-39634-2_30
Emilio Jesús Gallego Arias (Sep 14 2023 at 16:26):Thanks for the discussion and the link folks, indeed with Flèche we are trying to improve incremental checking greatly. As Andrey Mokhov put it, Flèche tries to be at the "intersection of a compiler and a build system". Already this provides some advantages, and IMHO many more to come. But incremental computing is hard !
@Patrick Nicodemus in addition to the proof promises, Isabelle has something called "Isabelle build", which is quite close to .vo files as it is based on heap dumps. I'm unsure how well that approach is documented tho.
Karl Palmskog (Sep 14 2023 at 17:51):HOL4 also uses heap dumps, they are part of the Poly/ML compiler. Not supported in OCaml, otherwise I guess they would be an option for Coq (this [lack of heap dumps in OCaml] is also arguably why Larry Paulson complained about usability of HOL Light on his blog)
Emilio Jesús Gallego Arias (Sep 14 2023 at 18:21):Coq could provide similar functionality to heap dumps, but this is an idea devs were not very friendly in the past.
I'd love to have a system like that, an in fact there is a coq-lsp branch that tries to do that, but the difficulties are documented in the TODO
Last updated: Nov 29 2023 at 21:01 UTC