Slowness in compiling the library #8
Comments
|
How do bare projections slow things down? And don't you have to use each bare projection at least once, to define the corresponding unbare ones? |
|
Whenever you use something like |
|
Thanks for the link to the paper! I looked at 2.3 and 2.5, so it seems I On Sun, Jan 19, 2014 at 4:18 PM, Jason Gross [email protected]:
|
|
For example, in the Definition eta3_sigma `{P : forall (a : A) (b : B a) (c : C a b), Type}
(u : sigT (fun a => sigT (fun b => sigT (P a b))))
: (u.1; (u.2.1; (u.2.2.1; u.2.2.2))) = u
:= match u with existT x (existT y (existT z w)) => 1 end.is sometimes an order of magnitude or more faster than regenerating the same proof term on the fly with specific types and arguments filled in---and the definition of |
|
You might also be interested about my brain-dump about speed in Coq at HoTT/Coq-HoTT#157 (comment). |
|
Re: "If you Set Printing All and Print PullbackArrow_PullbackPr2, you will see a giant term. " You were right, and wc showed it had 291000 words in it! I think I have to understand that better. I'll experiment... |
|
precomp_ess_surj contains a quite lengthy proof which I am not going to refactor; also, since it proves an hprop, one can savely opacify it and forget about it. Nonetheless, your measurements will help to identify bottlenecks and thus to improve on speed, so thanks a lot! |
|
By the way, one can't always be totally comfortable with tacking a Qed on the end of a proof -- the statement of PullbackArrow_PullbackPr2 itself has up to 4 nested projections, and applying the lemma to arguments might result in a gigantic term, momentarily. I suppose. |
|
Hmm, I find nothing conceptually simple about a term like (pr2 (pr2 (pr1 (pr2 (pr2 Pb) e h k H)))) appearing in a proof. Who can read that? |
Only if you need to unfold it. If you don't unfold it, Coq doesn't care how big it really is, because it's hidden. And
To me, it says "there's nothing deep going on here, I'm just defining a projection of |
|
Can someone please post the same table for 8.3? On Jan 19, 2014, at 3:58 PM, Jason Gross [email protected] wrote:
|
|
I get this: 25.37 (v8.4) limits/pullbacks 23.56 (v8.3) limits/pullbacks |
|
Is there a similarly detailed measurement for Foundations? On 01/22/2014 03:39 PM, Daniel R. Grayson wrote:
|
|
89.66 (v8.4) hlevel2/algebra1d 14.26 (v8.3) hlevel2/hq |
|
If you are interested, you can pass |
|
I was wondering how you did that -- under Mac OS X, GNU time is not On Wed, Jan 22, 2014 at 11:40 AM, Jason Gross [email protected]:
|
|
I got the trick from trunk's |
|
Thanks, that's very interesting:
Some files in Foundations take 10 times longer (hSet, algebra1d). It On 01/22/2014 05:06 PM, Daniel R. Grayson wrote:
|
|
The trunk version of Coq has a |
|
I happen to have a patched version of the trunk so we can try that out. On Wed, Jan 22, 2014 at 3:10 PM, Jason Gross [email protected]:
|
|
I think it's Set Asymmetric Patterns? -Jason
|
|
The -time option works, and produces tons of output like this: |
|
You can pipe it through |
|
Or just pipe it through |
|
Here are the top ten offenders: |
|
Is |
|
I think I'll work on the big guys first. Often I find that apply in 8.4 is On Wed, Jan 22, 2014 at 9:05 PM, Jason Gross [email protected]:
|
|
I got the two big guys, but using "exact" on idpath didn't help (yet): |
|
That cuts algebra1d from 90 seconds to 28.25 sec, 1782857728 bytes: hlevel2/algebra1d |
|
On 01/23/2014 06:34 AM, Daniel R. Grayson wrote:
Awesome. |
|
Compile from scratch with make COQTIME=yes first. On Thu, Jan 23, 2014 at 10:58 AM, benediktahrens
|
|
And use the patched coq trunk you'll find in my "coq" repository, which On Thu, Jan 23, 2014 at 11:48 AM, Daniel R. Grayson [email protected]:
|
|
Thanks. Is the native code compilation responsible for that increase in : compiling hlevel2/algebra1b.v ; >hlevel2/algebra1b.timing \time -f "%U Is there a way to turn that off, by any chance? On 01/23/2014 05:52 PM, Daniel R. Grayson wrote:
|
|
Did you pass |
|
Commit 98cc2f0 introduces an |
|
It's weird, because I should be able to choose when compiling the Coq On 01/23/2014 07:05 PM, Jason Gross wrote:
|
|
There might also be an option to pass to coqc, but I've had the problems when compiling the stdlib, so always pass my arguments to ./configure. |
|
" This seems to me to be the main question, or with typechecking rather |
|
Qed instead of Opaque speeds Foundations up by 33%, see DanGrayson/Foundations2@21de280 |
|
Native code compilation adds 20% to the time, and turning it off prevents an anomaly when compiling my K-theory stuff. |
|
The option for coqc is called -no-native-compiler. |
|
Dan, did you send this to Matthieu? V. On Jan 22, 2014, at 11:06 AM, Daniel R. Grayson [email protected] wrote:
|
|
On Jan 23, 2014, at 12:34 AM, Daniel R. Grayson [email protected] wrote:
what is the number 178.... about? V. |
|
It is great for now, but I am uncomfortable with the amount of hacking which one needs to apply where the system should work without any. V. On Jan 23, 2014, at 4:54 AM, benediktahrens [email protected] wrote:
|
|
There were no Qed's. Opaques were added to Defined's. Qed's are not good because there are proofs where I use "transparent" on constants which have been opaqued and this does not work with things which have been qed'ed. V. On Jan 23, 2014, at 8:55 AM, Daniel R. Grayson [email protected] wrote:
|
|
On Jan 23, 2014, at 9:21 AM, benediktahrens [email protected] wrote:
I am not sure that this has been intended. May be "Global Opaque" is Ok. But again, I do not think that it is a good idea to hck the library when the fault is with Coq. V. |
|
Why do you call Qed'ing lemmas "hacking"? I agree that the performance regression from 8.3 to 8.4 is worrying, and But I think that opacifying some stuff in Foundations will be On 01/24/2014 01:23 PM, Vladimir Voevodsky wrote:
|
|
Yes, the two constants you use Transparent with were left alone. And it's On Fri, Jan 24, 2014 at 7:21 AM, Vladimir Voevodsky <
|
|
It's the number of bytes of memory used by coq. On Fri, Jan 24, 2014 at 5:08 AM, Vladimir Voevodsky <
|
|
On Jan 23, 2014, at 1:21 PM, benediktahrens [email protected] wrote:
Why? The projection from, for example, commring to UU is much longer. V. |
|
On 01/24/2014 02:25 PM, Vladimir Voevodsky wrote:
What I really meant was that literally chaining many pr{1,2}'s is too E.g. Definition foo := pr1 (pr2 (pr2 (pr1 (pr2 b))))) will take long whereas Definition bar b := pr2 (pr1 (pr2 b))) will give acceptable compile times. Since commrng is built "in stages", the projection from commrng to UU |
|
No, I didn't send it to him, but feel free to do so. On Fri, Jan 24, 2014 at 4:27 AM, Vladimir Voevodsky <
|
|
On Jan 24, 2014, at 8:21 AM, Daniel R. Grayson [email protected] wrote:
For our experimental work with the library it's Ok. But what about someone who wants to use the library without changing it (which is the way libraries are supposed to be used)? V. |
|
That's a good point, which I didn't consider. Perhaps I should undo it. On Fri, Jan 24, 2014 at 8:46 AM, Vladimir Voevodsky <
|
|
On 01/24/2014 03:08 PM, Daniel R. Grayson wrote:
RezkCompletion does not use any of the files in which you have replaced It might be good to ask how HoTT is handling the issue. @JasonGross, are I think there is a range of lemmas which can safely be closed by Qed, |
|
I think the perspective of HoTT/HoTT (at least, my perspective) is that we are a long way from being able to build a library that most users can use without modification -- the whole project is still an experiment -- so we have no problem with switching Defineds and Qeds around as needed by users. I think the default is to Defined everything unless Qed seems to produce a significant speedup for some things. |
|
I follow a slightly different approach to the category theory contributions I've been making to HoTT/HoTT: Defined for everything that isn't an hProp, and for the hProps that are expected to sometimes reduce to refl (e.g., in composition of functors). Qed (rather, |
|
It seems that gradth in Vladimir's u00 would be made Qed by your recipe, On Fri, Jan 24, 2014 at 3:02 PM, Jason Gross [email protected]:
|
|
Ah, I should specify that the only hProps that I tend to encounter in the category theory stuff are proofs of equality and proofs of truncation. Even so, I sometimes need the proofs of equality to be partially transparent, because, for example, I need to remove instances of funext and play some other tricks to pull refls out of them. So I guess my rule isn't so hard and fast. My guess is that my inclination would be to make the inverse transparent, but the rest of the proof terms opaque (the section, retraction, adjointifcation coherence) opaque. |
|
On Jan 24, 2014, at 9:08 AM, Daniel R. Grayson [email protected] wrote:
I thought about it when I worked on Foundations and could not come up with any useful criterion. V. |
When I compile the library with Coq 8.4 and time how long it takes to make each file, I get
(Admittedly, the HoTT library takes around three times as long, and I don't have a good sense of how complicated the constructions in
precomp_ess_surjandlimits/pullbacks.)At least a third of the time in
limits/pullbacks, probably much more, is spent checking trivial lemmas which are slow due to nested sigma types. It's plausible that Matthieu's polyproj branch fixes this, but if you're interested in fixing it before that lands for 8.5, you can replace nested sigmas with records (or, possibly just define custom projections for each nested sigma, so that you never use the bare projections from a sigma type).The text was updated successfully, but these errors were encountered: