Stream: Coq users

Topic: Cost of automatic tactics during compilation


view this post on Zulip Pierre Rousselin (Dec 18 2022 at 13:15):

I am playing around with the standard library (in particular Reals).
My questions are the following:

view this post on Zulip Karl Palmskog (Dec 18 2022 at 13:24):

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.

view this post on Zulip Karl Palmskog (Dec 18 2022 at 13:27):

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

view this post on Zulip Karl Palmskog (Dec 18 2022 at 14:50):

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.

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 06:54):

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.

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 07:02):

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

view this post on Zulip Pierre Rousselin (Dec 19 2022 at 10:08):

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 ?

view this post on Zulip Karl Palmskog (Dec 19 2022 at 10:10):

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.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 10:13):

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.

view this post on Zulip Michael Soegtrop (Dec 19 2022 at 10:17):

@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.

view this post on Zulip Michael Soegtrop (Dec 19 2022 at 10:17):

I can live quite well with this.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 10:19):

@Michael Soegtrop I don't think it does if you have a file with 3000+ lines of code, which is actually fairly common.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 10:20):

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)

view this post on Zulip Michael Soegtrop (Dec 19 2022 at 11:20):

@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.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 11:26):

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.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 11:30):

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)

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 12:10):

_if_ you use sections (which many some don't), you indeed need Proof using. or Set Default Proof Using + Proof.

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 12:11):

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)

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:11):

we did actually check in 2018 or so how many projects on GitHub could use async directly

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:13):

from memory, I think it was something like 20% (that didn't use sections, etc.), but I'll try to find the figure

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:15):

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.

view this post on Zulip Michael Soegtrop (Dec 19 2022 at 12:19):

@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.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:23):

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.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:24):

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.

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 12:30):

at least in VsCoq, more async workers don't feel so much faster

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:33):

sure, but that's because I think they go in a single pool (possibly with a separate top-level process)

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:35):

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)

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 12:37):

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

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:41):

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.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:45):

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 .voslocally.

view this post on Zulip Karl Palmskog (Dec 19 2022 at 12:51):

is it even possible in CoqIDE and/or VsCoq to just not build/check proofs at all?

view this post on Zulip Enrico Tassi (Dec 19 2022 at 13:09):

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.

view this post on Zulip Enrico Tassi (Dec 19 2022 at 13:10):

Of course it would be nice to be just faster...

view this post on Zulip Karl Palmskog (Dec 19 2022 at 13:24):

but in a more sophisticated workflow involving CI, why would you check anything at all on your way "to point"?

view this post on Zulip Karl Palmskog (Dec 19 2022 at 13:25):

you could just trust whatever you check out, and that everything you commit will only be accepted once fully checked

view this post on Zulip Karl Palmskog (Dec 19 2022 at 13:26):

I think we were focusing on checking everything to point above because this was what the original question was about

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 14:06):

even with CI, you're often working with code that didn't pass CI: you made changes and want to see what breaks

view this post on Zulip Paolo Giarrusso (Dec 19 2022 at 14:09):

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).

view this post on Zulip Enrico Tassi (Dec 19 2022 at 14:11):

IMO .vos up to your file, then async is what you ask for.

view this post on Zulip Enrico Tassi (Dec 19 2022 at 14:12):

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.

view this post on Zulip Ali Caglayan (Dec 25 2022 at 13:41):

Sorry if it was mentioned before, but CoqIDE spends most of its time printing goals when you have a slow step.


Last updated: Mar 28 2024 at 22:01 UTC