I’m looking to work with native OCaml integers in Coq, with the objective of extracting the program and running it natively.
My problem is that I can’t seem to understand what “Require Import” command to use to import these integers. My understanding is that they are stored in stdlib (as suggested by Standard Library | The Coq Proof Assistant) but all of my attempts (Require Import Numbers, Require Import Int63, etc) have given me the following Error:
Cannot find a physical path bound to logical path.
Any hints would be very appreciated.
If you look at the page e.g. for Uint63:
you’ll see at the vey top “Library Coq.Numbers.Cyclic.Int63.Uint63”.
That given, in your code you could simply write:
The point is those are logical paths and Coq needs to be told how those map to physical paths on disk. The code above works if you start coqc/coqtop with default options, otherwise there are command line options or the use of
_CoqProject files to do that/your mapping (e.g. custom defined paths in _CoqProject files is common to share code among one’s projects).
See the docs for more details, e.g. here: https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=_coqproject#logical-paths-and-the-load-path and here: https://coq.inria.fr/refman/practical-tools/coq-commands.html#command-line-options
I see. Thanks a lot, that was very instructive!
From Coq Require Uint63. is sufficient provided that there is only one package matching Coq. … .Uint63
From is not required, but it avoids name clashes if you later load another package that defines its own Uint63.