Ltac2 Compile

doc/changelog/06-Ltac2-language/17521-tac2compile.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  :cmd:`Ltac2 Compile` command
+  (`#17521 <https://github.com/coq/coq/pull/17521>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -356,8 +356,8 @@ Reduction
 ~~~~~~~~~
 
 We use the usual ML call-by-value reduction, with an otherwise unspecified
-evaluation order. This is a design choice making it compatible with OCaml,
-if ever we implement native compilation. The expected equations are as follows::
+evaluation order. This is a design choice making it compatible with OCaml.
+The expected equations are as follows::
 
   (fun x => t) V ≡ t{x := V} (βv)
 
@@ -1700,9 +1700,57 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions.
    together with its type. This command is pure in the sense that it does not
    modify the state of the proof, and in particular all side-effects are discarded.
 
+Compilation
+-----------
+
+Ltac2 definitions can be compiled to OCaml.  The compiled definitions
+will then run natively instead of using the interpreter.
+
+This functionality is experimental, it may change in non backwards compatible ways.
+
+.. cmd:: Ltac2 Compile {* @qualid }
+
+   Compiles the named Ltac2 definitions and any other Ltac2 definitions they depend on
+   for use in the current Coq process.  The compiled code is used to execute the definitions
+   until the state reset (end of file, end of module, end of section).
+
+   Ltac2 code in an :ref:`antiquotation <term-antiquotations>` will
+   not be compiled. Nor will it be detected by dependency analysis,
+   so Ltac2 definitions in antiquotations in tactics passed to
+   `Ltac2 Compile` will not be automatically compiled.  In this case,
+   the compile command should explicitly list such definitions.
+
+   Compiled code currently does not respect :flag:`Ltac Profiling` and
+   :flag:`Ltac2 Backtrace`.
+
+   Compilation of string and open constructor patterns in or-patterns
+   (e.g. `("foo" | "bar")` or `(Not_found | Assertion_failure)`) is
+   exponentially inefficient. For instance
+   `(("a" | "b" | "c"), ("a" | "b" | "c" | "d"))` produces `3 * 4` OCaml branches.
+
+   .. attr:: recursive{? = {| yes | no } }
+
+      By default :cmd:`Ltac2 Compile` also compiles the dependencies of
+      its arguments. This attribute may be used to make this behaviour
+      explicit or to disable it.
+
+   .. warn:: Skipped compilation of mutable definitions {+ qualid }
+
+      Mutable definitions cannot be compiled. If :cmd:`Ltac2 Compile` in
+      recursive mode is used on a definition which depends on a mutable
+      definition, this warning will be emitted.
+
+   .. exn:: Not allowed to compile mutable @qualid
+
+      This error is emitted when :cmd:`Ltac2 Compile` is given a mutable
+      definition as an argument.
+
+
 Debug
 -----
 
+:flag:`Ltac Profiling` and the related commands and tactics also produce Ltac2 profiles.
+
 .. flag:: Ltac2 Backtrace
 
    When this :term:`flag` is set, toplevel failures will be printed with a backtrace.

doc/tools/docgram/fullGrammar

@@ -697,6 +697,7 @@ command: [
 | "Print" "Ltac2" reference      (* ltac2 plugin *)
 | "Locate" "Ltac2" reference      (* ltac2 plugin *)
 | "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
+| "Ltac2" "Compile" LIST0 reference      (* ltac2 plugin *)
 ]
 
 reference_or_constr: [

doc/tools/docgram/orderedGrammar

@@ -964,6 +964,7 @@ command: [
 | "Print" "Ltac2" qualid      (* ltac2 plugin *)
 | "Locate" "Ltac2" qualid      (* ltac2 plugin *)
 | "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
+| "Ltac2" "Compile" LIST0 qualid      (* ltac2 plugin *)
 | "Hint" "Resolve" LIST1 [ qualid | one_term ] OPT hint_info OPT ( ":" LIST1 ident )
 | "Hint" "Resolve" [ "->" | "<-" ] LIST1 qualid OPT natural OPT ( ":" LIST1 ident )
 | "Hint" "Immediate" LIST1 [ qualid | one_term ] OPT ( ":" LIST1 ident )

plugins/ltac2/g_ltac2.mlg

@@ -132,6 +132,8 @@ let opt_fun ?loc args ty e =
   | [] -> e
   | _ :: _ -> CAst.make ?loc (CTacFun (args, e))
 
+let recursive_att = Attributes.bool_attribute ~name:"recursive"
+
 }
 
 GRAMMAR EXTEND Gram
@@ -1057,3 +1059,8 @@ END
 VERNAC COMMAND EXTEND Ltac2PrintSigs CLASSIFIED AS QUERY
 | [ "Print" "Ltac2" "Signatures" ] -> { Tac2entries.print_signatures () }
 END
+
+VERNAC COMMAND EXTEND Ltac2Compile CLASSIFIED AS SIDEFF
+| #[ recursive = recursive_att ] [ "Ltac2" "Compile" reference_list(n) ] ->
+  { Tac2entries.perform_compile ?recursive n }
+END