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/@firstname.lastname@example.org/110927336989796987 but it seems of more general interest).
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
in Coq, there is of course the general confusion that comes from conflation of compile time and runtime
@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
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
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"
and potentially, Coq build processes might also do this: producing the binary files with precisely the non-
Qed-ed terms separately from checking the
don't know if you saw the build system (non-proof-assistant) formalizations by Mokhov et al:
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
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
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
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.
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?
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 :-)
.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
if you only use the
.vo toolchain via
coqc, then sure, you've reduced everything to running a regular compilation/build process
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"
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
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
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.
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
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
but then with extra engineering I can also get
.vo files, right?
I suppose so, but it's not obvious that they are always needed in full, in particular all the big
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
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.
due to using
.vio, iCoq didn't guarantee universe constraint checking (as described in paper) - I don't think
.vos does either?
yep, same story
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.
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)
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.
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)
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