Stream: Coq users

Topic: Coq/x64 + Ocaml 4.10.2/4.12.0

view this post on Zulip Paolo Giarrusso (Apr 05 2021 at 19:46):

https://ocaml.org/releases/4.10.2.html and https://ocaml.org/releases/4.12.0.html are the only OCaml compilers supporting M1, so I was interested in upgrading on x64 as well.

  1. I guess using 4.10.2 on x64 should already be safe; I worry a bit because it's not tested, but that's paranoia, right?
  2. 4.12.0 isn't explicitly supported, but I guess it's probably fine?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 19:49):

There is only one way to know :)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 19:49):

4.10.2 has been used on M1 with Coq quite a bit, so indeed there is at least proof that it works, and I heard pretty well

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 19:50):

4.12.0 should be fine ; only reason it is not supported officially yet is that it requires Dune 2.8 I think

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 19:51):

due to some non-backwards compatible changes in OCaml itself IIRC, unfortunately this won't work well

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 19:54):

Due to some complexities due to work on the build system, it will still take a bit of time to have Coq's CI using 4.12.0, but don't let that hold you back.

view this post on Zulip Paolo Giarrusso (Apr 05 2021 at 21:32):

Thanks a lot for the info!

Last updated: Apr 20 2024 at 07:01 UTC