Stream: Coq devs & plugin devs

Topic: Using "malfunction" for native code


view this post on Zulip Ali Caglayan (May 13 2022 at 10:52):

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

view this post on Zulip Ali Caglayan (May 13 2022 at 10:59):

cc @Maxime Dénès

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 11:47):

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.

view this post on Zulip Ali Caglayan (May 14 2022 at 11:51):

We could rely on it and if it causes issues in the future vendor (or essentially fork) it ourselves?

view this post on Zulip Ali Caglayan (May 14 2022 at 11:53):

Or maybe maintaining it is a little too optimistic.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 11:54):

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

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 11:55):

FWIW the certified extraction project from metacoq is probably going to rely on (at least the spec of) malfunction.

view this post on Zulip Ali Caglayan (May 14 2022 at 11:56):

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.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 11:56):

An untyped ML using the OCaml toolchain seems to be something that is part of many different dependency chains.

view this post on Zulip Ali Caglayan (May 14 2022 at 11:57):

There is an experimental backend for idris by the same person: https://github.com/stedolan/idris-malfunction

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 11:58):

(Stephen Dolan is not a random guy from the internet, also.)

view this post on Zulip Ali Caglayan (May 14 2022 at 12:01):

Shall we try to do an experiment then? How much work do you think it is to set up?

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:03):

Last time I tried I suffered from issues with the legacy makefile. Maybe we should just wait for its removal.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:03):

Maybe the OCaml version bump helped, also.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:05):

We can probably still experiment with it making sure only the dune makefile works.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:05):

(BTW, half of the stuff in the malfunction repo is not needed. The important part is just the stable API for OCaml compiler-libs.)

view this post on Zulip Ali Caglayan (May 14 2022 at 12:07):

Not that it matters for the experiment, but we could always ask for the API to be in a separate package.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:12):

Actually I don't think that even matters, it is a completely tiny package anyhow.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:13):

It does depend on a bit of stuff.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:19):

So instead of building OCaml terms we instead build terms in the AST of mlf and use the mlf compiler to run these?

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:20):

Up to annoying technical details, yes;

view this post on Zulip Ali Caglayan (May 14 2022 at 12:26):

When OCaml is being compiled, the typing can block the inlining right? Does mlf just have everything inlined or what?

view this post on Zulip Ali Caglayan (May 14 2022 at 12:27):

I'm a little confused since mlf is supposedly the intermediate state of the OCaml compiler right

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:27):

AFAIU OCaml doesn't really rely on typing for optimizations.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:27):

But Obj.magic does affect things?

view this post on Zulip Ali Caglayan (May 14 2022 at 12:28):

Or is that only with flambda?

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:28):

Historically the OCaml compiler was very conservative, you could predict the output by just looking at the code.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:28):

Nowadays with flambda enabled you can get a lot of fancy optimizations.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:28):

But that is the speed bump people are looking for when using native code I guess

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:29):

flambda makes native compilation essentially useless because compilation times explode

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:29):

(not that it's very usable already, but it's frankly worse)

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:29):

For native compilation we want the dumbest compiler possible.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:30):

So is this another advantage of using mlf? flambda won't affect native anymore?

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:30):

@Maxime Dénès even wanted to reimplement a standalone compiler at some point.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:30):

Was that the stuff about miniml?

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:30):

flambda acts on the untyped treee

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:30):

so malfunction is basically at the flambda level

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:31):

(hence it wouldn't help)

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:31):

what malfunction helps with is typing

view this post on Zulip Guillaume Melquiond (May 14 2022 at 12:31):

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.

view this post on Zulip Ali Caglayan (May 14 2022 at 12:31):

Ok so flambda will still touch mlf code and make it untenable?

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:31):

@Guillaume Melquiond that's not quite typing, these are annotations that are lower-level than typing.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:32):

Malfunction exposes this kind of data by providing flags to say that some data is immutable and stuff.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:32):

AFAIU the GADT optimizations happen before that pass.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:33):

There are other considerations in flambda that are not quite typing-based like function arities, purity of code, etc.

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:35):

@Ali Caglayan probably

view this post on Zulip Pierre-Marie Pédrot (May 14 2022 at 12:35):

