Ahead of time compilation

[SkySkimmer]

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.

[JasonGross]

For a first pass solution to this, can the compiled blobs be saved in the .vo file?

I'm interested in using the compiler in the rewriter and Fiat Crypto in a way that's transparent for clients, so I'm quite interested in being able to set up ahead of time compilation for rewriter reification.

Maybe @ejgallego has ideas for dune design?

[ejgallego]

I guess the first to determine here is if the file-level granularity will be good for your use case.

Ahead of time can be costly when compared to JIT, but YMMV.

I don't think Dune requires any special stuff, just to add the corresponding rules which are of the form {deps} -[action]-> {targets} ; what we do for coqnative should work fine.

I am more interested in finer-grained JIT designs, where we have a dynamic dependency graph inside an incremental computing engine. But to implement this you need something like coq-lsp / Flèche.

Happy to tell more about how I see this working, but roughtly:

• Coq vernaculars can offer an optional "JIT" phase
• Then some heuristics or fixed strategy determines whether for certains objects, we want to run the compile phase or not
• Note that everything is memoized so we will cache the JIT phase.

In this setting ahead-of-time is a) always running the compile phase + b) persisting the cache in some form.

[Janno]

Has anything changed here? What are the current blockers for AOT compilation?

We have a lot of files that significantly benefit from compiling our Ltac2 code but given the amount of code we have usually it does not pay off to compile it in every file.