At the time of writing Proof General does not handle quotations correctly, see ProofGeneral/PG#437. In particular Elpi Accumulate lp:{{ .... }}. is used in tutorials to mix Rocq and Elpi code without escaping. Rocq-Elpi also accepts Elpi Accumulate " .... ". but strings part of the Elpi code needs to be escaped. Finally, for non-tutorial material, one can always put the code in an external file declared with From some.load.path Extra Dependency "filename" as f. and use Elpi Accumulate File f..

RocqIDE does handle quotations. The installation process puts coq-elpi.lang in a place where RocqIDE can find it. Then you can select coq-elpi from the menu Edit -> Preferences -> Colors.

For Vim users, Coqtail provides syntax highlighting and handles quotations.

To install the development version one can type

opam pin add rocq-elpi https://github.com/LPCIC/coq-elpi.git

One can also clone this repository and type make, but check you have all the dependencies installed first (see rocq-elpi.opam).

We recommend to look at the CI setup for ocaml versions being tested. Also, we recommend to install dot-merlin-reader and ocaml-lsp-server (version 1.15).

• Elpi Command <qname> creates command named <qname> containing the preamble elpi-command.
• Elpi Tactic <qname> creates a tactic <qname> containing the preamble elpi-tactic.
• Elpi Db <dbname> <code> creates a Db (a program that is accumulated into other programs). <code> is the initial contents of the Db, including the type declaration of its constituting predicates. It understands the #[phase] attribute, see synterp-vs-interp.
• Elpi Program <qname> <code> lower level primitive letting one crate a command/tactic with a custom preamble <code>.
• From some.load.path Extra Dependency <filename> as <fname> declares <fname> as a piece of code that can be accumulated via Elpi Accumulate File. The content is given in the external file <filename> to be found in the Rocq load path some.load.path.
• Elpi File <fname> <code>. declares <fname> as a piece of code that can be accumulated via Elpi Accumulate File. This time the code is given in the .v file. It understands the #[phase] attribute, see synterp-vs-interp.
• Elpi Accumulate [<dbname>|<qname>] [<code>|File [Signature] <fname>|Db [Header] <dbname>] adds code to the current program (or <dbname> or <qname> if specified). The code can be verbatim, from a file or a Db. File names <fname> must have been previously declared with Extra Dependency or Elpi File. Accumulating File Signature <fname> only adds the signautre declarations (kinds, types, modes, type abbreviations) from <fname> skipping the code (clauses/rules). Accumulating Db Header <dbname>, instead of Db <dbname>, accumulates only the first chunk of code associated with Db, typically the type declaration of the predicates that live in the Db. When defining a command or tactic it can be useful to first accumulate the Db header, then some code (possibly calling the predicate living in the Db), and finally accumulating the (full) Db. Note that when a command is executed it may need to be (partially) recompiled, e.g. if the Db was updated. In this case all the code accumulated after the Db (but not after its header) may need to be recompiled. Hence we recommend to accumulate Dbs last. It understands the #[skip="rex"] and #[only="rex"] which make the command a no op if the Rocq version is matched (or not) by the given regular expression. It understands the #[phase] attribute, see synterp-vs-interp. It understands the #[local], #[global], and #[superglobal] scope attributes, although only when accumulating to a <dbname> (all accumulations to a program are #[superglobal]). Default accumulation to db is the equivalent of #[export]. See the Rocq reference manual for the meaning of these scopes.
• Elpi Typecheck [<qname>] typechecks the current program (or <qname> if specified). It understands the #[phase] attribute, see synterp-vs-interp
• 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
• Elpi Trace [[<start> <stop>] <predicate-filter>*|Off] enable/disable tracing, eventually limiting it to a specific range of execution steps or predicate names. It understands the #[phase] attribute, see synterp-vs-interp
• Elpi Trace Browser enable/disable tracing for Elpi's trace browser.
• Elpi Bound Steps <number> limits the number of steps an Elpi program can make.
• Elpi Print <qname> [<string> <filter>*] prints the program <qname> to a text file called <qname>.txt (or <string> if provided) filtering out clauses whose file or clause-name matches <filter>. It understands the #[phase] attribute, see synterp-vs-interp

