Skip to content

WIP: Make `make quick` make quickly.

Janno requested to merge janno/quick-make-quick into master

I am not sure if you guys are interested in this. I got a bit fed up by the compilation times so I used sed to put these annotations in (with only a few manual ones needed). This is quick and dirty. (Pun intended.)

Coq 8.5pl2 still hangs on the barrier_client.v file because some value is not available in the right process at the right time. The value is probably still in Memphis. Because of reasons, make quick decides to deal with this by not terminating. Coq 8.6beta1 powers through without problems.

On my laptop (4 cores) with 8.6beta1make quick takes pretty much exactly 2 minutes.

The files in prelude use sections in ways that require insane amounts of manual annotation and therefore they are not covered by this patch. They make up 40-50% of the time taken by make quick. So with some extra work the entire duration could probably go down to 1:30.

An alternative approach to my changeset would be to put one Default Proof Using at the top of every file. I didn't think about that before I wrote this request. (For those interested: They are not exported unless you prefix them with "Global".)

The branch also contains some Collections which might not be necessary. I couldn't figure out why it didn't work when I wrote the variables directly into Set Default Proof Using.

Merge request reports