@Maxime Dénès I forgot about this, does producing the .coq-native
files require to typecheck the .v
file, or can that be done from a .vo
?
theoretically you could do it from the vo I believe, but currently the compilation needs to be perfomed from the source file
Yes, exactly. I haven't thought a lot about it, but the terms should be enough to produce the native files, so like PMP said, it should be doable from the .vo
files.
Also because .vo
files are already used for ondemand
right?
Indeed, I see thanks; actually I was thinking of a bit of a different setup for dune
Does this mean you could compile native code for a library A only when building a "native" version of a library B (say CoqInterval) that uses A?
where for packages coq-mathcomp
we have also have coq-mathcomp-native
so the cost of compiling the cmxs is only paid by those that need the native files
@Paolo G. Giarrusso what I'm thinking is more to have different packages
Ah I see, that sounds easier to implement than what I was thinking
so for example coq-interval would depend on coq-mathcomp-native
:+1:
if it really needs the native stuff
also works if packages are installed system-wide, which I was consciously ignoring
but indeed some changes to Coq may be required, but in principle if the cmxs can be generated without re-typechecking
that may work
the problem with enabling native by default is that we would increase compile time for a lot of users
not enabling it by default means that people won't depend on it, and in the case they update the deps to depend on it everyone has to pay the cost even if not using
so indeed if native compilation can be performed in its own package then that'd be fine
yeah is a bit unfortunate that OCaml takes a long time to compile the cmxs
Pierre-Marie has submitted a few bug reports to improve complexity of compilation but that is not in the roadmap so far
Yeah it'd be great to drop configure -native-compiler no
from macos packages without triggering bugs
that is, even if linking stays slow, I'd still build Coq with native-compiler
, if I was confident it never got used automatically
I guess we could have coqc generates the .ml files for native's cmx code, but not compile them right away. If you can handle the compilation of extracted code with dune, you should be able to also handle this.
What won't work is .v files that interleave definitions with calls to native compute, in that case you would be force to fall back to vm compute.
Ups, indeed that's a problem.
Um.....
Is it a problem tho? Say mathcomp
doesn't use native-compute, does it?
I'd propose to support split packages _only_ for code that doesn't use native_compute
itself.
Indeed, that would seem a bit complex tho in terms of defaults
That seems enough, based on the user stories by silene
@Vincent Siles...
It would be a bit weird tho that some packages have a -native
version
and others don't
but include the native files
maybe use coq-interval-native
as package name, and keep the other as an alias?
BTW I'm not even sure if coq-interval would want to use native_compute
itself, I'm only assuming
(or maybe set the aliasing the other way — or whatever "aliasing" can be mapped to in opam)
re defaults, non-split packages need not be selected by default
so the default would either (a) get vm_compute
till you choose otherwise or (b) get an error and be required to choose explicitly what to do (to reduce surprise). Not sure what's best, and what's easy to implement.
Indeed, good points @Paolo G. Giarrusso ; I'll need a couple of days to think and re-push my prototype PR.
or rather, you can't get (b) without extra code, but having dune default to a new coq -native-compiler fail
sounds easy enough for both dune and even coqc?
Cool, happy this helps :-)
Last updated: Jun 08 2023 at 04:01 UTC