Slowness in compiling the library

[JasonGross]

When I compile the library with Coq 8.4 and time how long it takes to make each file, I get

0.10    pathnotations
0.17    topos/epis_monos
0.18    limits/terminal
0.20    limits/initial
0.21    HLevel_n_is_of_hlevel_Sn
0.24    limits/aux_lemmas_HoTT
0.31    category_hset
0.43    whiskering
0.46    auxiliary_lemmas_HoTT
0.70    rezk_completion
0.86    precategories
1.03    yoneda
1.12    limits/cones
1.12    sub_precategories
4.71    equivalences
6.99    functors_transformations
9.29    precomp_fully_faithful
32.22   precomp_ess_surj
69.37   limits/pullbacks

(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_surj and limits/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).

[vladimirias]

On Jan 23, 2014, at 12:34 AM, Daniel R. Grayson notifications@github.com wrote:

That cuts algebra1d from 90 seconds to

28.25 sec, 1782857728 bytes: hlevel2/algebra1d

what is the number 178.... about?

V.

[vladimirias]

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 notifications@github.com wrote:

On 01/23/2014 06:34 AM, Daniel R. Grayson wrote:

That cuts algebra1d from 90 seconds to

28.25 sec, 1782857728 bytes: hlevel2/algebra1d

Awesome. Would it make sense to try with opacified versions of some of the lemmas? — Reply to this email directly or view it on GitHub.

[vladimirias]

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 notifications@github.com wrote:

At some point Vladimir must have replaced a lot of Qed's with Opaque's, but I hear that isn't as good. If you think so, too, I could just try reverting all of those.

On Thu, Jan 23, 2014 at 4:54 AM, benediktahrens notifications@github.comwrote:

On 01/23/2014 06:34 AM, Daniel R. Grayson wrote:

That cuts algebra1d from 90 seconds to

28.25 sec, 1782857728 bytes: hlevel2/algebra1d

Awesome. Would it make sense to try with opacified versions of some of the lemmas?

— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33110099 .

— Reply to this email directly or view it on GitHub.

[vladimirias]

On Jan 23, 2014, at 9:21 AM, benediktahrens notifications@github.com wrote:

From the description on http://coq.inria.fr/distrib/current/refman/Reference-Manual008.html#hevea_default447 it seems that Opaque renders opaque from a user point of view, but not (completely) from the type-checking point of view.

Also, and maybe more importantly, "The scope of Opaque is limited to the current section, or current file, unless the variant Global Opaque qualid1 … qualidn is used." So all the Opaque commands in early algebra files are not retained in the later ones.

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.

[benediktahrens]

Why do you call Qed'ing lemmas "hacking"? From what I understand, we use Qed basically to avoid that terms which have already been typechecked (when they were defined) get unfolded later when being used and thus have to be typechecked again.

I agree that the performance regression from 8.3 to 8.4 is worrying, and that Qed'ing is not a replacement for finding the reason for the regression.

But I think that opacifying some stuff in Foundations will be unavoidable in the long run, when more mathematics is built upon it, in order to avoid an explosion in the size of terms. And for this it is not clear to me whether "Global Opaque" is sufficient, because I don't know where this option is respected and where it isn't. If we want to rely on it, we should have some Coq developer explain its functionality to us and know if its features are supposed to change in the future.

On 01/24/2014 01:23 PM, Vladimir Voevodsky 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.

[DanGrayson]

Yes, the two constants you use Transparent with were left alone. And it's easy enough to revert if you want to do it with another.

On Fri, Jan 24, 2014 at 7:21 AM, Vladimir Voevodsky < notifications@github.com> 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 notifications@github.com wrote:

At some point Vladimir must have replaced a lot of Qed's with Opaque's, but I hear that isn't as good. If you think so, too, I could just try reverting all of those.

On Thu, Jan 23, 2014 at 4:54 AM, benediktahrens < notifications@github.com>wrote:

On 01/23/2014 06:34 AM, Daniel R. Grayson wrote:

That cuts algebra1d from 90 seconds to

28.25 sec, 1782857728 bytes: hlevel2/algebra1d

Awesome. Would it make sense to try with opacified versions of some of the lemmas?

— Reply to this email directly or view it on GitHub< https://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33110099>

.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33218544 .

[DanGrayson]

It's the number of bytes of memory used by coq.

On Fri, Jan 24, 2014 at 5:08 AM, Vladimir Voevodsky < notifications@github.com> wrote:

On Jan 23, 2014, at 12:34 AM, Daniel R. Grayson notifications@github.com wrote:

That cuts algebra1d from 90 seconds to

28.25 sec, 1782857728 bytes: hlevel2/algebra1d

what is the number 178.... about?

V.

— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33210972 .

[vladimirias]

On Jan 23, 2014, at 1:21 PM, benediktahrens notifications@github.com wrote:

Commit 98cc2f0784eef764063f3c794352db26872a952b introduces an intermediate projection for pullback, thus reducing the compile time significantly. I guess that as a rule of thumb, one should not compose more than two or three pr{1,2}'s.