where:

• <qname> is a qualified Rocq name, e.g. derive.eq or my_program.
• <dbname> is like <qname> but lives in a different namespace. By convention <dbname> ends in .db, e.g. derive.eq.db.
• <code> is verbatim Elpi code, either lp:{{ ... }} or " ... " (in the latter case, strings delimiters need to be escaped following Rocq rules, e.g. lp:{{ coq.say "hello!" }} becomes " coq.say ""hello!"" ").
• <filename> is a string containing the path of an external file, e.g. "this_file.elpi".
• <fname> is a qualified Rocq name, eg foo.elpi (note that Extra Dependency only allows simple identifiers).
• <start> and <stop> are numbers, e.g. 17 24.
• <predicate-filter> is a regexp against which the predicate name is matched, e.g. "derive.*".

Since version 8.18 Rocq has separate parsing and execution phases, respectively called synterp and interp.

Since Rocq has an extensible grammar the parsing phase is not entirely performed by the parser: after parsing one sentence Rocq evaluates its synterp action. The synterp actions of a command like Import A. are the subset of its effect which affect parsing, like enabling a notation. Later, during the execution phase Rocq evaluates the its interp action, which includes effects like putting lemma names in scope or enables type class instances etc.

Being able to parse an entire document quickly, without actually executing any sentence, is important for developing reactive user interfaces, but requires some extra work when defining new commands, in particular to separate their synterp actions from their interp ones. Each command defined with Rocq-Elpi is split into two programs, one running during the parsing phase and the other one during the execution phase.

Declaration of synterp actions

Each Elpi Command internally declares two programs with the same name. One to be run while the Rocq document is parsed, the synterp-command, and the other one while it is executed, the interp command. Elpi Accumulate, by default, adds code to the interp-command. The #[phase] attribute can be used to accumulate code to the synterp-command or to both commands. Elpi Typecheck checks both commands.

Each Elpi Db internally declares one db, by default for the interp phase. The #[phase] attribute can be used crate a database for the synterp phase, or for both phases. Note that databases for the two phases are distinct, no data is shared among them. In particular the coq.elpi.accumulate* API exists in both phases and only acts on data bases for the current phase.

The alignment of phases

All synterp actions, i.e. calls to APIs dealing with modules and sections like begin/end-module or import/export, have to happen at both synterp and interp time and in the same order.

In order to do so, the synterp-command may need to communicate data to the corresponding interp-command. There are two ways for doing so.

The first one is to use, as the main entry points, the following ones:

pred main-synterp i:list argument, o:any.
pred main-interp i:list argument, i:any.

Unlike main the former outputs a datum while the latter receives it in input. During the synterp phase the API coq.synterp-actions lists the actions performed so far. An excerpt from the coq-builtin-synterp file:

% Action executed during the parsing phase (aka synterp)
kind synterp-action type.
type begin-module id -> synterp-action.
type end-module modpath -> synterp-action.

The synterp-command can output data of that type, but also any other data it wishes.

The second way to communicate data is implicit, but limited to synterp actions. Such synterp actions can be recorded into (nested) groups whose structure is declared using well-bracketed calls to predicates coq.begin-synterp-group and coq.end-synterp-group in the synterp phase. In the interp phase, one can then use predicate coq.replay-synterp-action-group to replay all the synterp actions of the group with the given name at once.

In the case where one wishes to interleave code between the actions of a given group, it is also possible to match the synterp group structure at interp, via coq.begin-synterp-group and coq.end-synterp-group. Individual actions that are contained in the group then need to be replayed individually.

One can use coq.replay-next-synterp-actions to replay all synterp actions until the next beginning/end of a synterp group. However, this is discouraged in favour of using groups explicitly, as this is more modular. Code that used to rely on the now-removed coq.replay-all-missing-synterp-actions predicate can rely on coq.replay-next-synterp-actions instead, but this is discouraged in favour of using groups explicitly)