we can pass the lowest optimization levels still, it can't hurt

view this post on Zulip Paolo Giarrusso (May 14 2022 at 13:02):

Indeed, shouldn’t -O0 just disable flambda and its performance costs?

view this post on Zulip Rudi Grinberg (May 14 2022 at 16:11):

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

view this post on Zulip Ali Caglayan (May 14 2022 at 16:23):

We could do that, I'm not against anything tbh

view this post on Zulip Rudi Grinberg (May 14 2022 at 16:27):

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

view this post on Zulip Guillaume Melquiond (May 14 2022 at 16:29):

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.

view this post on Zulip Rudi Grinberg (May 14 2022 at 16:35):

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?

view this post on Zulip Ali Caglayan (May 14 2022 at 16:37):

The tactic takes whatever AST we have in the proof, translates it to native code, runs it, then reifies the result

view this post on Zulip Ali Caglayan (May 14 2022 at 16:39):

I don't think it is possible to know what native_compute will actually do without having stepped through and checked the proof somewhat.

view this post on Zulip Rudi Grinberg (May 14 2022 at 18:52):

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.

view this post on Zulip Rudi Grinberg (May 14 2022 at 18:53):

If you let dune handle compilation, then the compilation step might be omitted in many cases

view this post on Zulip Rudi Grinberg (May 14 2022 at 18:53):

If you generated the same code with the tactic that is

view this post on Zulip Pierre Roux (May 14 2022 at 19:00):

Yes, native cmxs can be precompiled (and should be for any practical use), this is done for instance with the coq-native OPAM package.

view this post on Zulip Guillaume Melquiond (May 14 2022 at 19:09):

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.

view this post on Zulip Paolo Giarrusso (May 15 2022 at 16:48):

@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?

view this post on Zulip Rudi Grinberg (May 15 2022 at 18:16):

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.

view this post on Zulip Ali Caglayan (May 24 2022 at 11:26):

@Pierre-Marie Pédrot When we run the native code that gets generated, how do we pass the term around?

view this post on Zulip Gaëtan Gilbert (May 24 2022 at 11:29):

the Nativelib.rt1 and rt2 global refs

view this post on Zulip Ali Caglayan (May 24 2022 at 11:34):

Are these terms pretty big? Could they be marshalled to a file easily?

view this post on Zulip Pierre-Marie Pédrot (May 24 2022 at 11:38):

These are OCaml values, they're not marshallable.

view this post on Zulip Ali Caglayan (Jul 12 2022 at 12:29):

@Pierre-Marie Pédrot ping, now that we have finished the dune PR, shall we start planning this a bit?

view this post on Zulip Ali Caglayan (Sep 07 2022 at 17:25):

@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?

view this post on Zulip Guillaume Melquiond (Sep 07 2022 at 17:53):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2022 at 18:23):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2022 at 18:23):

worst case is that we maintain that ourselves

view this post on Zulip Ali Caglayan (Sep 07 2022 at 20:27):

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.

view this post on Zulip Ali Caglayan (Sep 28 2022 at 17:18):

Malfunction has been released for 4.14: https://github.com/stedolan/malfunction/issues/33

view this post on Zulip Ali Caglayan (Sep 28 2022 at 17:18):

cc @Pierre-Marie Pédrot

view this post on Zulip Enrico Tassi (Sep 28 2022 at 19:43):

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.

view this post on Zulip Enrico Tassi (Sep 28 2022 at 19:44):

It looks very interesting. Not sure it qualifies to be used in Coq (as in trusted, in the TCB)

view this post on Zulip Pierre-Marie Pédrot (Sep 28 2022 at 21:54):

Famous quote by Xavier Leroy: "repeat after me, Obj.magic is not part of the OCaml language".

view this post on Zulip Pierre-Marie Pédrot (Sep 28 2022 at 21:55):

The current situation where we abuse the OCaml compiler with very untypable programs is way worse, I believe.

view this post on Zulip Enrico Tassi (Sep 29 2022 at 05:42):

according to the doc, malfunction programs can go wrong. so what is the difference?

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 07:33):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 07:34):

Malfunction is untyped, so we know precisely what we do. Garbage in, garbage out.

