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 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!

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: Jun 25 2024 at 19:01 UTC