Syntax of the #[phase] attribute

• #[phase="ph"] where "ph" can be "parsing", "execution" or "both"
• #[synterp] is a shorthand for #[phase="parsing"]
• #[interp] is a shorthand for #[phase="execution]

• Elpi <qname> <argument>*. invokes the main predicate of the <qname> program passing a possible empty list of arguments. This is how you invoke a command.

• elpi <qname> <argument>*. invokes the solve predicate of the <qname> program passing a possible empty list of arguments and the current goal. This is how you invoke a tactic.

• Elpi Export <qname> [As <other-qname>] makes it possible to invoke command <qname> (or <other-qname> if given) without the Elpi prefix or invoke tactic <qname> in the middle of a term just writing <qname> args instead of ltac:(elpi <qname> args). Note that in the case of tactics, all arguments are considered to be terms. Moreover, remember that one can use Tactic Notation to give the tactic a better syntax and a shorter name when used in the middle of a proof script. Commands can declare the behavior of starting/ending a proof by, respectively, using #[proof="begin"] Elpi Export .. and #[proof="end"] Elpi Export ... Starting the proof can depend on the presence of an attribute, for example #[proof(begin_if="interactive")] Elpi Export foo will make foo not open a proof, while #[interactive] foo will open a proof. See also the main-interp-proof and main-interp-qed entry points in coq-builtin.

where <argument> can be:

• a number, e.g. 3, represented in Elpi as (int 3)
• a string, e.g. "foo" or bar.baz, represented in Elpi as (str "foo") and (str "bar.baz"). Rocq keywords and symbols are recognized as strings, eg => requires no quotes. Quotes are necessary if the string contains a space or a character that is not accepted for qualified identifiers or if the string is Definition, Axiom, Record, Structure, Inductive, CoInductive, Variant or Context.
• a term, e.g. (3) or (f x), represented in Elpi as (trm ...). Note that terms always require parentheses, that is 3 is a number while (3) is a Rocq term and depending on the context could be a natural number (i.e. S (S (S O))) or a Z or ... See also the section Terms as arguments down below, and the syntax for Ltac variables down below.

Commands also accept the following arguments (the syntax is as close as possible to the Rocq one: [...] means optional, * means 0 or more). See the argument data type in coq-builtin.elpi for their HOAS encoding. See also the section Terms as arguments down below.

• Definition name binder* [: term] := term
• Axiom name : term
• [ Record | Structure ] name binder* [: sort] := [name] { name : term ; * }
• [ Inductive | CoInductive | Variant ] name binder* [| binder] [: term] := | name binder : term *
• Context binder*

Ltac Variables

Tactics also accept Ltac variables as follows:

• ltac_string:(v) (for v of type string or ident)
• ltac_int:(v) (for v of type int or integer)
• ltac_term:(v) (for v of type constr or open_constr or uconstr or hyp)
• ltac_open_term:(v) (for v of type uconstr)
• ltac_(string|int|term|open_term)_list:(v) (for v of type list of ...)
• ltac_tactic:(t) (for t of type tactic)
• ltac_attributes:(v) (for v of type attributes) For example:

Tactic Notation "tac" string(X) ident(Y) int(Z) hyp(T) constr_list(L) simple_intropattern_list(P) uconstr(U) tactic(TA) :=
  elpi tac ltac_string:(X) ltac_string:(Y) ltac_int:(Z) ltac_term:(T) ltac_term_list:(L) ltac_tactic:(intros P) ltac_open_term:(U) ltac_tactic:(TA).

