Stream: Coq devs & plugin devs

Topic: Coq-as-compiler


view this post on Zulip Karl Palmskog (Nov 10 2020 at 11:09):

was there a reason (besides lack of interest) that Coq-as-compiler via opam wasn't investigated before this? Or has it been? I found this from 2019: https://github.com/coq/opam-coq-archive/issues/595

view this post on Zulip Théo Zimmermann (Nov 10 2020 at 11:28):

I would say lack of resources (time) rather than lack of interest.

view this post on Zulip Théo Zimmermann (Nov 10 2020 at 11:28):

And Coq-as-a-compiler is only possible since opam 2.0 IIUC.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 13:11):

I'd say that the reason Coq is not following the compiler per switch strategy is that at least for OCaml is very very painful

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 13:11):

You need to compile with optimizing options? Re-install all your packages ...

view this post on Zulip Karl Palmskog (Nov 10 2020 at 13:11):

the proposal with coq-nativemeta-package does that as well, no?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 13:11):

Also native doesn't have some of the problems OCaml has, plus the compiler setup is quite experimental in OPAM itself

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 13:12):

yes, that's why I think it's a bad idea

view this post on Zulip Kenji Maillard (Nov 10 2020 at 13:17):

Emilio Jesús Gallego Arias said:

You need to compile with optimizing options? Re-install all your packages ...

Is there currently a better option with opam ? My current setup is one ocaml switch per version of Coq so I also recompile from scratch the ocaml compiler for each Coq version even if I already have it compiled on my machine...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 13:19):

I'm afraid there is nothing better in this sense, at least in OPAM 2.0, I dunno about upcoming 2.1 / 2.2 .

view this post on Zulip Karl Palmskog (Nov 10 2020 at 13:35):

@Emilio Jesús Gallego Arias but the "compiler" approach at least seems more robust than the meta-package one to me, for options like native. You don't risk ending up in some undefined state with your packages (if you trigger recompilation in a switch going from native->nonnative or the opposite and something fails)

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 14:04):

since new arguments on coq-native are being presented here (instead of the CEP thread): the options for 8.13 seem to be either coq-native or broken native.

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 14:06):

and I’m not sure how well modifying switches can/should be supported.

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 14:07):

@Emilio Jesús Gallego Arias re “bad idea”, do you refer to coq-as-compiler, or also to coq-native? If the alternative is split packages, that can’t happen before 8.14

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 14:08):

(according to @Pierre-Marie Pédrot on the CEP thread)

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 14:09):

After the merge of https://github.com/coq/coq/pull/13297 we can have native split packages in 8.13 though, in an opt-in way

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 14:10):

it would require a bit of tinkering with opam files since there is no support from the build system but if you really want it nobody prevents it from doing so

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 14:11):

(the fact that we need to take a decision for the support of native is the reason I don't want to force stuff in 8.13)

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 14:12):

but the way we compile native files is orthogonal to that choice, so we can have an external tool that does it for us

view this post on Zulip Karl Palmskog (Nov 10 2020 at 14:16):

I can summarize the "new" arguments in the CEP thread, but would like to hear Emilio's comments on meta-vs.-compiler

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 14:20):

Yeah the compiler support could actually be interesting, but still pretty expensive IMHO, compiling with native = yes is _very_ expensive in terms of RAM etc,... so I still prefer a more granular approach, isn't it annoying that I'd need 20GiB of RAM just to use bignums with native

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 14:20):

?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 14:20):

I think native is not broken for 8.13 tho, however it has to be manually enabled for packages with is a bit annoying.

view this post on Zulip Karl Palmskog (Nov 10 2020 at 14:21):

hmm, but I think both meta-package and compiler would rule out granularity (although I agree granularity would be nice)

view this post on Zulip Karl Palmskog (Nov 10 2020 at 14:26):

in terms of the CEP, it looks like what the compiler approach also gives you is that you don't need to add "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed} in every package definition under the sun, since this would be redundant in a native switch?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 14:30):

Indeed; one open question with the compiler approach is what happens when developing and incremental builds. AFAICT, when developing a Coq lib you may want not to compile to native each time; as this is very expensive. Dune experimental support does this for example. Having the switch setup, you would pay the price always I assume?

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:03):

"Very expensive" seems like an overstatement. We ran the whole bench on pyrolyse and it only took 10% longer to compile the native libraries, if I understand the numbers correctly.

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:04):

More like +65% actually

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:05):

with a few remarkable explosions both in time and memory

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:06):

e.g. notably unimath, around +150% in time

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:08):

and about 10 times as much as memory :space_invader:

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:08):

(changing foundations require upgrading your hardware it seems)

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:11):

Unimath is more of an exception. Does it even contain a single Qed? Every proof gets compiled to native code, which is certainly not representative of libraries out there.

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:12):

I agree that it's an outlier, but if we want to activate native compilation by default they will complain

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:13):

Lambda-Rust, Flocq, Bignums, Mathcomp-field, Four-Color, and so on, are under 10% (Color is at 20%).

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:14):

"The reasonable people that terminate their proofs with Qed"

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:14):

Sure, but I do not think anyone would disagree if Unimath were to include -native-compiler no in its options.

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:17):

out of curiosity:

pm@ouranos:~/sources/UniMath$ git grep "\bQed\b" | wc -l
4169

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:17):

and

pm@ouranos:~/sources/UniMath$ git grep "\bDefined\b" | wc -l
7527

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:20):

Oh! Funnily enough, the file I am looking at ends Lemmas with Defined, and Definitions with Qed. That is indeed quite a change of foundations :-)

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:22):

More seriously, I guess this really depends on the parts of Unimath.

view this post on Zulip Guillaume Melquiond (Nov 10 2020 at 15:23):

What annoys me a bit more is that CompCert is taking a 30% hit and I do not have a good explanation to it. I guess the functions to compile are just too large.

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:28):

There is that crazy pattern matching that already takes ages in coqc, native compilation cannot be any better

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 15:28):

In Integer.v or something.

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 16:42):

@Emilio Jesús Gallego Arias

I think native is not broken for 8.13 tho, however it has to be manually enabled for packages with is a bit annoying.

I disagree. On Mac, native is just disabled for everybody (even those not affected by the critical bugs?). On Linux, you get ondemand by default, which is the worst of both worlds in most cases.

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 16:46):

native=no just requires your own Coq opam package (I guess I should just advertise mine, since I'm maintaining it anyway).

view this post on Zulip Paolo Giarrusso (Nov 10 2020 at 16:48):

and IIUC native=yes can be enabled with enough effort but I'm not sure how many people know how to do that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 23:00):

"Very expensive" seems like an overstatement. We ran the whole bench on pyrolyse and it only took 10% longer to compile the native libraries, if I understand the numbers correctly.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 23:02):

I disagree. On Mac, native is just disabled for everybody (even those not affected by the critical bugs?). On Linux, you get ondemand by default, which is the worst of both worlds in most cases.

Oh, I see what you mean. Actually the Mac situation is unfortunate, I would have personally implemented a different fix and keep the support for native enabled.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 23:03):

There is really little justification for the current decision.

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 18:51):

Regardless of the Mac bugs, I think the usecases for ondemand are limited, and the arguments for ondemand as default are essentially non-existent.

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 18:52):

IIRC, the only potential usecase is when vm_compute is slower than native_compute including the compilation time of all the involved libraries.

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 18:56):

I'm willing to accept that argument, even tho it hasn't been demonstrated; it doesn't seem a great argument for enabling it by default.


Last updated: Oct 21 2021 at 20:02 UTC