Stream: Coq users

Topic: Coq with OCaml 4.10


view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 16:07):

Hi, I can only get OCaml 4.10.2 right now, since older versions don't support macOS + arm64. I built Coq and it seems so far so good; are there any gotchas?

view this post on Zulip Karl Palmskog (Jan 11 2021 at 16:28):

I think there are issues with native compilation. So far, the only native-compilation-issue-free OCaml seems to be 4.07.1.

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 17:21):

What are the issues with native compilation? (I suspect that at least for jsCoq that should not matter since it only uses the bytecode version.)

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 17:21):

Compilation time explosion in some corner cases

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 17:22):

But indeed jsCoq deactivates native compilation so you should be fine

view this post on Zulip Guillaume Melquiond (Jan 11 2021 at 17:48):

Just in case there is a misunderstanding, by native compilation, we do not mean the architecture-specific executable (as opposed to the bytecode one), we mean the support for the native_compute tactic. (That said, this is also disabled for jsCoq.)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2021 at 19:27):

@Shachar Itzhaky no issues at all, except for a bug in the GC which will be fixed in 4.11.2 / 4.10.3 , this bug has some perf impact.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2021 at 19:27):

Regarding the efficiency of the OCaml compiler itself, there are cases where it is better, others it is worse, so YMMV.

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 19:27):

Hi @Emilio Jesús Gallego Arias ! Long time no see.

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 19:29):

I spent the evening writing Dune files for the coq-elpi plugin. You should be proud.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2021 at 19:30):

Hi @Shachar Itzhaky ! Oh, do you know that there is already a stub for the files at coq-elpi's github PR tracker?

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 19:30):

oh is there :face_palm:

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2021 at 19:30):

It used to have dune files before, but they were removed. Note that there are some issues with linking, but they can be workarounded.

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 19:31):

Yes I used the common workaround of a rule that links using ocamlfind -linkpkg.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 11 2021 at 19:31):

you need to use -linkall, but that will fail in OCaml >= 4.08 as it forbids double-linking

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 19:32):

Yup; I have to -dontlink the packages that are linked within Coq. Ofc that would not solve problems when two plugins link against the same lib.

view this post on Zulip Shachar Itzhaky (Jan 11 2021 at 19:59):

Here's the thing, this is currently working in OCaml 4.10.2, fingers crossed:
https://github.com/jscoq/addon-elpi/tree/elpi-1.11-8.12/dune-files


Last updated: Feb 09 2023 at 00:03 UTC