@Pierre-Marie Pédrot You mentioned that it might be possible to use malfunction as a target for native code. This would get rid of our typing/Obj.magic issues with OCaml presumably.
cc @Maxime Dénès
Yes, I am an ardent advocate for this (and it's not that hard). The problem with malfunction is that it's currently a one-man side project.
We could rely on it and if it causes issues in the future vendor (or essentially fork) it ourselves?
Or maybe maintaining it is a little too optimistic.
I think we could come with a agreement with the guy behind it. Maintaining is not very hard, but AFAIK malfunction is very sensitive to OCaml versions. Which is fine since we ourselves usually have problem supporting the latest OCaml versions...
FWIW the certified extraction project from metacoq is probably going to rely on (at least the spec of) malfunction.
Looking at the repo, they seem to be preparing for OCaml 5.0, so I am assuming they will keep support from 4.14 for time to come.
An untyped ML using the OCaml toolchain seems to be something that is part of many different dependency chains.
There is an experimental backend for idris by the same person: https://github.com/stedolan/idris-malfunction
(Stephen Dolan is not a random guy from the internet, also.)
Shall we try to do an experiment then? How much work do you think it is to set up?
Last time I tried I suffered from issues with the legacy makefile. Maybe we should just wait for its removal.
Maybe the OCaml version bump helped, also.
We can probably still experiment with it making sure only the dune makefile works.
(BTW, half of the stuff in the malfunction repo is not needed. The important part is just the stable API for OCaml compiler-libs.)
Not that it matters for the experiment, but we could always ask for the API to be in a separate package.
Actually I don't think that even matters, it is a completely tiny package anyhow.
It does depend on a bit of stuff.
So instead of building OCaml terms we instead build terms in the AST of mlf and use the mlf compiler to run these?
Up to annoying technical details, yes;
When OCaml is being compiled, the typing can block the inlining right? Does mlf just have everything inlined or what?
I'm a little confused since mlf is supposedly the intermediate state of the OCaml compiler right
AFAIU OCaml doesn't really rely on typing for optimizations.
But Obj.magic does affect things?
Or is that only with flambda?
Historically the OCaml compiler was very conservative, you could predict the output by just looking at the code.
Nowadays with flambda enabled you can get a lot of fancy optimizations.
But that is the speed bump people are looking for when using native code I guess
flambda makes native compilation essentially useless because compilation times explode
(not that it's very usable already, but it's frankly worse)
For native compilation we want the dumbest compiler possible.
So is this another advantage of using mlf? flambda won't affect native anymore?
@Maxime Dénès even wanted to reimplement a standalone compiler at some point.
Was that the stuff about miniml?
flambda acts on the untyped treee
so malfunction is basically at the flambda level
(hence it wouldn't help)
what malfunction helps with is typing
Pierre-Marie Pédrot said:
AFAIU OCaml doesn't really rely on typing for optimizations.
When there are GADTs, the OCaml compiler relies on typing to guess when code is dead. And when using Flambda, the compiler uses typing to guess which words in memory blocks are constant.
Ok so flambda will still touch mlf code and make it untenable?
@Guillaume Melquiond that's not quite typing, these are annotations that are lower-level than typing.
Malfunction exposes this kind of data by providing flags to say that some data is immutable and stuff.
AFAIU the GADT optimizations happen before that pass.
There are other considerations in flambda that are not quite typing-based like function arities, purity of code, etc.
@Ali Caglayan probably
we can pass the lowest optimization levels still, it can't hurt
Indeed, shouldn’t -O0
just disable flambda and its performance costs?
Ali Caglayan said:
Not that it matters for the experiment, but we could always ask for the API to be in a separate package.
Why don't you want to generate malfunction sexp? That's basically a stable api
We could do that, I'm not against anything tbh
The advantage of that is of course you could leave the actual compilation of the malfunction source files to dune and benefit from cutoff, caching, and other goodies
Native files are transient (one is created, compiled, dynlinked, executed, on-the-fly whenever the native_compute
tactic is called). I don't think Dune is able to handle such files.
but you’re going to be rerunning the same tactic over and over no? Don’t you want to do the compilation step only once if possible?
The tactic takes whatever AST we have in the proof, translates it to native code, runs it, then reifies the result
I don't think it is possible to know what native_compute will actually do without having stepped through and checked the proof somewhat.
I could be wrong here, but you’re still going to be recompiling a lot of native code to run the tactic. Basically, what will happen if you add some unrelated definition to the .v file that uses native compute? You will need to generate the malfunction, compile it, and then run it.
If you let dune handle compilation, then the compilation step might be omitted in many cases
If you generated the same code with the tactic that is
Yes, native cmxs can be precompiled (and should be for any practical use), this is done for instance with the coq-native OPAM package.
Rudi Grinberg said:
I could be wrong here, but you’re still going to be recompiling a lot of native code to run the tactic. Basically, what will happen if you add some unrelated definition to the .v file that uses native compute? You will need to generate the malfunction, compile it, and then run it.
Coq does not do any detection of "unrelated definition". All the available definitions from the file are compiled.
@Rudi Grinberg even if the other problems were fixable, it seems coqc/coqtop would have to invoke dune. Even if they were started by dune. Would that even be possible?
Yes, we have an action plug-in for exactly that. It does not yet allow setting up rules - only requesting dependencies, but we would obviously improve it for that.
@Pierre-Marie Pédrot When we run the native code that gets generated, how do we pass the term around?
the Nativelib.rt1 and rt2 global refs
Are these terms pretty big? Could they be marshalled to a file easily?
These are OCaml values, they're not marshallable.
@Pierre-Marie Pédrot ping, now that we have finished the dune PR, shall we start planning this a bit?
@Pierre-Marie Pédrot Do you have time this week to sketch what needs to be done when moving the malfunction. Perhaps we can also discuss it in next weeks Coq call?
There is a huge prerequisite that needs to be cleared first and foremost, that is, Malfunction must actually exist. Indeed, Coq requires OCaml >= 4.09, while Malfunction requires OCaml < 4.09. And I have never heard (even unofficially) the OCaml developers state they were willing to bring back support for Malfunction in the future.
I don't really care about malfunction per se, I care about the small shim for compiler-libs that gives a stable API for miniML
worst case is that we maintain that ourselves
One of the reasons we need to start sorting this out now is because OCaml 5.0 will not allow us to do some of the hacks we rely on currently. Although it has been a while since I thought about the details.
Malfunction has been released for 4.14: https://github.com/stedolan/malfunction/issues/33
cc @Pierre-Marie Pédrot
From the readme:
Malfunction is a revolting hack, exposing bits of the OCaml compiler's guts that were never meant to see the light of day.
It looks very interesting. Not sure it qualifies to be used in Coq (as in trusted, in the TCB)
Famous quote by Xavier Leroy: "repeat after me, Obj.magic is not part of the OCaml language".
The current situation where we abuse the OCaml compiler with very untypable programs is way worse, I believe.
according to the doc, malfunction programs can go wrong. so what is the difference?
The difference is that the recent versions of OCaml can take advantage of types to perform optimizations. With Obj.magic everywhere we're playing on a minefield waiting for an optimization to go wrong. (Most notably, we already have the type of native values set to t = t -> t which might be problematic enough because it's just not true).
Malfunction is untyped, so we know precisely what we do. Garbage in, garbage out.
Does it mean that all type-driven optimizations are performed before reaching the compilation chain point where malfunction hooks in?
Malfunction operates on an untyped representation, i.e. basically our mini-ML. There are a few optimizations you can enforce at that level that are indirectly related to typing, like e.g. the fact that an expression is pure but that's about it. It will never perform a real type-directed transformation because it simply doesn't have access to that data.
has someone persuaded the OCaml people to keep Malfunction around? One might be hesistant to commit to Malfunction-based extraction in a project without long-term compiler support.
We're talking about native compute here, not extraction. On a related note, the metacoq people are working on targetting malfunction for their extraction process.
As for support, last time I've heard of it, the OCaml people don't want to expose a stable API for compiler libs, just as we keep breaking our own OCaml API in Coq.
If you look into the malfunction implementation though, it's really a thin compat layer and I'm convinced I could even perform the updates when new OCaml releases are published.
OK, but then do they offer something like Coq CI? Seems shaky if upstream's only position is: "this is unsupported" and caveat emptor
I don't think that the official position is "it's unsupported" otherwise why on earth would they release a compiler-lib package?
the official statement looks rather like:
This library is part of the internal OCaml compiler API, and is not the language standard library. There are no compatibility guarantees between releases, so code written against these modules must be willing to depend on specific OCaml compiler versions.
(from https://v2.ocaml.org/api/compilerlibref/Compiler_libs.html)
This looks pretty similar to our own promises about the OCaml API of Coq.
and the current strategy is more strongly unsupported
there may be a difference between:
Which one is Coq and which one is OCaml?
I think Coq['s ML API] is currently in the first category. I'm asking if we know something about where Malfunction may fall.
The only file I really care about in malfunction is https://github.com/stedolan/malfunction/blob/master/src/malfunction_compat.cppo.ml. Worst case, we can vendor it.
a recent example of "ambiguous APIs" and their consequences: https://github.com/bluez/bluez/commit/35a2c50437cca4d26ac6537ce3a964bb509c9b62#commitcomment-56028543
@Yannick Forster might say more on our dependency on malfunction, but from my point of view, it's unlikely that ocaml will e.g. remove lambdas from their Ast, which is what we (mainly) currently care about.
I didn't read the whole thread, but here are a couple of comments: Steven Dolan told me that his release cycle of Malfunction is "whenever somebody asks me to release again", and he is open to contributions, simplifications, etc. The initial goal of Malfunction was to serve as target for extraction from Idris. The Malfunction compiler can take as input an mli
file. I don't know what that means re type-directed optimisations, but for instance all optimisations happening at the flambda
layer will also be carried out when compiling from malfunction
Personally, I think that on the engineering side, we should first care about the problems that we already have, before solving the ones that may or may not happen. For research on Coq, it's a totally different story, of course. In terms of engineering, the real problem is not so much the hypothetical type-directed optimizations as the fact that we spit out generated code to a compiler that was not made for that.
I'm confident we can assign engineering resources when and if we see the problem coming, though. Which AFAICT is not the case today. And meanwhile, we have 2.6k open issues :)
We have a problem today. Native compilation is incompatible with OCaml 5.0.
And not because it requires a light porting. Precisely because we have to twist the arm of the OCaml compiler to implement accumulators.
So, this is really a chronicle of an announced death, much like the switch to findlib.
We can prepare for it, or ignore it until it blows in our face.
so the most likely thing is that malfunction is bundled with Coq? Or becomes a dependency like zarith?
I personally see two options: either we depend on it, or we vendor the small subset we depend on.
A good 3/4 of the code of malfunction is irrelevant for Coq
Looks like the license allows bundling/vendoring, albeit not without explicitly upgrading it:
license: "LGPL-2.0-or-later"
Pierre-Marie Pédrot said:
We have a problem today. Native compilation is incompatible with OCaml 5.0.
Oh, so I was missing context. This thread initially talked about "Obj.magic
issues". Will a switch to malfunction solve the OCaml 5.0 compatibility issue? How?
With malfunction you can write untyped pattern-matchings on arbitrary tags. With this you can decide that something is a closure, and by convention a closure in an inductive type should be an accumulator.
We can do this in OCaml with hackery, but all tests showed that this was catastrophical for performances.
In theory, this should be fine with malfunction because it reuses the same underlying table jump compilation.
I see. Do we have a deadline that we set for OCaml 5.0 support?
Not that I know of.
don't forget also that all extracted code that contains Pervasives
breaks with OCaml 5.0, so there may be quite a lot of other work (unrelated to native compilation) for full support
Extraction is a different beast, though. Not all Coq developments use extraction, and if you don't it doesn't matter that it's broken.
For native compilation, even deactivating it you face trouble.
I doubt we want half support of a given OCaml version...
Do we have the support project described somewhere, with the list of things that need to be done?
(or a collection of issues)
I think @Emilio Jesús Gallego Arias had a document on that somewhere.
We need to integrate that in the roadmap
I think I'll create a github project for that
Yes, sounds like the right tool
https://github.com/coq/coq/projects/55
I'll retroactively add some PRs to this
BTW given his interventions in the issue thread, Stephen Dolan, the author of Malfunction, seems to be aware of our half-baked plans to use it for various backends of Coq. Maybe we should chat a bit with him as well.
apparently the license for Malfunction is not LGPL-2.0-or-later as reported via opam, but LGPL-2.1-possibly-with-some-exception-like-OCaml. So already there, some question marks need to be ironed out for downstream packagers like in Debian
Last updated: Oct 13 2024 at 01:02 UTC