Ltac2 Compile #17521
Ltac2 Compile #17521
Conversation
coqbot-app
bot
added
the
needs: full CI
plugins/ltac2/tac2compile.ml
Outdated
| (* TODO HACK!!! TODO get these values the proper way | ||
| (NB: we need engine for proofview, kernel for KerName.equal) *) | ||
| ["-I"; "/home/gaetan/dev/coq/coq/_build/default/plugins/ltac2/.ltac2_plugin.objs/byte"] @ | ||
| ["-I"; "/home/gaetan/dev/coq/coq/_build/default/engine/.engine.objs/byte"] @ | ||
| ["-I"; "/home/gaetan/dev/coq/coq/_build/default/kernel/.kernel.objs/byte"] @ |
There was a problem hiding this comment.
@coq/build-maintainers what is the correct way to get these paths?
I see native compile gets passed -nI but while that's OK for a kernel feature it's not so nice for a plugin.
There was a problem hiding this comment.
As of today we have no way to get these paths, there are some hacks (native relies on a really wild one, see Nativelib.get_load_paths) but I recommend against extending those.
I think that if a plugin (like quickchick or ltac2) need an OCaml compilation context we should extend the plugin API properly to accommodate so, there are a couple of designs, IMHO it makes sense that the compilation request is pushed to the upper layer schedulers, but YMMV here.
Also, if plugins want to cache things (beyond what libobject provides) we should provide them proper API, otherwise maintenance will be hard.
There was a problem hiding this comment.
I think that if a plugin (like quickchick or ltac2) need an OCaml compilation context we should extend the plugin API properly to accommodate so, there are a couple of designs, IMHO it makes sense that the compilation request is pushed to the upper layer schedulers, but YMMV here.
I don't know what this means.
Also, if plugins want to cache things (beyond what libobject provides) we should provide them proper API, otherwise maintenance will be hard.
I'm not caching anything in this PR, everything goes to /tmp
There was a problem hiding this comment.
I don't know what this means.
What it is that you don't understand?
There was a problem hiding this comment.
What are the "couple of designs"? (Maybe "I don't know what to do with what you said" is more accurate than "I don't know what this means")
There was a problem hiding this comment.
I see, thanks. I'll try to explain a bit what I mean.
So indeed our case is that the plugins are per-sentence (or per-tactic) but want to access some more global state, in this case a compilation context, terminology we use in some build systems to denote the things that are needed to compile a file, this includes not only the flags, but libraries that have to be in place, etc...
So I see two possibilities:
- we pass to plugins the ocaml context, and they do the call to ocaml themselves
- we pass to plugin a callback so they can request the compilation of a file, and the callback returns the file location
Each approach has (in my view) its own drawbacks and advantages. The first one is more low-level, but is way less flexible. The second one (which I lean towards) is easier to use but gives less control to the plugins (which maybe is a good thing).
Common to both approach is other problem that we should eventually tackle: in both cases the commands actually involve some async execution (of a compiler). While this can be handled (at least in Unix OS) by doing synchronous IO, IMHO that's not so nice, and it would be nice for the vernacular interpretation to allow async commands (for example Require could be async, triggering also .vo compilation, call to smt solvers, etc...)
Does this make more sense?
There was a problem hiding this comment.
The TL; DR answer to your original question is: "we don't a way to pass such flags. We could do like native, and set some global flag, or update the plugin API to pass the missing stuff"
There was a problem hiding this comment.
So I see two possibilities:
In the second case, whatever layer owns the callback still needs access to the ocaml context right?
So regardless of if the ocaml context lives below or above plugins, my question is how do I get it?
There was a problem hiding this comment.
Ah, I see what you mean, for now Coq is using two ways:
- calling ocamlfind to get it, as done in
coq_rules.ml:findlib_plugin_flags, basicallyFindlib.package_directory. nativelib.mlwill callBoot.Env.native_cmi, which is way more hacky.
Neither method does guarantee that the libraries will be actually already built, so you gotta be a bit careful with the timing of the call.
| let include_dirs () = | ||
| (* TODO make this work in -boot / dev shim mode *) | ||
| let open Boot.Env in | ||
| let env = init () in | ||
| (* engine for Proofview, kernel for Names *) | ||
| List.map (fun x -> Path.to_string (native_cmi env x)) | ||
| [ "kernel"; "engine"; "plugins/ltac2" ] |
There was a problem hiding this comment.
This works with an installed Coq on my machine.
As noted in the comment it doesn't work if you want to use in the stdlib (-boot) or with the dev shims.
There was a problem hiding this comment.
at least it's not some hardcoded paths ;)
There was a problem hiding this comment.
SkySkimmer
added
needs: changelog entry
| let a := constr:($x + ltac:(exact $y)) in | ||
| constr:($a + ltac2:(let y := z in exact $y)). | ||
|
|
||
| Set Printing Ltac2 Extension Used Variables. |
There was a problem hiding this comment.
This is just for debug, do we want to keep it?
SkySkimmer
added
request: full CI
coqbot-app
bot
removed
request: full CI
|
Did the no compilation mode change? |
| Compiled code currently does not respect :flag:`Ltac Profiling` and | ||
| :flag:`Ltac2 Backtrace`. |
There was a problem hiding this comment.
I expect it will not play nicely with the debugger, either, when that becomes available. But not an issue for today.
|
🏁 Bench results: 🐢 Top 25 slow downs🐇 Top 25 speed ups |
|
While I think the ability to compile to OCaml is the natural future of Ltac2, the limitations of this PR makes me think it should be an effort with some precise planning. At the same time the original perf problem seems to be about finding a variable in a term, and one can surely provide this feature as a builtin, and that is way simpler than compiling arbitrary code. In a sense I've mixed feelings about solving that problem with this PR. |
coqbot-app
bot
added
the
needs: full CI
Doing that for every feature does not sound simple at all to me. |
SkySkimmer
added
kind: feature
|
At the very least this feature should be really opt-in, because we can break all kind of soundness invariants with it. I think it deserves some serious discussion before potentially merging. |
|
It is certainly optin, but what soundness invariants are you thinking about? |
Agreed. Further thoughts:
|
SkySkimmer
force-pushed
the
tac2compile
branch
2 times, most recently
from
0241dc8
to
11a23e2
Compare
github-actions
bot
added
the
needs: rebase
coqbot-app
bot
removed
the
needs: rebase
Offline we discussed that compilation does not use Obj.magic or other ocaml nontypechecking features, so even with the possibility of compiler bugs it should still break less invariants than eg Coq module application (which doesn't check Ltac2 types) |
The core API makes it possible to register a `valexpr` for each `ltac_constant`. For functional `ltac_constant` (the vast majority) this will be a closure, which in valexpr are represented as arbitrary OCaml closures. This allows arbitrary compilation schemes, eg - dynlinked OCaml code as in coq#17521 (like native_compute) - compiling to the VM eg `let code = compile expr in mk_closure arity (fun args -> interpret code args)` - partially evaluating the tacexpr and sending it back to the normal evaluator `let e = partial_eval e in mk_closure arity (fun args -> interp (TacApp (e, args))` and any other scheme someone might come up with. We also expose some convenient APIs.
|
After discussion we will avoid committing to this particular compilation model and instead expose the hook APIs to make it possible as a separate plugin (non coq-core for now) |
This will be useful for compilation, because it will need to rebuild the interpretation env to interp extensions.
The core API makes it possible to register a `valexpr` for each `ltac_constant`. For functional `ltac_constant` (the vast majority) this will be a closure, which in valexpr are represented as arbitrary OCaml closures. This allows arbitrary compilation schemes, eg - dynlinked OCaml code as in coq#17521 (like native_compute) - compiling to the VM eg `let code = compile expr in mk_closure arity (fun args -> interpret code args)` - partially evaluating the tacexpr and sending it back to the normal evaluator `let e = partial_eval e in mk_closure arity (fun args -> interp (TacApp (e, args))` and any other scheme someone might come up with. We also expose some convenient APIs.
|
We will do #17696 instead |
The core API makes it possible to register a `valexpr` for each `ltac_constant`. For functional `ltac_constant` (the vast majority) this will be a closure, which in valexpr are represented as arbitrary OCaml closures. This allows arbitrary compilation schemes, eg - dynlinked OCaml code as in coq#17521 (like native_compute) - compiling to the VM eg `let code = compile expr in mk_closure arity (fun args -> interpret code args)` - partially evaluating the tacexpr and sending it back to the normal evaluator `let e = partial_eval e in mk_closure arity (fun args -> interp (TacApp (e, args))` and any other scheme someone might come up with. We also expose some convenient APIs.
This makes the example from #10107 (comment) take 0.025s instead of 0.15s (using
Ltac2 Compile find). Compilation time is about 0.040s.TODO before merge:
I guess this mostly works now
Future work:
with_framein some places)Ltac2 Compile foo. Ltac2 Compile foo.will compile twice)