Synopsis:
Require Import bedrock.elpi.extra.extra.
(* ... *)
Elpi Accumulate File extra.{Program,Tactic,Command}.The three databases account for the nature of the Elpi program being accumulated.
Only commands, for example, can parse attributes, and that's reflected in the types, terms, and predicates available from the Elpi command template and database extra.Command.
All three databases support Coq's half-baked phase distinction (e.g., only interp actions fully support Coq terms while only synterp actions change Coq's module structure).
Use attributes #[interp], #[synterp], #[phase="both"] on Elpi Accumulate.
We put everything in the following Elpi namespaces.
attr, Command only, both phases: Command/both,coq, any prelude, both phases: Program/both, Program/interp, TacticCommand/interp,diag, any prelude, both phases: Program/both, Program/interp,elpi, any prelude, both phases: Program/both,ident, any prelude, interp only: Program/interp,int, any prelude, interp only: Program/interp,list, any prelude, both phases: Program/both, Program/interp,option, any prelude, both phases: Program/both, Program/interp,pair, any prelude, interp only: Program/interp,
Note.
In part, this library relates Elpi types and terms to Gallina types and terms.
We address the same problem---in much the same way---in our Ltac2 library ltac2-extra.
The Elpi namespaces ident, int, list, and option defined here, for example, track modules Ltac2.{Ident, Int, List, Option} from ltac2-extra.
Please try to be consistent!
Example:
Require Import bedrock.elpi.extra.extra.
Elpi Command example.
Elpi Accumulate File extra.Command.We package up the library as databases rather than files because accumulating a given database into an Elpi program may be idempotent while accumulating files certainly is not (see coq-elpi#627).
Idempotence matters because duplicate clauses may lead to hard-to-diagnose operational errors (e.g., backtracking to (a copy of) the same code).
Less important, database names need not vary with Coq's synterp, interp phase distinction and databases (presumably) store compiled code rather than source code.
Our Elpi code uses lib:name to resolve Coq paths previously registered with Rocqlib.
The command Elpi Accumulate panics on unresolved names.
Rather than register everything we need, we reuse names registered by Coq's standard library; for example, we require Coq.Numbers.BinNums because it has the effect of registering names for positive, N, and Z (and their constructors).
Elpi should improve.
Note.
Rocqlib names matter when viewing elpi-extra as a collection of disembodied Elpi files rather than as an Elpi database.
Using elpi-extra as a bunch of files is not supported due to coq-elpi#627, and probably should not be supported in any case.
There seems to be no nice way to tell dune about dependencies between Elpi files triggered by Elpi's accumulate directive.
(Neither dune nor coqdep scans Elpi files for depenencies.)
As a stopgap, we ask dune to generate Elpi files from templates, adding comments containing hashes of their (manually listed) dependencies. This forces clients to recompile when those dependencies change.