view this post on Zulip Enrico Tassi (Sep 29 2022 at 10:44):

Does it mean that all type-driven optimizations are performed before reaching the compilation chain point where malfunction hooks in?

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:49):

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.

view this post on Zulip Karl Palmskog (Sep 29 2022 at 10:51):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:53):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:54):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:55):

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.

view this post on Zulip Karl Palmskog (Sep 29 2022 at 10:55):

OK, but then do they offer something like Coq CI? Seems shaky if upstream's only position is: "this is unsupported" and caveat emptor

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:55):

I don't think that the official position is "it's unsupported" otherwise why on earth would they release a compiler-lib package?

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:56):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:56):

(from https://v2.ocaml.org/api/compilerlibref/Compiler_libs.html)

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 10:57):

This looks pretty similar to our own promises about the OCaml API of Coq.

view this post on Zulip Paolo Giarrusso (Sep 29 2022 at 10:57):

and the current strategy is more strongly unsupported

view this post on Zulip Karl Palmskog (Sep 29 2022 at 10:59):

there may be a difference between:

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 11:00):

Which one is Coq and which one is OCaml?

view this post on Zulip Karl Palmskog (Sep 29 2022 at 11:05):

I think Coq['s ML API] is currently in the first category. I'm asking if we know something about where Malfunction may fall.

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2022 at 11:09):

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.

view this post on Zulip Karl Palmskog (Sep 29 2022 at 11:09):

a recent example of "ambiguous APIs" and their consequences: https://github.com/bluez/bluez/commit/35a2c50437cca4d26ac6537ce3a964bb509c9b62#commitcomment-56028543

view this post on Zulip Matthieu Sozeau (Sep 29 2022 at 12:33):

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

view this post on Zulip Yannick Forster (Sep 29 2022 at 13:58):

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

view this post on Zulip Maxime Dénès (Sep 29 2022 at 16:28):

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.

view this post on Zulip Maxime Dénès (Sep 29 2022 at 16:30):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 12:54):

We have a problem today. Native compilation is incompatible with OCaml 5.0.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 12:55):

And not because it requires a light porting. Precisely because we have to twist the arm of the OCaml compiler to implement accumulators.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 12:56):

So, this is really a chronicle of an announced death, much like the switch to findlib.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 12:56):

We can prepare for it, or ignore it until it blows in our face.

view this post on Zulip Karl Palmskog (Sep 30 2022 at 13:00):

so the most likely thing is that malfunction is bundled with Coq? Or becomes a dependency like zarith?

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:01):

I personally see two options: either we depend on it, or we vendor the small subset we depend on.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:02):

A good 3/4 of the code of malfunction is irrelevant for Coq

view this post on Zulip Karl Palmskog (Sep 30 2022 at 13:04):

Looks like the license allows bundling/vendoring, albeit not without explicitly upgrading it:

license:      "LGPL-2.0-or-later"

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:05):

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?

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:06):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:06):

We can do this in OCaml with hackery, but all tests showed that this was catastrophical for performances.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:07):

In theory, this should be fine with malfunction because it reuses the same underlying table jump compilation.

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:08):

I see. Do we have a deadline that we set for OCaml 5.0 support?

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:09):

Not that I know of.

view this post on Zulip Karl Palmskog (Sep 30 2022 at 13:12):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:12):

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.

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:13):

For native compilation, even deactivating it you face trouble.

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:13):

I doubt we want half support of a given OCaml version...

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:13):

Do we have the support project described somewhere, with the list of things that need to be done?

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:14):

(or a collection of issues)

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:14):

I think @Emilio Jesús Gallego Arias had a document on that somewhere.

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:14):

We need to integrate that in the roadmap

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:16):

I think I'll create a github project for that

view this post on Zulip Maxime Dénès (Sep 30 2022 at 13:17):

Yes, sounds like the right tool

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:18):

https://github.com/coq/coq/projects/55

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:18):

I'll retroactively add some PRs to this

view this post on Zulip Pierre-Marie Pédrot (Sep 30 2022 at 13:24):

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.

view this post on Zulip Karl Palmskog (Sep 30 2022 at 16:27):

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