Shachar Itzhaky (Jan 11 2021 at 16:07): 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?
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.
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.)
Pierre-Marie Pédrot (Jan 11 2021 at 17:21):Compilation time explosion in some corner cases
Pierre-Marie Pédrot (Jan 11 2021 at 17:22):But indeed jsCoq deactivates native compilation so you should be fine
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.)
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.
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.
Shachar Itzhaky (Jan 11 2021 at 19:27):Hi @Emilio Jesús Gallego Arias ! Long time no see.
Shachar Itzhaky (Jan 11 2021 at 19:29):I spent the evening writing Dune files for the coq-elpi plugin. You should be proud.
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?
Shachar Itzhaky (Jan 11 2021 at 19:30):oh is there :face_palm:
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.
Shachar Itzhaky (Jan 11 2021 at 19:31):Yes I used the common workaround of a rule that links using ocamlfind -linkpkg.
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
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.
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: Oct 05 2023 at 02:01 UTC