Port HoTT to Coq 8.5pl1

[JasonGross]

This bumps the submodule to 8.5pl1, and fixes what needs to be fixed to support that.

The timing diff, since 8.5beta2, is:

After    | File Name                                                 | Before   || Change
--------------------------------------------------------------------------------------------
3m41.65s | Total                                                     | 3m15.18s || +0m26.47s
--------------------------------------------------------------------------------------------
0m06.32s | categories/Adjoint/Pointwise                              | 0m20.34s || -0m14.01s
0m15.72s | hit/V                                                     | 0m10.72s || +0m05.00s
0m10.53s | Algebra/ooGroup                                           | 0m06.22s || +0m04.30s
0m14.63s | Spaces/BAut/Bool                                          | 0m11.50s || +0m03.13s
0m13.81s | categories/Category/Sigma/Univalent                       | 0m10.68s || +0m03.13s
0m05.89s | Spaces/BAut                                               | 0m02.38s || +0m03.50s
0m04.83s | contrib/HoTTBook                                          | 0m01.38s || +0m03.45s
0m07.94s | contrib/Freudenthal                                       | 0m06.47s || +0m01.47s
0m06.25s | Spaces/No                                                 | 0m04.62s || +0m01.62s
0m04.72s | categories/ExponentialLaws/Law2/Law                       | 0m03.59s || +0m01.12s
0m02.50s | Spaces/BAut/Cantor                                        | 0m01.27s || +0m01.23s
0m01.82s | Spaces/BAut/Bool/IncoherentIdempotent                     | 0m00.80s || +0m01.02s
0m08.02s | Modalities/ReflectiveSubuniverse                          | 0m07.70s || +0m00.31s
0m05.99s | Spaces/Finite                                             | 0m05.06s || +0m00.93s
0m05.82s | Idempotents                                               | 0m05.44s || +0m00.37s

I think the changes are small enough that it's reasonable to merge this.

The slowdown in V.v (50%) and Algebra/ooGroup.v (70%) and Spaces/BAut.v (150%) and contrib/HoTTBook.v (250%), and possibly others, are from the 8.5beta2 → 8.5beta3 transition. Overall, we have a 15% slowdown, which isn't terrible on a project this size, I think. Any ideas on this @ppedrot @mattam82 ?

This closes #794, #785, #793, #735.

[mikeshulman]

Sure, I'm ok with that. Cute that this is issue #800.

[mattam82]

Certainly good to keep in mind that these have slowed down, but it all seems pretty reasonable to me. Did you try to Ltacprof the few larger ones? This might reveal hotspots.

[JasonGross]

@mattam82 at least one of the issues (contrib/HoTTBook.v) seems to be that some universe handling is slower?

I don't have an LtacProf that works with 8.5beta2. Here's the profiling log from selected files with 8.5pl1:

• contrib/HoTTBook spends 0.004 s in tactic code, 0.751 s in Require Import, and 3.944 s on Definition Book_10_5_8_item_vi := @HoTT.hit.V.function. (I presume all of this is on managing the 2316 universe variables that get associated with Book_10_5_8_item_vi.)
• Spaces/BAut (2.38 s -> 5.89 s):

