I am playing around with the standard library (in particular Reals).
My questions are the following:
Is compilation time of .v
files an issue ?
I would say yes, for instance Rineq.v
takes a long time to be checked in coqide. But is there a general agreement around this question ?
If the answer is yes, are there good practice related to this point ? Do the following tactics take significantly more time than, say, using manual rewrites and applys with unification ?
easy
or ; try easy
ring
, field
, ...auto
, auto with reals
, ...lia
, lra
we investigated compilation times for several Coq projects empirically, with and without parallelism and selection of files/proofs here. One takeaway is that far from all projects have a compilation time issue, and those that do have many options available to them (e.g., reorganize project files, use different proof automation). But since Coq has an extremely wide range of use cases and approaches to proof automation, compilation/checking times will likely never stop being a problem for some projects.
however, in conventional small projects, the choice of auto
vs. lia
vs. ring
is almost never an issue for performance. You may run into issues with structure inference long before those become the bottleneck, e.g., https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html
ah, I should mention that Jason Gross's PhD thesis is probably the most recent detailed account of Coq performance, especially w.r.t. proof automation.
Using the Time
command and the time
tactical might also help getting a (very rough!) first idea of what's expensive — which varies across projects.
personally, I've seen both (setoid) rewriting and unification diverge much more easily than e.g. lia
. auto
uses exponential proof search, but its default search depth is only 5, and it doesn't try applying hints that are expensive to unify with the goal
Thank you for the very nice information and the pointers. Compiling with coqc -time
showed that it was actually quite fast. What is not is interpreting the file in coqide
. Is it because coqide
uses another interpretor ?
In CoqIDE, every sentence you check usually needs to be sent individually to the background Coq process. There's significant overhead both due to this and all the general GUI components.
I think coq-lsp and the in-progress VsCoq2 are both trying to lift some of the performance issues in GUI-Coq communication. But I think those improvements are not likely to make it to CoqIDE in the near future.
@Karl Palmskog : Doesn't the "interpret to cursor" function in CoqIDE and VsCoq solve this in a satisfactory way? I think it is quite reasonable, especially because it allows to enter a proof before it finished checking the upstream proofs.
I can live quite well with this.
@Michael Soegtrop I don't think it does if you have a file with 3000+ lines of code, which is actually fairly common.
but I haven't done the numbers at GUI level, because it's not really such an interesting use case to me (there's a ton more resources to save in optimizing a batch CI workflow)
@Karl Palmskog : if I have a long file and do "goto cursor" it parses the file - which takes a few seconds - then immediately enters the current proof and processes it until the cursor and does all upstream proofs in the back ground. So it does usually not much depend on the length of the file (except for the parsing) but on the length of the proof one enters.
but this only works if you use Proof using
annotations, right? If you don't process definitions before the proof in the file, how could you even get a proof state (assuming the proof depends on some definition there)? And most projects don't have Proof using
annotations but still use sections.
to my knowledge, the only unit we can safely process asynchronously are Qed
-terminated lemmas with Proof using
annotations (and even this doesn't check universe constraints)
_if_ you use sections (which many some don't), you indeed need Proof using.
or Set Default Proof Using
+ Proof.
corrected: I trust your estimate on projects better, but I think many Coq users don't use sections (for instance, I haven't seen then in SF)
we did actually check in 2018 or so how many projects on GitHub could use async directly
from memory, I think it was something like 20% (that didn't use sections, etc.), but I'll try to find the figure
Additionally, when surveying 260 publicly available Coq projects on GitHub, each with more than 10k lines of code (LOC), we found that ∼20% of these projects can also leverage fine-grained parallel proof checking, two years after support was added to Coq.
@Karl Palmskog : if one doesn't use sections, the using
annotations are not required. I am more using modules than sections, so I don't have this issue.
also, another issue we saw was that the overhead of asynch is significant for small lemmas. So if you set up a bunch of workers for your GUI and do asynch proofs for a lot of small lemmas as you step through, it's actually going to be much slower in proof time than if you proved top-to-bottom. But, sure, you gain in interactivity, since you can edit your proof right away.
the best thing to do is probably to have several pools of workers, so you can run par
and stuff like that even when other workers do all that async busywork.
at least in VsCoq, more async workers don't feel so much faster
sure, but that's because I think they go in a single pool (possibly with a separate top-level process)
I think there are only a few projects that can get a big speedup from async proofs with lots of workers (mostly due to overheads for short proofs)
without dune, .aux
files could make it better since Coq would _know_ which proofs are short? But with dune + caching, I think we lack a good way to cache .aux
files since they're not reproducible, so these days .aux
files are not cached, and are probably discarded
it's not obvious what you would actually do with all the .aux
data in the GUI setting. In CI setting, you could probably at least do some good estimates when something is worth doing asynchronously or using .vos
or using regular .vo
, etc.
I think the "Google testing workflow", where everything is actually checked in CI with fast turnaround, and users basically only check some local work before submitting, is likely the way to handle large projects. One could go all in on .vos
locally.
is it even possible in CoqIDE and/or VsCoq to just not build/check proofs at all?
The overhead of async is visible, hopefully smaller on unix in vscoq 2. But I think you are looking at the wrong measure, the whole point is to make it fast to "go to point", not to check what was postponed.
Of course it would be nice to be just faster...
but in a more sophisticated workflow involving CI, why would you check anything at all on your way "to point"?
you could just trust whatever you check out, and that everything you commit will only be accepted once fully checked
I think we were focusing on checking everything to point above because this was what the original question was about
even with CI, you're often working with code that didn't pass CI: you made changes and want to see what breaks
if I change a definition in a file, I want to recheck the theory right away — and unless your client has _much_ worse single-core performance, CI is at best as fast as my laptop (and that lower bound is hard to reach).
IMO .vos up to your file, then async is what you ask for.
In any case, it would be nice to list these scenarios, so that tuning in vscoq 2 can allow for them. I guess we all know the limitations.
Sorry if it was mentioned before, but CoqIDE spends most of its time printing goals when you have a slow step.
Last updated: Oct 13 2024 at 01:02 UTC