Speed up compilation

[mikeshulman]

Courtesy of @jdchristensen, here are all of the files whose processing time (after #1238) takes at least 5s. We should see if some simple optimizations like nrefine can speed them up noticeably.

0m20.22s | 548372 ko | Homotopy/BlakersMassey.vo                                    | 0m21.31s | 554068 ko || -0m01.08s || -5696 ko     | -5.11%   | -1.02%        
0m19.29s | 438404 ko | Classes/implementations/natpair_integers.vo                  | 0m19.03s | 451560 ko || +0m00.25s || -13156 ko    | +1.36%   | -2.91%        
0m13.97s | 404216 ko | Cubical/PathCube.vo                                          | 0m14.63s | 404312 ko || -0m00.66s || -96 ko       | -4.51%   | -0.02%        
0m13.68s | 438664 ko | Modalities/ReflectiveSubuniverse.vo                          | 0m15.62s | 471760 ko || -0m01.93s || -33096 ko    | -12.41%  | -7.01%        
0m11.51s | 519916 ko | Spaces/BAut/Bool.vo                                          | 0m08.34s | 423852 ko || +0m03.16s || 96064 ko     | +38.00%  | +22.66%       
0m10.26s | 529296 ko | Homotopy/HomotopyGroup.vo                                    | 0m11.14s | 573916 ko || -0m00.88s || -44620 ko    | -7.89%   | -7.77%        
0m08.42s | 401248 ko | Idempotents.vo                                               | 0m08.93s | 402580 ko || -0m00.50s || -1332 ko     | -5.71%   | -0.33%        
0m08.23s | 633228 ko | Spaces/Torus/TorusEquivCircles.vo                            | 0m08.91s | 635884 ko || -0m00.67s || -2656 ko     | -7.63%   | -0.41%        
0m08.21s | 335196 ko | Categories/Adjoint/Pointwise.vo                              | 0m08.36s | 335216 ko || -0m00.14s || -20 ko       | -1.79%   | -0.00%        
0m06.41s | 359240 ko | Spaces/Finite.vo                                             | 0m06.74s | 365496 ko || -0m00.33s || -6256 ko     | -4.89%   | -1.71%        
0m06.32s | 361976 ko | Spaces/No/Core.vo                                            | 0m06.33s | 365308 ko || -0m00.00s || -3332 ko     | -0.15%   | -0.91%        
0m05.85s | 405072 ko | Algebra/AbelianGroup.vo                                      | 0m05.93s | 418236 ko || -0m00.08s || -13164 ko    | -1.34%   | -3.14%        
0m05.75s | 428368 ko | Colimits/Colimit_Flattening.vo                               | 0m06.17s | 428364 ko || -0m00.41s || 4 ko         | -6.80%   | +0.00%        
0m05.22s | 392660 ko | Classes/theory/premetric.vo                                  | 0m05.12s | 393008 ko || +0m00.09s || -348 ko      | +1.95%   | -0.08%        

[jdchristensen]

Here's something easy that is win-win: look for unneeded imports. Importing large things takes a surprising amount of time. I checked Descent.v and Separated.v, and found a bunch. Removing unneeded imports has the extra benefit that when developing, changes won't trigger building as many files. @JasonGross Can your bug minimizer to adapted to find unneeded imports?

I suspect reduced import time is why Mike's no-module changes slightly sped up so many other files.

[JasonGross]

Imports, or Requires? https://github.com/JasonGross/coq-tools/blob/master/minimize-requires.py should be able to use unneeded Requires. Be warned that this may break subsequent files.

[jdchristensen]

Cool. If someone wants to give it a try, please do!

[jdchristensen]

And here are the 20 slowest lines in the library. This is after #1267, which greatly speeds up BlakersMassey. (In current master, it tops the list with >10s on one Qed line.)

$ cd theories
$ find . -name '*.v.timing' -exec awk '{printf "%-55s %s\n", "{}:", $0}' {} \; | sort -nr -k7 | head -20 | sed 's/.v.timing//'
./Spaces/Torus/TorusEquivCircles:              Chars 7665 - 7686 [End~TorusEquivCircle.] 4.727 secs (4.696u,0.028s)
./Cubical/PathCube:                            Chars 20377 - 20391 [by~destruct~a.] 4.379 secs (4.341u,0.007s)
./Categories/Adjoint/Pointwise:                Chars 3499 - 4713 [Time~(exists~unit_l~counit_l;~...] 4.377 secs (4.311u,0.054s)
./Spaces/Torus/TorusEquivCircles:              Chars 7015 - 7023 [Defined.] 3.863 secs (3.839u,0.024s)
./Categories/Adjoint/Pointwise:                Chars 7107 - 8392 [Time~(exists~unit_r~counit_r;~...] 3.55 secs (3.549u,0.s)
./Categories/ExponentialLaws/Law2/Law:         Chars 1471 - 1641 [(split;~path_functor;~~~[~exis...] 3.012 secs (3.007u,0.003s)
./Homotopy/BlakersMassey:                      Chars 25002 - 25006 [(cbn).] 2.92 secs (2.919u,0.s)
./Homotopy/HomotopyGroup:                      Chars 6425 - 6433 [Defined.] 2.846 secs (2.802u,0.007s)
./Categories/ExponentialLaws/Law3/Law:         Chars 1093 - 1400 [(split;~path_functor;~~~[~exis...] 2.641 secs (2.611u,0.027s)
./Cubical/PathCube:                            Chars 3659 - 3663 [(cbn).] 2.623 secs (2.613u,0.007s)
./Categories/Grothendieck/ToSet/Univalent:     Chars 1548 - 1638 [refine~~(@isequiv_homotopic~_~...] 2.317 secs (2.301u,0.015s)
./Spaces/Torus/TorusEquivCircles:              Chars 3363 - 3371 [Defined.] 2.247 secs (2.23u,0.016s)
./Colimits/Colimit_Flattening:                 Chars 7166 - 7174 [Defined.] 1.962 secs (1.956u,0.004s)
./Spaces/BAut/Bool:                            Chars 15969 - 16121 [exact~~(nontrivial_negb_center...] 1.938 secs (1.937u,0.s)
./Algebra/AbelianGroup:                        Chars 4006 - 4014 [Defined.] 1.932 secs (1.915u,0.015s)
./Homotopy/BlakersMassey:                      Chars 13959 - 13963 [Qed.] 1.907 secs (1.907u,0.s)
./Categories/Adjoint/Functorial/Laws:          Chars 6767 - 7514 [Definition~right_composition_o...] 1.898 secs (1.889u,0.007s)
./Classes/implementations/natpair_integers:    Chars 13000 - 13140 [(repeat~split;~try~apply~_;~(f...] 1.852 secs (1.852u,0.s)
./Algebra/AbelianGroup:                        Chars 4827 - 4836 [End~Abel.] 1.63 secs (1.574u,0.023s)
./Spaces/Torus/TorusEquivCircles:              Chars 4357 - 4365 [Defined.] 1.593 secs (1.581u,0.011s)

[jdchristensen]

I tried using @JasonGross 's minimize-requires script, but I couldn't get it to work on the HoTT library. I opened an issue: JasonGross/coq-tools#123

It would be great to get rid of unneeded imports!

[jdchristensen]

After #1823, here are the slowest files in the library. I'll make a separate comment about Pointed/Core.v

    Time |  Peak Mem | File Name                                                   
-----------------------------------------------------------------------------------
1m50.18s | 529420 ko | Total Time / Peak Mem                                       
-----------------------------------------------------------------------------------
0m04.20s | 474556 ko | Homotopy/Syllepsis.vo                                       
0m03.31s | 498748 ko | Pointed/Core.vo                                             
0m02.78s | 460732 ko | Classes/implementations/natpair_integers.vo                 
0m02.03s | 424120 ko | Colimits/Sequential.vo                                      
0m01.94s | 434492 ko | Cubical/PathCube.vo                                         
0m01.73s | 458948 ko | Homotopy/CayleyDickson.vo                                   
0m01.63s | 529420 ko | Spaces/Torus/TorusEquivCircles.vo                           
0m01.54s | 360508 ko | Categories/Adjoint/Pointwise.vo                             
0m01.47s | 405948 ko | Idempotents.vo                                              
0m01.31s | 356540 ko | Categories/Adjoint/Functorial/Laws.vo                       
0m01.31s | 407856 ko | Homotopy/Join/TriJoin.vo                                    
0m01.29s | 421724 ko | Algebra/AbSES/Pushout.vo                                    
0m01.20s | 431036 ko | Colimits/Colimit_Flattening.vo                              
0m01.19s | 428668 ko | Algebra/AbSES/PullbackFiberSequence.vo                      
0m01.18s | 411032 ko | Algebra/Groups/FreeProduct.vo                               
0m01.16s | 418596 ko | Algebra/AbSES/Core.vo                                       
0m01.09s | 412732 ko | Classes/theory/premetric.vo                                 
0m01.06s | 360888 ko | Categories/ExponentialLaws/Law2/Law.vo                      
0m01.03s | 416732 ko | Algebra/AbSES/Pullback.vo                                   
0m01.00s | 400084 ko | Homotopy/Join/JoinAssoc.vo                                  
0m01.00s | 395192 ko | Modalities/ReflectiveSubuniverse.vo                         
0m00.91s | 392360 ko | Spaces/Finite/Finite.vo                                     
0m00.84s | 357688 ko | Categories/ExponentialLaws/Law3/Law.vo                      
0m00.83s | 403872 ko | Analysis/Locator.vo                                         
0m00.80s | 382520 ko | Spaces/No/Core.vo                                           
0m00.78s | 404560 ko | Classes/theory/rationals.vo                                 
0m00.78s | 366780 ko | Colimits/Coeq.vo                                            
0m00.78s | 429740 ko | Homotopy/ClassifyingSpace.vo                                
0m00.76s | 420952 ko | Homotopy/HomotopyGroup.vo                                   
0m00.75s | 403584 ko | Pointed/pSusp.vo                                            
0m00.74s | 416820 ko | Spaces/BAut/Bool.vo                                         
0m00.73s | 353208 ko | Categories/ExponentialLaws/Law4/Law.vo                      

[jdchristensen]

@Alizter The new material using pelim in Pointed/Core.v is slow, especially in is21cat_ptype. The Defined line for that proof is the slowest line in the library. The line-by-line timing of that file is shown here.

[jdchristensen]

The 20 slowest lines in the library are below. @JasonGross Categories gets 7 of the spots on the list.

$ find . -name '*.v.timing' -exec awk '{printf "%-55s %s\n", "{}:", $0}' {} \; | sort -nr -k7 | head -20 | sed 's/.v.timing//' | sed 's|\./||'
Pointed/Core:                                Chars 21773 - 21781 [Defined.] 1.129 secs (1.109u,0.019s)
Categories/Adjoint/Pointwise:                Chars 3355 - 4476 [(exists~unit_l~counit_l;~~~abs...] 0.787 secs (0.724u,0.063s)
Categories/Adjoint/Functorial/Laws:          Chars 6697 - 7444 [Definition~right_composition_o...] 0.697 secs (0.697u,0.s)
Categories/Adjoint/Pointwise:                Chars 6868 - 8057 [(exists~unit_r~counit_r;~~~abs...] 0.668 secs (0.668u,0.s)
Categories/ExponentialLaws/Law2/Law:         Chars 1306 - 1476 [(split;~path_functor;~~~[~exis...] 0.633 secs (0.623u,0.009s)
Homotopy/Syllepsis:                          Chars 36784 - 36804 [(generalize_goal~lem).] 0.614 secs (0.606u,0.007s)
Categories/ExponentialLaws/Law3/Law:         Chars 978 - 1285 [(split;~path_functor;~~~[~exis...] 0.571 secs (0.532u,0.039s)
Spaces/Torus/TorusEquivCircles:              Chars 7062 - 7070 [Defined.] 0.555 secs (0.547u,0.007s)
Homotopy/Syllepsis:                          Chars 39316 - 39320 [Qed.] 0.527 secs (0.519u,0.007s)
Cubical/PathCube:                            Chars 3964 - 3972 [Defined.] 0.496 secs (0.484u,0.012s)
Colimits/Colimit_Flattening:                 Chars 7057 - 7065 [Defined.] 0.488 secs (0.484u,0.003s)
Spaces/Torus/TorusEquivCircles:              Chars 7724 - 7745 [End~TorusEquivCircle.] 0.476 secs (0.464u,0.012s)
Homotopy/Syllepsis:                          Chars 30389 - 36211 [Definition~eh_V_p_pp_gen~{X~:~...] 0.472 secs (0.468u,0.003s)
Homotopy/CayleyDickson:                      Chars 9091 - 9108 [(apply~join_natsq).] 0.39 secs (0.39u,0.s)
Homotopy/CayleyDickson:                      Chars 9492 - 9509 [(apply~join_natsq).] 0.366 secs (0.366u,0.s)
Categories/ExponentialLaws/Law2/Law:         Chars 1479 - 1483 [Qed.] 0.366 secs (0.366u,0.s)
Colimits/Sequential:                         Chars 8911 - 8919 [Defined.] 0.363 secs (0.36u,0.003s)
Idempotents:                                 Chars 25465 - 25469 [Qed.] 0.307 secs (0.307u,0.s)
Categories/GroupoidCategory/Morphisms:       Chars 654 - 901 [(apply~~~(isequiv_adjointify~(...] 0.306 secs (0.262u,0.043s)
Homotopy/CayleyDickson:                      Chars 9512 - 9520 [Defined.] 0.303 secs (0.295u,0.007s)

[Alizter]

@Alizter The new material using pelim in Pointed/Core.v is slow, especially in is21cat_ptype. The Defined line for that proof is the slowest line in the library. The line-by-line timing of that file is shown here.

I reckon if we split the proof into smaller lemmas that the speed will be better.