Why? The projection from, for example, commring to UU is much longer.

V.

[benediktahrens]

On 01/24/2014 02:25 PM, Vladimir Voevodsky wrote:

On Jan 23, 2014, at 1:21 PM, benediktahrens notifications@github.com wrote:

Commit 98cc2f0784eef764063f3c794352db26872a952b introduces an intermediate projection for pullback, thus reducing the compile time significantly. I guess that as a rule of thumb, one should not compose more than two or three pr{1,2}'s.

Why? The projection from, for example, commring to UU is much longer.

What I really meant was that literally chaining many pr{1,2}'s is too slow, as Jason also mentioned earlier in this thread.

E.g.

Definition foo := pr1 (pr2 (pr2 (pr1 (pr2 b)))))

will take long whereas

Definition bar b := pr2 (pr1 (pr2 b))) Definition foo' := pr1 (pr2 (bar b))

will give acceptable compile times.

Since commrng is built "in stages", the projection from commrng to UU looks like the second example.

[DanGrayson]

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 < notifications@github.com> wrote:

Dan,

did you send this to Matthieu?

V.

On Jan 22, 2014, at 11:06 AM, Daniel R. Grayson notifications@github.com wrote:

89.66 (v8.4) hlevel2/algebra1d 46.61 (v8.4) hlevel2/algebra1b 29.90 (v8.4) hlevel2/algebra1c 26.38 (v8.4) Generalities/uu0 17.76 (v8.4) hlevel2/hq 9.24 (v8.4) hlevel2/hSet 6.51 (v8.4) hlevel2/hz 4.75 (v8.4) hlevel2/finitesets 1.01 (v8.4) hlevel2/algebra1a 0.70 (v8.4) hlevel2/hnat 0.49 (v8.4) hlevel2/stnfsets 0.17 (v8.4) hlevel1/hProp 0.14 (v8.4) Proof_of_Extensionality/funextfun 0.08 (v8.4) Generalities/uuu

14.26 (v8.3) hlevel2/hq 10.73 (v8.3) hlevel2/algebra1c 9.26 (v8.3) Generalities/uu0 7.65 (v8.3) hlevel2/algebra1b 7.09 (v8.3) hlevel2/hz 6.45 (v8.3) hlevel2/algebra1d 3.07 (v8.3) hlevel2/finitesets 0.98 (v8.3) hlevel2/hSet 0.95 (v8.3) hlevel2/algebra1a 0.63 (v8.3) hlevel2/hnat 0.45 (v8.3) hlevel2/stnfsets 0.14 (v8.3) hlevel1/hProp 0.10 (v8.3) Proof_of_Extensionality/funextfun 0.06 (v8.3) Generalities/uuu

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33208421 .

[vladimirias]

On Jan 24, 2014, at 8:21 AM, Daniel R. Grayson notifications@github.com wrote:

Yes, the two constants you use Transparent with were left alone. And it's easy enough to revert if you want to do it with another.

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.

[DanGrayson]

That's a good point, which I didn't consider. Perhaps I should undo it. Is there any class of theorems that we could be certain would never need unfolding? Benedikt, what about that point for your library?

On Fri, Jan 24, 2014 at 8:46 AM, Vladimir Voevodsky < notifications@github.com> wrote:

On Jan 24, 2014, at 8:21 AM, Daniel R. Grayson notifications@github.com wrote:

Yes, the two constants you use Transparent with were left alone. And it's easy enough to revert if you want to do it with another.

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.

— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33223423 .

[benediktahrens]

On 01/24/2014 03:08 PM, Daniel R. Grayson wrote:

That's a good point, which I didn't consider. Perhaps I should undo it. Is there any class of theorems that we could be certain would never need unfolding? Benedikt, what about that point for your library?

RezkCompletion does not use any of the files in which you have replaced Opaque by Qed.

It might be good to ask how HoTT is handling the issue. @JasonGross, are there any guidelines for contributions to HoTT concerning this question?

I think there is a range of lemmas which can safely be closed by Qed, such as any isofhlevel lemma, and in general many hprops. But we should also not be afraid of getting it wrong: when people stumble upon an opaque thing they need transparent, they can file an issue.

[mikeshulman]

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.

[JasonGross]

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, abstract) for the rest of the hProps.

[DanGrayson]

It seems that gradth in Vladimir's u00 would be made Qed by your recipe, since it returns isweq f, but that breaks later code, probably because the proof needs to be unfolded to produce the inverse of f later on.

On Fri, Jan 24, 2014 at 3:02 PM, Jason Gross notifications@github.comwrote:

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, abstract) for the rest of the hProps.

— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/8#issuecomment-33255686 .

[JasonGross]

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.

[vladimirias]

On Jan 24, 2014, at 9:08 AM, Daniel R. Grayson notifications@github.com wrote:

That's a good point, which I didn't consider. Perhaps I should undo it. Is there any class of theorems that we could be certain would never need unfolding?

I thought about it when I worked on Foundations and could not come up with any useful criterion.

V.