Emilio Jesús Gallego Arias (Jun 24 2020 at 11:44): 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?
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
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.
Paolo Giarrusso (Jun 24 2020 at 12:32):Also because .vo files are already used for ondemand right?
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
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?
Emilio Jesús Gallego Arias (Jun 24 2020 at 12:34):where for packages coq-mathcomp we have also have coq-mathcomp-native
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
Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):@Paolo G. Giarrusso what I'm thinking is more to have different packages
Paolo Giarrusso (Jun 24 2020 at 12:35):Ah I see, that sounds easier to implement than what I was thinking
Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):so for example coq-interval would depend on coq-mathcomp-native
Paolo Giarrusso (Jun 24 2020 at 12:35)::+1:
Emilio Jesús Gallego Arias (Jun 24 2020 at 12:35):if it really needs the native stuff
Paolo Giarrusso (Jun 24 2020 at 12:35):also works if packages are installed system-wide, which I was consciously ignoring
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
Emilio Jesús Gallego Arias (Jun 24 2020 at 12:36):that may work
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
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
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
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
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
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
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
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.
Emilio Jesús Gallego Arias (Jun 24 2020 at 13:25):Ups, indeed that's a problem.
Emilio Jesús Gallego Arias (Jun 24 2020 at 13:25):Um.....
Paolo Giarrusso (Jun 24 2020 at 13:38):Is it a problem tho? Say mathcomp doesn't use native-compute, does it?
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.
Emilio Jesús Gallego Arias (Jun 24 2020 at 13:40):Indeed, that would seem a bit complex tho in terms of defaults
Paolo Giarrusso (Jun 24 2020 at 13:40):That seems enough, based on the user stories by silene @Vincent Siles...
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
Emilio Jesús Gallego Arias (Jun 24 2020 at 13:41):and others don't
Emilio Jesús Gallego Arias (Jun 24 2020 at 13:41):but include the native files
Paolo Giarrusso (Jun 24 2020 at 13:41):maybe use coq-interval-native as package name, and keep the other as an alias?
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
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)
Paolo Giarrusso (Jun 24 2020 at 13:43):re defaults, non-split packages need not be selected by default
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.
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.
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?
Paolo Giarrusso (Jun 24 2020 at 13:47):Cool, happy this helps :-)
Last updated: Dec 06 2023 at 15:01 UTC