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?
I think there are issues with native compilation. So far, the only native-compilation-issue-free OCaml seems to be 4.07.1.
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.)
Compilation time explosion in some corner cases
But indeed jsCoq deactivates native compilation so you should be fine
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.)
@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.
Regarding the efficiency of the OCaml compiler itself, there are cases where it is better, others it is worse, so YMMV.
Hi @Emilio Jesús Gallego Arias ! Long time no see.
I spent the evening writing Dune files for the coq-elpi plugin. You should be proud.
Hi @Shachar Itzhaky ! Oh, do you know that there is already a stub for the files at coq-elpi's github PR tracker?
oh is there :face_palm:
It used to have dune files before, but they were removed. Note that there are some issues with linking, but they can be workarounded.
Yes I used the common workaround of a rule that links using
you need to use -linkall, but that will fail in OCaml >= 4.08 as it forbids double-linking
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.
Here's the thing, this is currently working in OCaml 4.10.2, fingers crossed:
Last updated: Oct 05 2023 at 02:01 UTC