Replace Pervasives with Stdlib in nat extraction

[rudynicolop]

• Added changelog.

• Opened overlay pull requests.

[proux01]

What are the OCaml versions supported by extraction? Coq itself should build on OCaml 4.05 to 4.13, is it possible to support that range of versions here?

[herbelin]

@rudynicolop: do your #???? in the header intend to refer to #7017 and #13288? As hinted by @proux01, Stdlib requires OCaml 4.08 (I did not follow closely the discussions, but the OCaml requirements for Coq 8.16 are probably not decided though).

[rudynicolop]

@rudynicolop: do your #???? in the header intend to refer to #7017 and #13288? As hinted by @proux01, Stdlib requires OCaml 4.08 (I did not follow closely the discussions, but the OCaml requirements for Coq 8.16 are probably not decided though).

Sorry my bad I don't think I need the issue number.

[rudynicolop]

To allow support for any OCaml version I could inline the functions in the extraction without referring to those in the standard library. I mainly would like to avoid Pervasives because extraction with it produces many warning messages in later OCaml versions.

[herbelin]

To allow support for any OCaml version I could inline the functions in the extraction without referring to those in the standard library. I mainly would like to avoid Pervasives because extraction with it produces many warning messages in later OCaml versions.

Is there a way from inside OCaml to have code dependent on the version of OCaml running? If yes, extraction could add a header redefining Pervasives from Stdlib (or vice-versa).

An alternative would be to inline the code, e.g. fun x -> x + 1 in place of succ, etc. To mitigate this, we could imagine extending Extract Constant so that it takes arguments, as in Extract Constant succ n => "n + 1".

About what you propose, see the discussion at #10936: we would typically need to let succ, max, min be local keywords so that they don't need a qualifier and Coq extracts its own succ, max, min to say succ0, max0, min0.

[Alizter]

Now that we have bumped OCaml, we can probably go ahead with this.

@rudynicolop Can you rebase on a recent master?

cc @ppedrot

[ppedrot]

I've taken the liberty to rebase myself for faster integration.

[ppedrot]

I've tweaked a bit the commit message because it was the result of squashing temporary commits, but this is ready. Will merge when CI finishes.

[ppedrot]

@coqbot merge now

[liyishuai]

Stdlib.Int.max was first introduced in ocaml/ocaml#10392.
As a result, the extracted code only compiles on OCaml 4.13.

[Alizter]

@liyishuai That's a shame, I saw "since 4.08" at the top of Int and didn't assume that max and min would not be included. Am I correct in thinking that removing .Int will be enough?

[liyishuai]

Yes removing .Int should fix the issue.
Maybe also worth adding https://github.com/liyishuai/coq-http (that revealed this issue) to the CI test suite.