Elpi Compile

README.md

@@ -193,6 +193,10 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
+- `Elpi Compile <qname list>` forces the compilation (and cache) of a set of programs/tactics.
+  Running a program or a tactic compiles it on the fly and caches the result.
+  The cache entries generated in the middle of proofs are lost then the proof ends,
+  so one may want to cache the compilation of (very large) tactics outside of proofs.
 - `Elpi Debug <string>` sets the variable `<string>`, relevant for conditional
   clause compilation (the `:if VARIABLE` clause attribute).
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)

src/coq_elpi_vernacular.ml

@@ -147,6 +147,7 @@ let compile src =
     try
       lookup_code 0 h src
     with Not_found ->
+      Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: compile: cache miss")));
       match src with
       | Code.Base { base = (k,u) } ->
           let elpi = P.ensure_initialized () in
@@ -166,6 +167,7 @@ let compile src =
     try
       lookup_chunk bh h src
     with Not_found ->
+      Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: compile: cache miss")));
       match src with
       | Chunk.Base { base = (k,u) } ->
           let prog = P.extend_w_units ~base [u] in
@@ -200,6 +202,14 @@ let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,CErrors.iprint
 let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,[],CErrors.iprint ei)))
 [%%endif]
 
+  let compile pl =
+    let t0 = Unix.gettimeofday () in
+    Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: compile: filling cache")));
+    List.iter (fun p -> ignore(get_and_compile p)) pl;
+    Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: compile: filled: %4.3f" (Unix.gettimeofday () -. t0))))
+
+  let compile ~atts:ph pl = skip ~ph compile pl
+
 let run_static_check query =
   let checker = 
     let elpi = P.ensure_initialized () in
@@ -537,11 +547,13 @@ module type Common = sig
   val accumulate_db          : atts:((Str.regexp list option * Str.regexp list option) * phase option) -> ?program:qualified_name -> qualified_name -> unit
   val accumulate_to_db       : atts:((Str.regexp list option * Str.regexp list option) * phase option) -> qualified_name -> Elpi.API.Ast.Loc.t * string -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit
 
+
   val load_checker : string -> unit
   val load_printer : string -> unit
   val load_tactic : string -> unit
   val load_command : string -> unit
-
+
+  val compile : atts:phase option -> qualified_name list -> unit
   val debug         : atts:phase option -> string list -> unit
   val trace         : atts:phase option -> int -> int -> string list -> string list -> unit
   val trace_browser : atts:phase option -> string list -> unit

src/coq_elpi_vernacular.mli

@@ -38,6 +38,8 @@ module type Common = sig
   val load_tactic : string -> unit
   val load_command : string -> unit
 
+  val compile : atts:phase option -> qualified_name list -> unit
+
   val debug         : atts:phase option -> string list -> unit
   val trace         : atts:phase option -> int -> int -> string list -> string list -> unit
   val trace_browser : atts:phase option -> string list -> unit

src/coq_elpi_vernacular_syntax.mlg

@@ -240,6 +240,14 @@ VERNAC COMMAND EXTEND ElpiUnnamed CLASSIFIED AS SIDEFF
    } -> {
      EV.Interp.accumulate_db ~atts  ~program:(snd p) (snd d) }
 
+| #[ atts = any_attribute ] [ "Elpi" "Compile" qualified_name_list(pl) ] SYNTERP AS atts {
+     let atts = validate_attributes synterp_attribute atts in
+     EV.Synterp.compile  ~atts (pl |> List.map snd);
+     atts
+   } -> {
+     EV.Interp.compile  ~atts (pl |> List.map snd) }
+
+
 | #[ atts = any_attribute ] [ "Elpi" "Debug" string_list(s) ] SYNTERP AS atts {
      let atts = validate_attributes synterp_attribute atts in
      EV.Synterp.debug  ~atts s;

tests/test_compile.v

@@ -0,0 +1,10 @@
+From elpi Require Import elpi.
+
+Elpi Command foo.
+Elpi Accumulate lp:{{
+  main _ :- coq.say "ok".
+}}.
+
+Set Debug "elpitime".
+Elpi Compile foo.
+Elpi foo.