skyskimmer/coq-ltac2-compiler

Compiler for Ltac2

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).

Usage

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.

Dependency handling

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).

Limitations

Compilation is local

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.

No mutables

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 use the full Ltac2 environment

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).

No backtraces

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.

String and open constructor patterns are suboptimal

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).

Roadmap (in no particular order)

• 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.

coq-ltac2-compiler's Issues

Mutable definitions lead to dynlink errors

The README says mutable definitions are not compiled. IIUC everything should still work, it would just be "slower". Is that correct?

Here's my test case:

From Ltac2 Require Import Ltac2.
Ltac2 mutable mut : unit := ().
Ltac2 test () := match mut with () => () end.

From Ltac2Compiler Require Import Ltac2Compiler.
Ltac2 Compile test.
(*
Warning: Skipped compilation of mutable definitions mut [tac2compile-skipped-mutable,ltac2,default]

Dynlink error: execution of module initializers in the shared library failed: File "plugins/ltac2/tac2env.ml", line 79, characters 2-8: Assertion failed
*)

I am running 8.18.0.

I had mixed success with reproducing my original, much larger example. Ltac2 Compile would succeed if I did it in the same file where the mutable definition lives, but not if I ran it in another file. The example above replicates the error message but isn't derived from my actual example. I hope it's the same underlying issue.

OCaml does not support unicode binders?

Thanks for fixing #4 so quickly! I managed to compile quite a few functions already (so far with a 10% speedup in the one test file I am looking at) but I got stuck again at the next binder error:

File "/tmp/tac2compile_02742a/fdc8e1b.ml", line 2399, characters 30-31:
2399 |                         (let φ =
                                     ^
Error: Illegal character (\134)

Syntax error in generated code (need to avoid ocaml keywords)

File "/tmp/tac2compile_6802a9/f6fbe42.ml", line 5843, characters 47-52:
5843 |       ((make_app1_kn102_f__ preWait p) >>= fun class ->
                                                      ^^^^^
Error: Syntax error

The corresponding Ltac2 code is:

    let class := make_app1 preWait p in

I think class is restricted keyword: https://v2.ocaml.org/releases/4.07/htmlman/manual049.html

Handle backtraces and profiling

There's a question of how much having the trace handlers will cost, hopefully not much.

Ahead of time compilation

Not sure how to handle this.

As long as the compiler is separate from the main ltac2 plugin we need to be able to compile files which did not load the compiler.

We could imagine having a separate executable (like coqnative), or add some Compile File command to the plugin.

The compilation results then need to be handled by the build / install system (provide some Makefile template to include in Makefile.local for coq_makefile users? what about dune?)

Then they need to be detected and loaded when executing ltac2 tactics.

Compilation produces code in incorrect order

I've found a particularly confusing bug and it took me a while to minimize and reproduce. Luckily the effort paid off. I think the bug is in evaluation order but I can only reproduce it with Ltac2 externals that manipulate global state, not with Ltac2's own mutable references so I am not entirely sure how about what's happening.

Please have a look at https://github.com/Janno/ltac2-compiler-bug-repro. I've only tested the code with 8.18 but I hope it still works with master. dune build should build everything. I didn't manage to write a working _CoqProject file so stepping through it in emacs doesn't work.

The code exposes a OCaml reference to an integer that is incremented and decremented in a stack-like fashion (i.e. decrementing only works if the argument provided is the result of the last increment). The problem is in Ltac2 test2. In > [ ... | .. push ..], the push is executed before the tactic for the first subgoal is finished. This can be prevented by adding a printf before push, as is done in Ltac2 test1.

Incorrect compilation of Array.empty

Require Import Ltac2Compiler.Ltac2Compiler.
From Ltac2 Require Import Array.
Ltac2 test () := Array.empty.
Ltac2 Eval Array.length (test ()).
Ltac2 Compile Array.empty.
Ltac2 Eval Array.length (test ()). (* Fails with anomaly in `Tac2ffi.to_array` *)

reported by @Janno

Assertion failed in `force_nontac_expr`

I am still trying to make progress on compiling our automation and managed to minimize another failure:

From Ltac2Compiler Require Import Ltac2Compiler.
Ltac2 Compile apply_cancelx_instance.
Ltac2 beta_iota :=
  let x := { rBeta := true; rMatch := true; rFix := true; rCofix := true; rZeta := false; rDelta := false; rConst := [] } in x.
Ltac2 test () := Std.eval_lazy beta_iota.
Set Debug "backtrace".
Ltac2 Compile test.

The failure disappears when using

Ltac2 beta_iota :=
  { rBeta := true; rMatch := true; rFix := true; rCofix := true; rZeta := false; rDelta := false; rConst := [] }.

Unfortunately the backtrace is just pure confusion:

Error: Anomaly "File "src/tac2compile.ml", line 624, characters 2-8: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Unicode.next_utf8 in file "clib/unicode.ml", line 162, characters 16-34
Called from Unicode.ident_refutation.aux in file "clib/unicode.ml", line 267, characters 26-39
Called from Unicode.ident_refutation in file "clib/unicode.ml", line 271, characters 16-21
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml" (inlined), line 212, characters 16-41
Called from Vernacinterp.interp.(fun) in file "vernac/vernacinterp.ml", line 226, characters 54-111
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from NewProfile.profile in file "lib/newProfile.ml" (inlined), line 151, characters 32-36
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml" (inlined), line 226, characters 15-115
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 226, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2185, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 965, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2327, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2424, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 79, characters 29-50
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 153, characters 6-46

Raised at Exninfo.iraise in file "clib/exninfo.ml" (inlined), line 79, characters 4-11
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 164, characters 4-34
Called from Util.try_finally in file "lib/util.ml" (inlined), line 140, characters 16-19
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 168, characters 2-166
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 168, characters 2-166
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml" (inlined), line 144, characters 6-32
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 168, characters 2-166
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 433, characters 17-62

I am working on a slightly adapted fork of the main branch to make it work in 8.18 so the line numbers could be a little off.

Experiment with optimization flags