From 1e7c4355dcc3395afeff11c6686eb3c7d7b766c7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 9 Aug 2023 10:51:13 +0200 Subject: [PATCH] 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 --- structures.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/structures.v b/structures.v index 19f1153f..eb25b758 100644 --- a/structures.v +++ b/structures.v @@ -268,6 +268,7 @@ Elpi Export HB.locate. *) #[arguments(raw)] Elpi Command HB.about. +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". @@ -275,7 +276,6 @@ 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)). @@ -301,6 +301,7 @@ Elpi Export HB.about. *) #[arguments(raw)] Elpi Command HB.howto. +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". @@ -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] :- !, @@ -342,13 +342,13 @@ Elpi Export HB.howto. *) #[arguments(raw)] Elpi Command HB.status. +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. @@ -370,6 +370,7 @@ tred file.dot | xdot - *) #[arguments(raw)] Elpi Command HB.graph. +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". @@ -377,7 +378,6 @@ 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)). @@ -418,6 +418,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := { *) #[arguments(raw)] Elpi Command HB.mixin. +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". @@ -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 _, !, @@ -585,6 +585,7 @@ HB.structure Definition StructureName params := *) #[arguments(raw)] Elpi Command HB.structure. +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". @@ -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! [ @@ -639,6 +639,7 @@ HB.instance Definition N Params := Factory.Build Params T … *) #[arguments(raw)] Elpi Command HB.instance. +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". @@ -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] :- !, @@ -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. +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". @@ -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)). @@ -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". @@ -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)). @@ -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". @@ -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.". @@ -806,6 +806,7 @@ 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". @@ -813,7 +814,6 @@ 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.". @@ -832,6 +832,7 @@ 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". @@ -839,7 +840,6 @@ 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))). @@ -878,6 +878,7 @@ 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". @@ -885,7 +886,6 @@ 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)). @@ -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". @@ -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 _, !,