Skip to content

Commit

Permalink
Accumulate DB first
Browse files Browse the repository at this point in the history 
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
  • Loading branch information
@proux01
proux01 committed Aug 29, 2023
1 parent a12b58f commit dc9c6e4
Showing 1 changed file with 19 additions and 14 deletions.
33 changes: 19 additions & 14 deletions structures.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,11 @@ pred docstring o:loc, o:string.

#[arguments(raw)] Elpi Command HB.locate.

Check warning on line 240 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
(* Since it can become rather large, accumulating the DB is often by far the
most expensive accumulation. It is then worth sharing its cache between
the commands. To this end, we accumulate the DB first in each command to
ensure the same dependencies and maximize cache hits. For instance, this
can save a few (2 or 3) percents of total compilation time on MathComp. *)
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate lp:{{
Expand Down Expand Up @@ -268,14 +273,14 @@ Elpi Export HB.locate.
*)

#[arguments(raw)] Elpi Command HB.about.

Check warning on line 275 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/about.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [str S] :- !, with-attributes (with-logging (about.main S)).
Expand All @@ -301,6 +306,7 @@ Elpi Export HB.about.
*)

#[arguments(raw)] Elpi Command HB.howto.

Check warning on line 308 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -309,7 +315,6 @@ Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/about.elpi".
Elpi Accumulate File "HB/howto.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [trm T, str STgt] :- !,
Expand Down Expand Up @@ -342,13 +347,13 @@ Elpi Export HB.howto.
*)

#[arguments(raw)] Elpi Command HB.status.

Check warning on line 349 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/status.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [] :- !, status.print-hierarchy.
Expand All @@ -370,14 +375,14 @@ tred file.dot | xdot -
*)

#[arguments(raw)] Elpi Command HB.graph.

Check warning on line 377 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/graph.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [str File] :- with-attributes (with-logging (graph.to-file File)).
Expand Down Expand Up @@ -418,6 +423,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
*)

#[arguments(raw)] Elpi Command HB.mixin.

Check warning on line 425 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -430,7 +436,6 @@ Elpi Accumulate File "HB/instance.elpi".
Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate File "HB/factory.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [A] :- A = indt-decl _, !,
Expand Down Expand Up @@ -585,6 +590,7 @@ HB.structure Definition StructureName params :=
*)

#[arguments(raw)] Elpi Command HB.structure.

Check warning on line 592 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -598,7 +604,6 @@ Elpi Accumulate File "HB/instance.elpi".
Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/factory.elpi".
Elpi Accumulate File "HB/structure.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [const-decl N (some B) Arity] :- !, std.do! [
Expand Down Expand Up @@ -639,6 +644,7 @@ HB.instance Definition N Params := Factory.Build Params T …
*)

#[arguments(raw)] Elpi Command HB.instance.

Check warning on line 646 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -648,7 +654,6 @@ Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/instance.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

main [const-decl Name (some BodySkel) TyWPSkel] :- !,
Expand All @@ -670,6 +675,7 @@ Elpi Export HB.instance.
(** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)

#[arguments(raw)] Elpi Command HB.factory.

Check warning on line 677 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.15) 

This command does not support this attribute: arguments.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -682,7 +688,6 @@ Elpi Accumulate File "HB/instance.elpi".
Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate File "HB/factory.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{
main [A] :- (A = indt-decl _ ; A = const-decl _ _ _), !,
with-attributes (with-logging (factory.declare A)).
Expand Down Expand Up @@ -730,6 +735,7 @@ HB.end.
*)

#[arguments(raw)] Elpi Command HB.builders.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -743,7 +749,6 @@ Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate File "HB/factory.elpi".
Elpi Accumulate File "HB/builders.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{
main [ctx-decl C] :- !, with-attributes (with-logging (builders.begin C)).

Expand All @@ -754,6 +759,7 @@ Elpi Export HB.builders.


#[arguments(raw)] Elpi Command HB.end.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -765,7 +771,6 @@ Elpi Accumulate File "HB/instance.elpi".
Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate File "HB/builders.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{
main [] :- !, with-attributes (with-logging builders.end).
main _ :- coq.error "Usage: HB.end.".
Expand Down Expand Up @@ -806,14 +811,14 @@ Export Algebra.Exports.
*)

#[arguments(raw)] Elpi Command HB.export.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{
main [str M] :- !, with-attributes (with-logging (export.any M)).
main _ :- coq.error "Usage: HB.export M.".
Expand All @@ -832,14 +837,14 @@ Elpi Export HB.export.
(a module which is not closed yet) *)

#[arguments(raw)] Elpi Command HB.reexport.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{
main [] :- !, with-attributes (with-logging (export.reexport-all-modules-and-CS none)).
main [str M] :- !, with-attributes (with-logging (export.reexport-all-modules-and-CS (some M))).
Expand Down Expand Up @@ -878,14 +883,14 @@ Notation foo := foo.body.
*)

#[arguments(raw)] Elpi Command HB.lock.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/lock.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{
main [const-decl Name (some BoSkel) TySkel] :- !,
with-attributes (with-logging (lock.lock-def Name TySkel BoSkel)).
Expand Down Expand Up @@ -927,6 +932,7 @@ HB.instance Definition _ : Ml ... T := ml.
*)

#[arguments(raw)] Elpi Command HB.declare.
Elpi Accumulate Db hb.db.
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
Elpi Accumulate File "HB/common/stdpp.elpi".
Expand All @@ -939,7 +945,6 @@ Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate File "HB/instance.elpi".
Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/factory.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate lp:{{

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

0 comments on commit dc9c6e4

Please sign in to comment.