Hello,
I am trying to use Coq ExtrOcamlZInt library (coqc 8.13.2),
From Coq Require Extraction.
From Coq Require Import ExtrOcamlZInt.
but my ocamlopt
complain that (4.11.1)
ocamlopt -o X X.ml
2119 | (Pervasives.succ (Pervasives.succ (Pervasives.succ (Pervasives.succ
^^^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Pervasives
Use Stdlib instead
should we update this Coq library?
Best wishes,
btw, Pervasives.
is everywhere in the extracted ocaml code
from what I remember, you can use the OCaml package stdlib-shims
if you want to get rid of the deprecation. See also https://github.com/coq/coq/issues/11359
thx, currently, I prefer to replace all Pervasives
with Stdlib.
:rolling_on_the_floor_laughing:
BTW, the ExtrOcamlZInt library specifies:
Extract Constant Pos.compare_cont =>
"fun c x y -> if x=y then c else if x<y then Lt else Gt".
But the extracted ocaml doesn't know what are Lt
and Gt
,
So, I have to modify the extraction mapping relation:
Extract Constant Pos.compare_cont =>
"fun c x y -> if x=y then c else if x<y then (-1) else 1".
This may be because you require ExtrOCamlInt63
which overrides the extraction of comparison
to int
, which won't be the case in a future version of Coq. https://github.com/coq/coq/commit/8531e96ad4f47bef39b5890786ed2f1d142b9eca
Li-yao said:
This may be because you require
ExtrOCamlInt63
which overrides the extraction ofcomparison
toint
, which won't be the case in a future version of Coq. https://github.com/coq/coq/commit/8531e96ad4f47bef39b5890786ed2f1d142b9eca
Extractly, I removed ExtrOCamlInt63 just now, it is fine now~ thanks a lot!
shenghao has marked this topic as resolved.
ah, this is worrying: https://github.com/ocaml/opam-repository/pull/22081
xenstore < 2.1.1 is not compatible with OCaml 5.0 (uses Pervasives)
I have a feeling OCaml 5.0 is going to be a lot of work for everyone in the Coq ecosystem...
Last updated: Oct 13 2024 at 01:02 UTC