Stream: Coq users

Topic: ✔ Coq extraction: Pervasives is deprecated

shenghao (Sep 06 2022 at 21:24):

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,

shenghao (Sep 06 2022 at 21:32):

btw, Pervasives. is everywhere in the extracted ocaml code

Karl Palmskog (Sep 06 2022 at 21:43):

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

shenghao (Sep 06 2022 at 21:53):

thx, currently, I prefer to replace all Pervasives with Stdlib. :rolling_on_the_floor_laughing:

shenghao (Sep 06 2022 at 21:59):

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".

Li-yao (Sep 06 2022 at 22:09):

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

shenghao (Sep 06 2022 at 22:18):

Li-yao said:

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

Extractly, I removed ExtrOCamlInt63 just now, it is fine now~ thanks a lot!

Notification Bot (Sep 06 2022 at 22:19):

shenghao has marked this topic as resolved.

Karl Palmskog (Sep 07 2022 at 19:39):

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 05 2023 at 02:01 UTC