Stream: Coq users

Topic: OCaml implementation of Coq's PrimInt63


view this post on Zulip Yannick Forster (Jul 07 2023 at 11:35):

The refman on primitive integers states

The extraction of these primitives can be customized similarly to the extraction of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlInt63 module can be used when extracting to OCaml: it maps the Coq primitives to types and functions of a Uint63 module (including signed functions for Sint63 despite the name). That 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.

Where can I find such a module in the kernel of Coq? I found uint63, but the names don't match. For instance PrimInt63 specifies lsl, whereas the ml module only provides lsl

view this post on Zulip Gaëtan Gilbert (Jul 07 2023 at 11:36):

you mean the ml provides l_sl right?

view this post on Zulip Gaëtan Gilbert (Jul 07 2023 at 11:38):

but that matches https://github.com/coq/coq/blob/c7b14d0c800697f94845b14943ab281c5478adbb/theories/extraction/ExtrOCamlInt63.v#L26 so I don't understand the problem

view this post on Zulip Karl Palmskog (Jul 07 2023 at 11:40):

we had some discussion about packaging these things separately and updating the manual on this topic: https://github.com/coq/coq/issues/15936

Maybe this is still an option to clear up this confusion?

view this post on Zulip Ana de Almeida Borges (Jul 07 2023 at 13:56):

That one works (or at least it used to work), here is the commit message from when we started using it at FV:

Add OCaml module for Uint63

This module was taken from Coq at
coq/kernel/uint63.mli
coq/_build/default/kernel/uint63.ml (after compilation)

with the small tweak of avoiding OCaml Warning 50.
(Basically some OCaml comments have special meaning and need newlines
between them. See https://ocaml.org/manual/doccomments.html)

view this post on Zulip Yannick Forster (Oct 26 2023 at 17:01):

I would like to link an OCaml program with Coq's uint63.ml. I am trying something like ocamlfind opt -package coq-core.kernel cMap.cmx int.cmx uint63.cmx myfile.ml -o exec. I'm getting

/usr/bin/ld: cannot find /home/yannick/.opam/switch/lib/coq-core/kernel/uint63.o: No such file or directory
/usr/bin/ld: cannot find /home/yannick/.opam/switch/lib/coq-core/clib/int.o: No such file or directory
/usr/bin/ld: cannot find /home/yannick/.opam/switch/lib/coq-core/clib/cMap.o: No such file or directory

view this post on Zulip Yannick Forster (Oct 27 2023 at 11:15):

I figured it out: ocamlfind opt -package coq-core.kernel coqrun.cmxa clib.cmxa kernel.cmxa myfile.ml -o run

view this post on Zulip Ana de Almeida Borges (Oct 31 2023 at 16:09):

Huh, so you don't need to specifically mention uint63.ml?

view this post on Zulip Yannick Forster (Oct 31 2023 at 16:39):

Yep, uint63.cmx is part of kernel.cmxa

view this post on Zulip Yannick Forster (Oct 31 2023 at 16:40):

I would have liked a slimmer way to link to just uint63.cmx, but since there is no uint63.o installed by Coq this doesn't work - so I have to brute force link in all relevant cmxa files

view this post on Zulip Karl Palmskog (Oct 31 2023 at 16:56):

I think the best way would be if we wrote a proper separate opam package for uint63.ml using Dune

view this post on Zulip Yannick Forster (Oct 31 2023 at 16:57):

I absolutely agree :) But since the opam package seems to be planned for a while already, but I needed a solution now this was my workaround

view this post on Zulip Karl Palmskog (Oct 31 2023 at 16:57):

for example, call it coq-uint63

view this post on Zulip Karl Palmskog (Oct 31 2023 at 16:58):

one hacky solution would be if we just made a repo in Coq-community with the uint63.ml file and a dune build and opam file for it

view this post on Zulip Karl Palmskog (Oct 31 2023 at 16:59):

at least it might be a good way to test the workflow before integrating into Coq proper

view this post on Zulip Yannick Forster (Oct 31 2023 at 17:02):

I like the idea :) We need cMap.ml, int.ml, and uint63.ml I think

view this post on Zulip Karl Palmskog (Oct 31 2023 at 17:05):

are they self-contained?

view this post on Zulip Karl Palmskog (Oct 31 2023 at 17:05):

I think I will play around with it in a repo of my own for 8.18, and if it works I will move it to Coq-community

view this post on Zulip Yannick Forster (Oct 31 2023 at 17:06):

I think they are self-contained, yes

view this post on Zulip Yannick Forster (Oct 31 2023 at 17:06):

I only care about uint63.ml, but I had to identify a suitable self-contained subset

view this post on Zulip Karl Palmskog (Oct 31 2023 at 17:07):

since this will not be rolled out for Coq 8.18 anyway (hard to motivate inclusion in 8.18.1), it makes sense to have a separate semi-official repo. Then we just archive the repo when Coq includes the package.

view this post on Zulip Karl Palmskog (Oct 31 2023 at 18:46):

@Yannick Forster what do you think? I tried to copy and minimize all the Dune boilerplate from v8.18: https://github.com/palmskog/coq-uint63

The main difference from Coq itself is that this library is "wrapped" as coq-uint63.uint63.

view this post on Zulip Karl Palmskog (Oct 31 2023 at 18:48):

we could maybe least use this to experiment with extraction projects, then if that workflow is validated I'm sure lots of stuff could be improved and added into Coq eventually (my Dune knowledge is not great, I probably missed some options)


Last updated: Jun 23 2024 at 05:02 UTC