lets one write tac "a" b 3 H t1 t2 t3 [|m] u ta in any Ltac context. Arguments are first interpreted by Ltac according to the types declared in the tactic notation and then injected in the corresponding Elpi argument. For example H must be an existing hypothesis, since it is typed with the hyp Ltac type, but in Elpi it will appear as a term, eg trm c0. Similarly t1, t2 and t3 are checked to be well typed and to contain no unresolved implicit arguments, since this is what the constr Ltac type means If they were typed as open_constr or uconstr, the last or both checks would be respectively skipped. In any case they are passed to the Elpi code as trm .... Both "a" and b are passed to Elpi as str .... Argument U flagged as ltac_open_term can mention free variables. The Elpi tactic receives open-trm N F where N is the number of free variables in U and F is fun x1 => ... fun xN => U. Argument TA is received as tac T where T is an (opaque) tactic that can be called via the coq.ltac.* APIs. Finally, ltac_term:(T) and (T) are not synonyms: but the former must be used when defining tactic notations, the latter when invoking elpi tactics directly. `(T) can be used to pass an open term to elpi tactic ....

Attributes

Attributes are supported in both commands and tactics. Examples:

• #[ att ] Elpi cmd
• #[ att ] cmd for a command cmd exported via Elpi Export cmd
• #[ att ] elpi tac
• Tactic Notation ... attributes(A) ... := ltac_attributes:(A) elpi tac. Due to a parsing conflict in Rocq grammar, at the time of writing this code:

  Tactic Notation "#[" attributes(A) "]" "tac" :=
    ltac_attributes:(A) elpi tac.
  

  has the following limitation:
  • #[ att ] tac. does not parse
  • (#[ att ] tac). works
  • idtac; #[ att ] tac. works

Terms as arguments

Since version 1.15, terms passed to Elpi commands code via (term) or via a declaration (like Record, Inductive ...) are in elaborated format by default. This means that all Rocq notational facilities are available, like deep pattern matching, or tactics in terms. One can use the attribute #[arguments(raw)] to declare a command which instead takes arguments in raw format. In that case, notations are unfolded, implicit arguments are expanded (holes _ are added) and lexical analysis is performed (global names and bound names are identified, holes are applied to bound names in scope), but deep pattern matching or tactics in terms are not supported, and in particular type checking/inference is not performed. Once can use the coq.typecheck or coq.elaborate-skeleton APIs to fill in implicit arguments and insert coercions on raw terms.

Terms passed to Elpi tactics via tactic notations can be forced to be elaborated beforehand by declaring the parameters to be of type constr or open_constr. Arguments of type uconstr are passed raw.

Testing/debugging:

• Elpi Query [<qname>] <code> runs <code> in the current program (or in <qname> if specified).
• Elpi Query [<qname>] <synterp-code> <interp-code> runs <synterp-code> in the current (synterp) program (or in <qname> if specified) and <interp-code> in the current program (or <qname>).
• elpi query [<qname>] <string> <argument>* runs the <string> predicate (that must have the same signature of the default predicate solve).

• functional core (fun, forall, match, application, let-in, sorts)
• evars (unification variables)
• single Inductive and CoInductive types (including parameters, non-uniform parameters, indexes)
• mutual Inductive and CoInductive types
• fixpoints
• mutual fixpoints
• cofixpoints
• primitive records
• primitive projections
• primitive integers
• primitive floats
• primitive arrays
• universe polymorphism
• modules
• module types
• functor application
• functor definition

Checked boxes are available, unchecked boxes are planned, missing items are not planned. This is a high level list, for the details see coq-builtin.

• i/o: messages, warnings, errors, Rocq version
• logical environment: read, write, locate
  • dependencies between objects
• type classes database: read, write
  • take over resolution
• canonical structures database: read, write
  • take over resolution
• coercions database: read, write
• sections: open, close
• scope management: import, export
• hints: mode, opaque, resolve, strategy
• arguments: implicit, name, scope, simpl
• abbreviations: read, write, locate
• typing and elaboration
• unification
• reduction: lazy, cbv, vm, native
  • flags for lazy and cbv
• ltac1: bridge to call ltac1 code, mono and multi-goal tactics
• option system: get, set, add
• pretty printer: boxes, printing width
• attributes: read