Stream: Coq devs & plugin devs

Topic: Quick question about native


view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 11:44):

@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?

view this post on Zulip Pierre-Marie Pédrot (Jun 24 2020 at 11:48):

theoretically you could do it from the vo I believe, but currently the compilation needs to be perfomed from the source file

view this post on Zulip Maxime Dénès (Jun 24 2020 at 11:49):

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.

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:32):

Also because .vo files are already used for ondemand right?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:33):

Indeed, I see thanks; actually I was thinking of a bit of a different setup for dune

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:34):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:34):

where for packages coq-mathcomp we have also have coq-mathcomp-native

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:34):

so the cost of compiling the cmxs is only paid by those that need the native files

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):

@Paolo G. Giarrusso what I'm thinking is more to have different packages

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:35):

Ah I see, that sounds easier to implement than what I was thinking

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):

so for example coq-interval would depend on coq-mathcomp-native

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:35):

:+1:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):

if it really needs the native stuff

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:35):

also works if packages are installed system-wide, which I was consciously ignoring

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):

but indeed some changes to Coq may be required, but in principle if the cmxs can be generated without re-typechecking

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:36):

that may work

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:36):

the problem with enabling native by default is that we would increase compile time for a lot of users

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:37):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:37):

so indeed if native compilation can be performed in its own package then that'd be fine

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:37):

yeah is a bit unfortunate that OCaml takes a long time to compile the cmxs

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 12:37):

Pierre-Marie has submitted a few bug reports to improve complexity of compilation but that is not in the roadmap so far

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:40):

Yeah it'd be great to drop configure -native-compiler no from macos packages without triggering bugs

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 12:41):

that is, even if linking stays slow, I'd still build Coq with native-compiler, if I was confident it never got used automatically

view this post on Zulip Enrico Tassi (Jun 24 2020 at 13:22):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:25):

Ups, indeed that's a problem.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:25):

Um.....

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:38):

Is it a problem tho? Say mathcomp doesn't use native-compute, does it?

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:40):

I'd propose to support split packages _only_ for code that doesn't use native_compute itself.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:40):

Indeed, that would seem a bit complex tho in terms of defaults

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:40):

That seems enough, based on the user stories by silene @Vincent Siles...

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:41):

It would be a bit weird tho that some packages have a -native version

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:41):

and others don't

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:41):

but include the native files

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:41):

maybe use coq-interval-native as package name, and keep the other as an alias?

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:42):

BTW I'm not even sure if coq-interval would want to use native_compute itself, I'm only assuming

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:42):

(or maybe set the aliasing the other way — or whatever "aliasing" can be mapped to in opam)

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:43):

re defaults, non-split packages need not be selected by default

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:45):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 24 2020 at 13:46):

Indeed, good points @Paolo G. Giarrusso ; I'll need a couple of days to think and re-push my prototype PR.

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:46):

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?

view this post on Zulip Paolo Giarrusso (Jun 24 2020 at 13:47):

Cool, happy this helps :-)


Last updated: Oct 15 2021 at 21:02 UTC