Stream: Coq users

Topic: ✔ Coq extraction: Pervasives is deprecated

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Notification Bot (Sep 06 2022 at 22:19):

shenghao has marked this topic as resolved.

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC