Stream: Coq devs & plugin devs

Topic: The writing is on the wall


view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 00:02):

https://github.com/ocaml/ocaml/pull/10831

view this post on Zulip Ali Caglayan (Jan 11 2022 at 10:00):

I guess the obvious place to try it is the STM. IIRC there were some changes/cleanups to the STM that we wanted to carry out first however? Do we have any other places it might be applicable?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 10:25):

The STM can't profit from this without a rewrite, and there are other parts of Coq that would need significant work too due to global shared state.

But there is a much more pressing problem, and it is that VM / native won't work in 5.0 at all.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 10:25):

Coq, with those disabled, seems to work fine for now on the limited testing multicore devs have done in my multicore branch

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 10:42):

Why would VM not work with OCaml 5.0?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 10:42):

It requires some changes w.r.t. closure representation IIRC

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 10:44):

speaking of the VM, while I have your attention @Guillaume Melquiond https://github.com/coq/coq/pull/12640 was discussed at the last weekly call but you weren't there

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 10:45):

My opinion has not changed. State threading is an awful paradigm and it has been a never-ending source of bugs in Coq already.

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 10:46):

yes, but this is not the goal of the PR

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 10:46):

As for the change to closure representations, it was performed a few years ago already.

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 10:46):

the goal of the PR is to be able to make the VM state local and persistent

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 10:47):

Yes, but you are doing it using state threading and I cannot agree to it.

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

pff

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

if I use a reference passing will you agree to merging it ASAP?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 10:48):

this stuff will be needed if we want a multicore-capable VM notably

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 10:49):

Yes, I will agree.

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

tope-là, expect it in a couple of minutes

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 11:35):

Guillaume Melquiond said:

Why would VM not work with OCaml 5.0?

Last time we tried it was using "private" stuff from the GC, but the code on both sides has changed considerably, my branch provides a point if someone is interested in trying to compile the C code again.

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 11:40):

The GC might have changed considerably, but as far as the interpreter is concerned, there is nothing worrying. I participated in the review of the changes to the OCaml interpreter, and there is no reason it will be harder to adapt the Coq interpreter. Sure, it will not compile out of the box, but nothing that cannot be solved by adding #define Alloc_small at the start of the file to account for the new argument to the macro.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 11:43):

Even if the VM fix only takes a few person days, native seems that will require significant engineering time.

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 11:44):

Sure, but I never talked about native.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 11:49):

Guillaume Melquiond said:

Sure, but I never talked about native.

I did

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 11:50):

Note that I did not make an estimate of effort, I just wrote that for now, they don't work at all

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 11:51):

So today we have lost the ability to run Coq with OCaml master, which I ensured was possible quite a long time ago

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:02):

in the meantime we could make it easier to allow compiling Coq without native

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 12:04):

Compilation is not the issue. As long as you do not call native_compute, it should work just fine.

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

I'm pretty sure the infamous set_tag function was removed

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

so Coq won't compile on OCaml 5.0

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

(notwithstanding the other calls to Obj and friends that might have changed)

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 12:05):

Still there:

external set_tag : t -> int -> unit = "caml_obj_set_tag"
  [@@ocaml.deprecated "Use with_tag instead."]

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:06):

interesting, they don't plan to remove if from the 5.0 API then?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 12:06):

Guillaume Melquiond said:

Compilation is not the issue. As long as you do not call native_compute, it should work just fine.

It is an issue, to start with, due to static initializers in native coqc will just segfault

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:07):

hm, this precise part was tweaked recently though

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 12:07):

Are you guessing @Guillaume Melquiond or have you actually tried?

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 12:07):

I am guessing. As you said yourself, Coq does not compile with OCaml trunk.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 12:11):

Pierre-Marie Pédrot said:

hm, this precise part was tweaked recently though

I actually saw it, but was not enough to fix the problem, a couple more remained, I have a tree that tried to fix it tho

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 12:12):

I don't have the time these days to experiemnt, but I have spent quite some time messing with Coq and multicore so if anyone would like to go ahead I have git branches and notes around

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 12:12):

A good start is the branch used in sandmark

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2022 at 12:13):

The diffs show everything that is broken

view this post on Zulip Enrico Tassi (Jan 11 2022 at 12:51):

What is the problem with native? I did port Elpi to 4.12+domains since it did segfault, but the only offender was the GC (I was reading the value of pointers, I guess I was messing the "domain" part of them). Using obj.magic and the like is just fine (I mean, if it was reasonable it still it).

What does native do which is unsafe? @Maxime Dénès ?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:52):

Representation of accumulators as closures with tag 0

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:52):

it's a problem with two constraints that can only solved that way in OCaml

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:52):

first constraint is that the accumulator is a function, because we don't want to wrap all applications in our own version of apply

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:53):

second constraint is that we can have efficient pattern-matching over accumulators

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2022 at 12:53):

in OCaml we can't pattern-match on the tag of a value directly so we hack this by setting the tag of accumulators to 0 by convention

view this post on Zulip Enrico Tassi (Jan 11 2022 at 12:54):

so you are saying that we could de-optimize it a little

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

de-optimizing is catastrophical

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

it's like ten times as slow or so, hence with overheads taken into account not even clear to be competitive with the VM

view this post on Zulip Enrico Tassi (Jan 11 2022 at 12:59):

You are are sayin that adding a | x when is_closure x -> to the matches makes it 10 times slower?

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

yes

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

tried and retried

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

even with is_closure carefully written in C

view this post on Zulip Enrico Tassi (Jan 11 2022 at 13:00):

How can it be? I expect most of the times you don't match an accumulator

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

yes but it's always called because that's the first thing you test

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

I would have expected branch prediction to be clever, but no

view this post on Zulip Enrico Tassi (Jan 11 2022 at 13:01):

hum, which is the tag of closures?

view this post on Zulip Enrico Tassi (Jan 11 2022 at 13:02):

why should it be the first case?

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

247

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

not first lexically, first as in we must check that the argument is an accumulator before doing anything

view this post on Zulip Enrico Tassi (Jan 11 2022 at 13:03):

Hum, so it is not match Obj.magic thing_which_may_be_accu with K1 ... | K246 .. | x when is_closure x -> .. ?

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:01):

Unfortunately, you need at least one extra constructor for the branch x when is_closure x to be relevant, and the tag of this constructor needs to be ignored by OCaml. (Otherwise, the branch will be compiled to K0 ... when is_closure x, which does not have the correct behavior.) The only case where it works (because OCaml's standard library relies on it) is when the remaining constructor is the only non-constant constructor. But that is not true for Coq; there usually are lots of block constructors.

view this post on Zulip Gaëtan Gilbert (Jan 11 2022 at 14:07):

because OCaml's standard library relies on it

How's that?

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:17):

Cf CamlinternalOO.method_impl.

view this post on Zulip Gaëtan Gilbert (Jan 11 2022 at 14:23):

the Closure _ as clo is a actually a value with closure_tag?

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:23):

I see thanks for the explanations. So it seems @Pierre-Marie Pédrot tried if is_closure x then .. else match x with K1 ... Did you also try K247 of Obj.t? (I guess this is what you meant by "our own apply")

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

"our own apply" means that we compile function types to a sum type Accu of accu | Fun of Obj.t and we dispatch depending on the tag

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

You can't write the K247 hack because this will fail at compile time

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

OCaml will tell you there are too many constructors in the type

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:25):

ok, that is what I meant, add a Fun case

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:26):

And that is too much space overhead?

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:27):

Gaëtan Gilbert said:

the Closure _ as clo is a actually a value with closure_tag?

Yes.

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

@Enrico Tassi this is a catastrophe as well

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

we need to reimplement the caml_apply dynamic dispatch in our own version of the runtime essentially

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:30):

By the way, this whole discussion is kind of moot, because Gabriel's patch for unboxed constructors is ready, which will solve our issue.

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:30):

ah ah ah, LOL

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:30):

but I've learnt some stuff ;-)

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

I am really unsure this will work

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

unboxed constructors, that is

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

because we gladly mess with the type system and this feature is typed-directed

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

expect trouble ahead

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

we're really playing with fire in the native compiler with Obj.magic but nobody seems to care

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:32):

It is also moot partially moot because IMO we gain zero moving to multicore, so we lose very little to stay on 4.13 for a while.

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:32):

Actually, we will not have to mess with the type system anymore. We will just systematically add a constructor Accu of t -> t to every inductive type.

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

@Guillaume Melquiond yes we do, because of large dependent elimination

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

how would you translate a function of type forall b : bool, if b then nat else nat -> nat?

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

the target of native compilation (and extraction, for that matter) is fundamentally untyped

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:34):

It is already a function, you do not need to translate it. The issue is with inductive values, not functions.

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

my point is that we still need to sprinkle Obj.magic everywhere

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 14:35):

Sure, but we will no longer lie. When doing match Obj.magic, the list of constructors will exactly match the actual constructors.

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

as a famous OCaml dev whose name starts with Xavier and ends with Leroy would say: "repeat after me, Obj.magic is not part of OCaml"

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

right

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:35):

This is bullshit

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

what's bullshit? that Obj.magic is not part of OCaml ?

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

some people in the Linux kernel also have strong opinions about what C should be, and it's not what the standard says

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:36):

yes, because it is.

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

... until you start using flambda and then any optimization breaks your code ?

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

we can't advocate for specs and formalizations on the one hand and blatantly ignore such issues on the other

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:37):

it's a mantra people akin to strong types repeat... it does not make it true. of course you have to use it knowing what you are doing.

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

... and I repeat, until the compiler understands that what you're doing is wrong

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:39):

and use is only when necessary, but the whole bullshit about optimized one constructor GADTS just proves my point (the ones that looks like type theory Id).

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

:shrug:

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:40):

The type system is inherently incomplete, and can't be as smart as you want... so sometimes you cheat.

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:40):

It is the reality

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

but then you need a semantic model of your runtime

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:45):

well, we have an operational one with a changelog... it is not too bad

view this post on Zulip Enrico Tassi (Jan 11 2022 at 14:54):

Also, my ocaml code broke more times in its safe-and-sound part, than it its unsafe parts. Multicore is actually the very first time I have to change some unsafe code because it really became unsafe. I still recall the sound change that flipped the arguments of some set/map API, which started to iterate on the other set/map and made my code compile fine but never terminate... It's life

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 15:00):

My favorite example is the time (hopefully past) when when clauses were actually unsound.

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

I can confirm all these explicit encodings add a catastrophic overhead. I tried them during my thesis.

view this post on Zulip Maxime Dénès (Jan 11 2022 at 16:31):

Guillaume Melquiond said:

By the way, this whole discussion is kind of moot, because Gabriel's patch for unboxed constructors is ready, which will solve our issue.

Is there an OCaml PR?

view this post on Zulip Maxime Dénès (Jan 11 2022 at 16:32):

I don't think we need to panic anyway. In the worst case, we'll remove the native compiler until somebody finds the time to implement one that targets a lower level language.

view this post on Zulip Guillaume Melquiond (Jan 11 2022 at 17:20):

I am not sure there is an actual pull request yet. There is an RFC and a few published papers about it.

view this post on Zulip Paolo Giarrusso (Jan 11 2022 at 18:30):

@Enrico Tassi I'd expect you want a real semantic model like in RustBelt/NuPRL, an operational one is too cumbersome to reason about... but the bigger problem is that you might need a contract for the optimizer (and for undefined behavior?) similar to the C/C++ standard (or the WIP work on Rust Undefined Behavior by @Ralf Jung)

view this post on Zulip Paolo Giarrusso (Jan 11 2022 at 18:33):

while the C and C++ standard have lots of accidental complexity, supporting low-level operations together with a high-level invariants (that an optimizer relies on) has lots of essential complexity (Robbert Krebbers's PhD thesis explains that nicely)

view this post on Zulip Enrico Tassi (Jan 11 2022 at 19:29):

If I had to reason formally about that code, sure. What I meant is that we have one implementation which is known and documented, it is not like relying on undefined behavior every implementation has the freedom to implement differently. For that implementation many uses of Obj make sense, others don't. I'm not saying you must use the unsafe feature at all costs, just that pretending it has no practical use or reason to exist is, well, bar sport (PMU for the french) discussion (at least, this is my reading of "is not part of the ocaml language").


Last updated: Feb 06 2023 at 18:03 UTC