total time:      4.188s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─baut_reduce ---------------------------  20.0%  27.1%       2    0.632s
─exact _ -------------------------------  15.1%  19.9%       6    0.328s
─rewrite !whiskerR_pp, !concat_pp_p ----  17.5%  17.5%       1    0.732s
─rewrite !whiskerL_pp, !concat_pp_p ----  16.6%  16.6%       1    0.696s
─cbn -----------------------------------   8.5%   8.5%       3    0.272s
─assert (forall Z : BAut X, IsHSet (1 =    0.1%   7.9%       1    0.332s
─assert (IsHSet (1 = 1)) by exact _ ----   0.0%   7.0%       1    0.292s
─change Contr_internal with Contr in * -   6.9%   6.9%     342    0.008s
─change IsTrunc_internal with IsTrunc in   6.4%   6.4%     339    0.008s
─assert (IsHSet (Z.1 = Z.1)) by exact _    0.1%   5.0%       1    0.208s
─exact (ap (path_sigma_hprop _ _) path_u   3.2%   3.2%       1    0.136s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─baut_reduce ---------------------------  20.0%  27.1%       2    0.632s
 ├─change Contr_internal with Contr in *   3.3%   3.3%      35    0.008s
 └─change IsTrunc_internal with IsTrunc    3.2%   3.2%      33    0.008s
─rewrite !whiskerR_pp, !concat_pp_p ----  17.5%  17.5%       1    0.732s
─rewrite !whiskerL_pp, !concat_pp_p ----  16.6%  16.6%       1    0.696s
─cbn -----------------------------------   8.5%   8.5%       3    0.272s
─assert (forall Z : BAut X, IsHSet (1 =    0.1%   7.9%       1    0.332s
└exact _ -------------------------------   5.9%   7.8%       1    0.328s
─assert (IsHSet (1 = 1)) by exact _ ----   0.0%   7.0%       1    0.292s
└exact _ -------------------------------   5.2%   7.0%       1    0.292s
─assert (IsHSet (Z.1 = Z.1)) by exact _    0.1%   5.0%       1    0.208s
└exact _ -------------------------------   3.8%   4.9%       1    0.204s
─exact (ap (path_sigma_hprop _ _) path_u   3.2%   3.2%       1    0.136s

• hit/V spends 1.764 seconds on refine (@untrunc_istrunc -1 {y : V & y ∈ v * [x, y] ∈ phi} _ (H2 x (transport (fun z => x ∈ z) memb_u^ (tr (a; 1)))))., 1.613 seconds on a Qed, and has the profile:

total time:      5.872s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─destruct (untrunc_istrunc (-1) (transpo  13.8%  13.8%       1    0.808s
─destruct (fst path_pair_ord p') as (px'  12.7%  12.7%       1    0.744s
─apply Trunc_rec -----------------------   9.6%   9.8%      13    0.124s
─destruct (fst path_pair_ord p) as (px,    8.7%   8.7%       1    0.508s
─apply path_ishprop --------------------   5.9%   6.0%       9    0.244s
─assert  (h :   forall a : [u], {b : [v]   6.0%   6.0%       1    0.352s
─apply (Trunc_functor (-1)) ------------   4.4%   4.4%      33    0.032s
─apply tr ------------------------------   2.7%   2.7%      33    0.020s
─apply  (isinj_embedding func_of_members   2.5%   2.5%       1    0.148s
─simpl ---------------------------------   2.1%   2.1%      17    0.052s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─destruct (untrunc_istrunc (-1) (transpo  13.8%  13.8%       1    0.808s
─destruct (fst path_pair_ord p') as (px'  12.7%  12.7%       1    0.744s
─apply Trunc_rec -----------------------   9.6%   9.8%      13    0.124s
─destruct (fst path_pair_ord p) as (px,    8.7%   8.7%       1    0.508s
─apply path_ishprop --------------------   5.9%   6.0%       9    0.244s
─assert  (h :   forall a : [u], {b : [v]   6.0%   6.0%       1    0.352s
─apply (Trunc_functor (-1)) ------------   4.4%   4.4%      33    0.032s
─apply tr ------------------------------   2.7%   2.7%      33    0.020s
─apply  (isinj_embedding func_of_members   2.5%   2.5%       1    0.148s
─simpl ---------------------------------   2.1%   2.1%      17    0.052s

• Algebra/ooGroup:

total time:     10.184s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─pose proof (eisretr (loops_group X) g)   38.3%  38.3%       2    1.956s
─simpl ---------------------------------  21.9%  21.9%       9    2.212s
─pose (p := eisretr (loops_group X) g) -  19.1%  19.1%       1    1.948s
─apply (equiv_inj (equiv_path_sigma_hpro   7.7%   7.7%       1    0.780s
─rewrite !loops_functor_group ----------   7.0%   7.0%       3    0.364s
─grouphom_reduce -----------------------   0.0%   3.5%       6    0.260s
─pointed_reduce ------------------------   0.0%   2.0%       6    0.140s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─pose proof (eisretr (loops_group X) g)   38.3%  38.3%       2    1.956s
─simpl ---------------------------------  21.9%  21.9%       9    2.212s
─pose (p := eisretr (loops_group X) g) -  19.1%  19.1%       1    1.948s
─apply (equiv_inj (equiv_path_sigma_hpro   7.7%   7.7%       1    0.780s
─rewrite !loops_functor_group ----------   7.0%   7.0%       3    0.364s
─grouphom_reduce -----------------------   0.0%   3.5%       6    0.260s
└pointed_reduce ------------------------   0.0%   2.0%       6    0.140s

• Spaces/BAut/Bool:

total time:      8.700s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─destruct (dec (y1 = y2)) as [p| p] ----  26.1%  26.2%       2    1.156s
─case (p ((ap e)^-1 (q1 @ q2^))) -------  25.7%  26.0%       4    0.592s
─destruct (dec (z = w)) ----------------  13.4%  13.5%       1    1.176s
─exact _ -------------------------------   4.2%   4.3%       8    0.124s
─simpl ---------------------------------   3.1%   3.1%      12    0.188s
─exact  (nontrivial_negb_center_baut_boo   2.8%   2.8%       1    0.240s
─change Contr_internal with Contr in * -   2.3%   2.3%     393    0.008s
─apply moveR_equiv_M -------------------   2.0%   2.2%       1    0.188s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─destruct (dec (y1 = y2)) as [p| p] ----  26.1%  26.2%       2    1.156s
─case (p ((ap e)^-1 (q1 @ q2^))) -------  25.7%  26.0%       4    0.592s
─destruct (dec (z = w)) ----------------  13.4%  13.5%       1    1.176s
─simpl ---------------------------------   3.1%   3.1%      12    0.188s
─exact _ -------------------------------   2.8%   2.9%       7    0.120s
─exact  (nontrivial_negb_center_baut_boo   2.8%   2.8%       1    0.240s
─apply moveR_equiv_M -------------------   2.0%   2.2%       1    0.188s

• categories/Category/Sigma/Univalent:

total time:      4.568s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─exact _ -------------------------------  20.8%  47.3%       7    2.084s
─change Contr_internal with Contr in * -  37.0%  37.0%     434    0.032s
─change IsTrunc_internal with IsTrunc in  36.7%  36.7%     406    0.032s
─exists ((e^-1)%morphism; center _) ----   1.0%   2.5%       1    0.116s

 tactic                                    self  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─exact _ -------------------------------  20.8%  47.3%       7    2.084s
 ├─change IsTrunc_internal with IsTrunc   13.6%  13.6%     129    0.024s
 └─change Contr_internal with Contr in *  12.9%  12.9%     130    0.020s
─change Contr_internal with Contr in * -  22.3%  22.3%     224    0.032s
─change IsTrunc_internal with IsTrunc in  21.8%  21.8%     203    0.032s
─exists ((e^-1)%morphism; center _) ----   1.0%   2.5%       1    0.116s

[ppedrot]

If I remember correctly, one of the costly refines of V was due to the retyping of projections (@mattam82 knows what I mean). It's quite credible that the same hotspot appears in other places.

[ppedrot]

FTR, I've made a bit of profiling on Spaces/BAut.v, and it turns out that the costliest operation is the hashconsing of algebraic universes in instance substitutions. Maybe we should try to turn it off?

[spitters]

Thanks! This looks good. Let's give the coqdevs some time to see whether they have any insights. If not feel free to merge.

[JasonGross]

I'm going to merge this, taking @spitters and @mikeshulman approving comments as acks.

[mikeshulman]

Now that we are on a stable branch, is there any chance we can make the library usable with a standard distribution of Coq, instead of having to be compiled by hand?

[JasonGross]

What do you mean? The library will work fine with the standard released Coq 8.5pl1; configure will find it if it's the first in the PATH. (We still need to compile our own replacement standard library, but I was under the impression this was because Coq's standard library was not compiled with -indices-matter, and so is believed to be inconsistent with univalence. Perhaps the installation instructions should be updated, though.

[mikeshulman]

Maybe that's it. The INSTALL file says

We are compatible with Coq 8.5pl1, so binary packages can be used. Paths still need to be set manually.

but that's extremely brief. Probably it would be better to start the file with detailed instructions on how to do this, and only then go into the "if you want to compile Coq yourself instead, then do X".