Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ahead of time compilation #7

Open
SkySkimmer opened this issue Oct 23, 2023 · 3 comments
Open

Ahead of time compilation #7

SkySkimmer opened this issue Oct 23, 2023 · 3 comments
Labels
enhancement New feature or request

Comments

@SkySkimmer
Copy link
Owner

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.

@SkySkimmer SkySkimmer added the enhancement New feature or request label Oct 23, 2023
@JasonGross
Copy link

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
Copy link

ejgallego commented Oct 24, 2023

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
Copy link

Janno commented Aug 30, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

4 participants