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.

I can rely the answer, but I don't know it ;-)

Being a user of primitive types extraction myself, I would love it if it was possible indeed.

So the answer is: please open a feature request?

There was a recent discussion on adding these to metacoq and use verified extraction.

Maybe @Jakob Botsch Nielsen remembers the link.

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

Coq already installas many libraries, eg `coq.kernel`

is one, but it includes much more than just these 3 files.

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

I don't know if something similar could/should be done w.r.t. the Nix packaging though.

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: Oct 13 2024 at 01:02 UTC