Skip to content

Commit 9116e20

Browse files
proux01proux01
committed
Accumulate DB first
Compilation of MathComp: before: 17.46 (1.24 GB) HB.structure: 01:37 HB.instance: 02:18 after: 17.22 (1.27 GB) HB.structure: 01:38 HB.instance: 02:21
1 parent 16318c8 commit 9116e20

File tree

1 file changed

+19
-14
lines changed

1 file changed

+19
-14
lines changed

‎structures.v‎

Lines changed: 19 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -239,6 +239,11 @@ pred docstring o:loc, o:string.
239239

240240
#[arguments(raw)] Elpi Command HB.locate.
241241
Elpi Accumulate Db hb.db.
242+
(* Since it can become rather large, accumulating the DB is often by far the
243+
most expensive accumulation. It is then worth sharing its cache between
244+
the commands. To this end, we accumulate the DB first in each command to
245+
ensure the same dependencies and maximize cache hits. For instance, this
246+
can save a few (2 or 3) percents of total compilation time on MathComp. *)
242247
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
243248
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
244249
Elpi Accumulate lp:{{
@@ -268,6 +273,7 @@ Elpi Export HB.locate.
268273
*)
269274

270275
#[arguments(raw)] Elpi Command HB.about.
276+
Elpi Accumulate Db hb.db.
271277
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
272278
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
273279
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -277,7 +283,6 @@ Elpi Accumulate File "HB/common/database.elpi".
277283
Elpi Accumulate File "HB/common/utils.elpi".
278284
Elpi Accumulate File "HB/common/log.elpi".
279285
Elpi Accumulate File "HB/about.elpi".
280-
Elpi Accumulate Db hb.db.
281286
Elpi Accumulate lp:{{
282287

283288
main [str S] :- !, with-attributes (with-logging (about.main S)).
@@ -303,6 +308,7 @@ Elpi Export HB.about.
303308
*)
304309

305310
#[arguments(raw)] Elpi Command HB.howto.
311+
Elpi Accumulate Db hb.db.
306312
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
307313
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
308314
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -313,7 +319,6 @@ Elpi Accumulate File "HB/common/utils.elpi".
313319
Elpi Accumulate File "HB/common/log.elpi".
314320
Elpi Accumulate File "HB/about.elpi".
315321
Elpi Accumulate File "HB/howto.elpi".
316-
Elpi Accumulate Db hb.db.
317322
Elpi Accumulate lp:{{
318323

319324
main [trm T, str STgt] :- !,
@@ -346,6 +351,7 @@ Elpi Export HB.howto.
346351
*)
347352

348353
#[arguments(raw)] Elpi Command HB.status.
354+
Elpi Accumulate Db hb.db.
349355
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
350356
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
351357
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -354,7 +360,6 @@ Elpi Accumulate File "HB/common/database.elpi".
354360
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
355361
Elpi Accumulate File "HB/common/utils.elpi".
356362
Elpi Accumulate File "HB/status.elpi".
357-
Elpi Accumulate Db hb.db.
358363
Elpi Accumulate lp:{{
359364

360365
main [] :- !, status.print-hierarchy.
@@ -376,6 +381,7 @@ tred file.dot | xdot -
376381
*)
377382

378383
#[arguments(raw)] Elpi Command HB.graph.
384+
Elpi Accumulate Db hb.db.
379385
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
380386
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
381387
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -385,7 +391,6 @@ Elpi Accumulate File "HB/common/database.elpi".
385391
Elpi Accumulate File "HB/common/utils.elpi".
386392
Elpi Accumulate File "HB/common/log.elpi".
387393
Elpi Accumulate File "HB/graph.elpi".
388-
Elpi Accumulate Db hb.db.
389394
Elpi Accumulate lp:{{
390395

391396
main [str File] :- with-attributes (with-logging (graph.to-file File)).
@@ -426,6 +431,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
426431
*)
427432

428433
#[arguments(raw)] Elpi Command HB.mixin.
434+
Elpi Accumulate Db hb.db.
429435
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
430436
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
431437
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -440,7 +446,6 @@ Elpi Accumulate File "HB/instance.elpi".
440446
Elpi Accumulate File "HB/context.elpi".
441447
Elpi Accumulate File "HB/export.elpi".
442448
Elpi Accumulate File "HB/factory.elpi".
443-
Elpi Accumulate Db hb.db.
444449
Elpi Accumulate lp:{{
445450

446451
main [A] :- A = indt-decl _, !,
@@ -599,6 +604,7 @@ HB.structure Definition StructureName params :=
599604
*)
600605

601606
#[arguments(raw)] Elpi Command HB.structure.
607+
Elpi Accumulate Db hb.db.
602608
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
603609
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
604610
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -614,7 +620,6 @@ Elpi Accumulate File "HB/instance.elpi".
614620
Elpi Accumulate File "HB/context.elpi".
615621
Elpi Accumulate File "HB/factory.elpi".
616622
Elpi Accumulate File "HB/structure.elpi".
617-
Elpi Accumulate Db hb.db.
618623
Elpi Accumulate lp:{{
619624

620625
main [const-decl N (some B) Arity] :- !, std.do! [
@@ -655,6 +660,7 @@ HB.instance Definition N Params := Factory.Build Params T …
655660
*)
656661

657662
#[arguments(raw)] Elpi Command HB.instance.
663+
Elpi Accumulate Db hb.db.
658664
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
659665
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
660666
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -666,7 +672,6 @@ Elpi Accumulate File "HB/common/log.elpi".
666672
Elpi Accumulate File "HB/common/synthesis.elpi".
667673
Elpi Accumulate File "HB/context.elpi".
668674
Elpi Accumulate File "HB/instance.elpi".
669-
Elpi Accumulate Db hb.db.
670675
Elpi Accumulate lp:{{
671676

672677
main [const-decl Name (some BodySkel) TyWPSkel] :- !,
@@ -688,6 +693,7 @@ Elpi Export HB.instance.
688693
(** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)
689694

690695
#[arguments(raw)] Elpi Command HB.factory.
696+
Elpi Accumulate Db hb.db.
691697
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
692698
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
693699
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -702,7 +708,6 @@ Elpi Accumulate File "HB/instance.elpi".
702708
Elpi Accumulate File "HB/context.elpi".
703709
Elpi Accumulate File "HB/export.elpi".
704710
Elpi Accumulate File "HB/factory.elpi".
705-
Elpi Accumulate Db hb.db.
706711
Elpi Accumulate lp:{{
707712
main [A] :- (A = indt-decl _ ; A = const-decl _ _ _), !,
708713
with-attributes (with-logging (factory.declare A)).
@@ -750,6 +755,7 @@ HB.end.
750755
*)
751756

752757
#[arguments(raw)] Elpi Command HB.builders.
758+
Elpi Accumulate Db hb.db.
753759
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
754760
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
755761
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -765,7 +771,6 @@ Elpi Accumulate File "HB/context.elpi".
765771
Elpi Accumulate File "HB/export.elpi".
766772
Elpi Accumulate File "HB/factory.elpi".
767773
Elpi Accumulate File "HB/builders.elpi".
768-
Elpi Accumulate Db hb.db.
769774
Elpi Accumulate lp:{{
770775
main [ctx-decl C] :- !, with-attributes (with-logging (builders.begin C)).
771776

@@ -776,6 +781,7 @@ Elpi Export HB.builders.
776781

777782

778783
#[arguments(raw)] Elpi Command HB.end.
784+
Elpi Accumulate Db hb.db.
779785
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
780786
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
781787
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -789,7 +795,6 @@ Elpi Accumulate File "HB/instance.elpi".
789795
Elpi Accumulate File "HB/context.elpi".
790796
Elpi Accumulate File "HB/export.elpi".
791797
Elpi Accumulate File "HB/builders.elpi".
792-
Elpi Accumulate Db hb.db.
793798
Elpi Accumulate lp:{{
794799
main [] :- !, with-attributes (with-logging builders.end).
795800
main _ :- coq.error "Usage: HB.end.".
@@ -830,6 +835,7 @@ Export Algebra.Exports.
830835
*)
831836

832837
#[arguments(raw)] Elpi Command HB.export.
838+
Elpi Accumulate Db hb.db.
833839
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
834840
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
835841
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -839,7 +845,6 @@ Elpi Accumulate File "HB/common/database.elpi".
839845
Elpi Accumulate File "HB/common/utils.elpi".
840846
Elpi Accumulate File "HB/common/log.elpi".
841847
Elpi Accumulate File "HB/export.elpi".
842-
Elpi Accumulate Db hb.db.
843848
Elpi Accumulate lp:{{
844849
main [str M] :- !, with-attributes (with-logging (export.any M)).
845850
main _ :- coq.error "Usage: HB.export M.".
@@ -858,6 +863,7 @@ Elpi Export HB.export.
858863
(a module which is not closed yet) *)
859864

860865
#[arguments(raw)] Elpi Command HB.reexport.
866+
Elpi Accumulate Db hb.db.
861867
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
862868
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
863869
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -867,7 +873,6 @@ Elpi Accumulate File "HB/common/database.elpi".
867873
Elpi Accumulate File "HB/common/utils.elpi".
868874
Elpi Accumulate File "HB/common/log.elpi".
869875
Elpi Accumulate File "HB/export.elpi".
870-
Elpi Accumulate Db hb.db.
871876
Elpi Accumulate lp:{{
872877
main [] :- !, with-attributes (with-logging (export.reexport-all-modules-and-CS none)).
873878
main [str M] :- !, with-attributes (with-logging (export.reexport-all-modules-and-CS (some M))).
@@ -906,6 +911,7 @@ Notation foo := foo.body.
906911
*)
907912

908913
#[arguments(raw)] Elpi Command HB.lock.
914+
Elpi Accumulate Db hb.db.
909915
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
910916
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
911917
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -915,7 +921,6 @@ Elpi Accumulate File "HB/common/database.elpi".
915921
Elpi Accumulate File "HB/common/utils.elpi".
916922
Elpi Accumulate File "HB/common/log.elpi".
917923
Elpi Accumulate File "HB/lock.elpi".
918-
Elpi Accumulate Db hb.db.
919924
Elpi Accumulate lp:{{
920925
main [const-decl Name (some BoSkel) TySkel] :- !,
921926
with-attributes (with-logging (lock.lock-def Name TySkel BoSkel)).
@@ -957,6 +962,7 @@ HB.instance Definition _ : Ml ... T := ml.
957962
*)
958963

959964
#[arguments(raw)] Elpi Command HB.declare.
965+
Elpi Accumulate Db hb.db.
960966
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
961967
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
962968
Elpi Accumulate File "HB/common/stdpp.elpi".
@@ -971,7 +977,6 @@ Elpi Accumulate File "HB/export.elpi".
971977
Elpi Accumulate File "HB/instance.elpi".
972978
Elpi Accumulate File "HB/context.elpi".
973979
Elpi Accumulate File "HB/factory.elpi".
974-
Elpi Accumulate Db hb.db.
975980
Elpi Accumulate lp:{{
976981

977982
main [Ctx] :- Ctx = ctx-decl _, !,

0 commit comments

Comments
 (0)