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
I would say lack of resources (time) rather than lack of interest.
And Coq-as-a-compiler is only possible since opam 2.0 IIUC.
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
You need to compile with optimizing options? Re-install all your packages ...
the proposal with coq-native
meta-package does that as well, no?
Also native doesn't have some of the problems OCaml has, plus the compiler setup is quite experimental in OPAM itself
yes, that's why I think it's a bad idea
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...
I'm afraid there is nothing better in this sense, at least in OPAM 2.0, I dunno about upcoming 2.1 / 2.2 .
@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)
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.
and I’m not sure how well modifying switches can/should be supported.
@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
(according to @Pierre-Marie Pédrot on the CEP thread)
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
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
(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)
but the way we compile native files is orthogonal to that choice, so we can have an external tool that does it for us
I can summarize the "new" arguments in the CEP thread, but would like to hear Emilio's comments on meta-vs.-compiler
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
?
I think native is not broken for 8.13 tho, however it has to be manually enabled for packages with is a bit annoying.
hmm, but I think both meta-package and compiler would rule out granularity (although I agree granularity would be nice)
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?
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?
"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.
More like +65% actually
with a few remarkable explosions both in time and memory
e.g. notably unimath, around +150% in time
and about 10 times as much as memory :space_invader:
(changing foundations require upgrading your hardware it seems)
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.
I agree that it's an outlier, but if we want to activate native compilation by default they will complain
Lambda-Rust, Flocq, Bignums, Mathcomp-field, Four-Color, and so on, are under 10% (Color is at 20%).
"The reasonable people that terminate their proofs with Qed"
Sure, but I do not think anyone would disagree if Unimath were to include -native-compiler no
in its options.
out of curiosity:
pm@ouranos:~/sources/UniMath$ git grep "\bQed\b" | wc -l
4169
and
pm@ouranos:~/sources/UniMath$ git grep "\bDefined\b" | wc -l
7527
Oh! Funnily enough, the file I am looking at ends Lemma
s with Defined
, and Definition
s with Qed
. That is indeed quite a change of foundations :-)
More seriously, I guess this really depends on the parts of Unimath.
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.
There is that crazy pattern matching that already takes ages in coqc, native compilation cannot be any better
In Integer.v or something.
@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.
native=no
just requires your own Coq opam package (I guess I should just advertise mine, since I'm maintaining it anyway).
and IIUC native=yes
can be enabled with enough effort but I'm not sure how many people know how to do that
"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.
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.
There is really little justification for the current decision.
Regardless of the Mac bugs, I think the usecases for ondemand
are limited, and the arguments for ondemand
as default are essentially non-existent.
IIRC, the only potential usecase is when vm_compute
is slower than native_compute
including the compilation time of all the involved libraries.
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 13 2024 at 01:02 UTC