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 18, 2023
1 parent a12b58f commit 1e7c435
Showing 1 changed file with 14 additions and 14 deletions.
28 changes: 14 additions & 14 deletions structures.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -268,14 +268,14 @@ Elpi Export HB.locate.
*)

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

Check warning on line 270 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 +301,7 @@ Elpi Export HB.about.
*)

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

Check warning on line 303 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 +310,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 +342,13 @@ Elpi Export HB.howto.
*)

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

Check warning on line 344 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 +370,14 @@ tred file.dot | xdot -
*)

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

Check warning on line 372 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 +418,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
*)

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

Check warning on line 420 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 +431,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 +585,7 @@ HB.structure Definition StructureName params :=
*)

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

Check warning on line 587 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 +599,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 +639,7 @@ HB.instance Definition N Params := Factory.Build Params T …
*)

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

Check warning on line 641 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 +649,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 +670,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 672 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 +683,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 +730,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 +744,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 +754,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 +766,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 +806,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 +832,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 +878,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 +927,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 +940,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 1e7c435

Please sign in to comment.