Stream: Coq devs & plugin devs

Topic: Question from Cuq Club about primitive types and extraction


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Dec 16 2020 at 16:59):

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Dec 16 2020 at 17:09):

So the answer is: please open a feature request?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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: Oct 16 2021 at 09:07 UTC