Enrico Tassi (Dec 16 2020 at 16:59): Enrico Tassi (Dec 16 2020 at 16:59):The documentation of Primitive Integers, Primitive Floats, and Primitive Arrays makes the point that, when extracting to OCaml, that implementations of Uint63, Float64, and PArray are not provided, but that the user must supply them. But it also points out that the Coq kernel has implementations of all of these. That being the case, could the building and installation of Coq be modified so that the binary form of these libraries is made available for those that would like to compile and execute Coq programs that use these features and are extracted to OCaml? That would save the user the work of extracting these from the Coq sources and having to rebuild them for each Coq version.
Enrico Tassi (Dec 16 2020 at 16:59):I can rely the answer, but I don't know it ;-)
Thomas Letan (Dec 16 2020 at 17:07):Being a user of primitive types extraction myself, I would love it if it was possible indeed.
Enrico Tassi (Dec 16 2020 at 17:09):So the answer is: please open a feature request?
Bas Spitters (Dec 16 2020 at 17:13):There was a recent discussion on adding these to metacoq and use verified extraction.
Maybe @Jakob Botsch Nielsen remembers the link.
Enrico Tassi (Dec 16 2020 at 17:33):I guess what users want is to have these files be shipped as a library, let's call it coq.primitive. The kernel of Coq could be a user, as well as any extracted piece of code. CC @Maxime Dénès @Erik Martin-Dorel @Kazuhiko Sakaguchi
Enrico Tassi (Dec 16 2020 at 17:34):Coq already installas many libraries, eg coq.kernel is one, but it includes much more than just these 3 files.
Erik Martin-Dorel (Dec 16 2020 at 18:02):@Enrico Tassi thanks for the ping, indeed with @Pierre Roux we had already mentioned that issue in the refman BTW, see:
https://coq.inria.fr/refman/language/core/primitive.html?highlight=primitive
The extraction of these primitives can be customized similarly to the extraction of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlFloats module can be used when extracting to OCaml: it maps the Coq primitives to types and functions of a Float64 module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq.
So we didn't follow the path up to thinking about packaging these primitive prerequisites apart as a reusable package, but this definitely looks feasible!
Erik Martin-Dorel (Dec 16 2020 at 18:04):I don't know if something similar could/should be done w.r.t. the Nix packaging though.
Enrico Tassi (Dec 16 2020 at 18:15):Note that I say "library" but I really mean a "findlib package" part of ...lib/coq/META, so I don't think it makes any difference w.r.t. nix.
Would you mind giving an answer on coqclub when you have a minute? Or I can do it, but I've no plans on working on these aspects of Coq, so I'm not a good entrypoint for the user.
Last updated: Jun 09 2023 at 08:01 UTC