Enforce correct database initialisation.

The `Elpi Db` command used to declare the database for all phases,
but only properly initialize it for the current phase. This is no
longer the case, and databases must be declared separately (or via
`#[phase="both"] Elpi Db`) for each phase.

Co-Authored-By: Jan-Oliver Kaiser <[email protected]>

Author: Rodolphe Lepigre

Changelog.md

@@ -4,6 +4,7 @@
 
 ### Commands
 - New `Elpi Accumulate dbname File filename` allows to accumulate a file int a db
+- `Elpi Db` now only creates (and initialises) a database for the specified phase
 
 ### API
 - New `coq.parse-attributes` support for the `attlabel` specification,

apps/NES/theories/NES.v

@@ -3,20 +3,21 @@ From elpi.apps.NES Extra Dependency "nes_interp.elpi" as nes_interp.
 
 From elpi Require Import elpi.
 
-#[synterp] Elpi Db NES.db lp:{{
+#[phase="both"] Elpi Db NES.db lp:{{
 
-pred open-ns o:string, o:list string.
-:name "open-ns:begin"
-open-ns _ _ :- fail.
+typeabbrev path (list string).
+
+:index (2)
+pred ns o:path, o:modpath.
 
 }}.
 
-#[phase="both"] Elpi Accumulate NES.db lp:{{
+#[synterp] Elpi Accumulate NES.db lp:{{
 
-typeabbrev path (list string).
+pred open-ns o:string, o:list string.
+:name "open-ns:begin"
+open-ns _ _ :- fail.
 
-:index (2)
-pred ns o:path, o:modpath.
 }}.
 
 Elpi Command NES.Status.

src/coq_elpi_vernacular.ml

@@ -463,10 +463,11 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc,
       | None -> same_phase Interp P.stage
       | Some phase -> same_phase phase P.stage in
     let elpi = P.ensure_initialized () in
-    P.declare_db n;
-    if do_init then
+    if do_init then begin
+      P.declare_db n;
       let unit = P.unit_from_string ~elpi loc s in
       P.init_db n unit  
+    end
 
   let load_command = P.load_command
   let load_tactic = P.load_tactic