This Coq plugin provides a command Ltac2 Compile tacs which compiles
the given Ltac2 definitions using OCaml.
This provides large speedups (time divided by 4 or more) in computation heavy tasks (tasks which mostly spend their time in OCaml-implemented tactics are not affected).
See eg https://gitlab.com/coq/coq/-/jobs/4444514347 (significant fixes and optimizations have happened since that bench).
Load the plugin, then call Ltac2 Compile on the tactics you care about, for instance:
Ltac2 Compile Array.get Array.set.Evaluation will then use the compiled code instead of the Ltac2 interpreter for these tactics.
Print Ltac2 indicates whether a given tactic has been compiled.
By default the dependencies (eg Array.iter_aux) are also compiled.
If a dependency is a mutable tactic
This can be disabled with the attribute #[recursive=no].
The attribute is provided for testing and debugging purposes. Users
should note that when disabling the automatic dependency inference,
providing the tactics in dependency order provides significantly
better performance (eg Ltac2 Compile Array.iter_aux Array.iter is
better than the opposite order).
Compilation is local to the current module or section. This means
compilation cannot be shared between .v files.
Workers (async proofs, par:) do not use the compilation results.
This limitation should eventually be lifted.
Mutable tactics cannot be compiled. In recursive mode if a dependency
is mutable its compilation is skipped and warning
tac2compile-skipped-mutable is emitted (its dependencies are still
compiled).
This limitation may be expected to be permanent.
Quotations such as constr:() do not analyze their free variables, so
they need the entire Ltac2 environment. This may prevent GC or cause
slowness in large environments. This can be worked around using a side definition: instead of
Ltac2 footac many things x y z := stuff constr:(foo $x).do
Ltac2 footac_aux x := constr:(foo $x).
Ltac2 footac many things x y z := stuff (footac_aux x).The quotation in footac_aux does not need to be analyzed to know
that it only has access to x.
There are no plans to lift this limitation currently, but it may be done if there are compelling cases (currently the performance impact of needing the entire environment is unknown).
The Ltac2 Backtrace and Ltac Profiling options are ignored by
compiled tactics, so backtraces and profiles will be incomplete when
using compilation.
This limitation will be lifted.
The compilation of matches using string patterns or open constructor
patterns may show exponential behaviour when combined with deep
patterns or "or" (|) patterns.
Even shallow matches are linear whereas the interpreted mode is logarithmic. As such matching over many specific open constructor (eg errors) should be avoided.
There are no plans to lift this limitation currently. Lifting it for shallow matches of open constructors could be done if there is a compelling case (it's not clear how many constructors need to be matched on before there is a noticeable impact).
identify and implement further optimizations
share compilation across files
handle backtraces
JIT evaluator (instead of using the interpreter, compile the given expression and run the result)? Bench https://gitlab.com/SkySkimmer/coq/-/jobs/5159008108 was not very promising, consider again once ahead of time compilation is done.