@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
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 are already used for
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
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
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.
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
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
and others don't
but include the native files
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: Dec 06 2023 at 15:01 UTC