FS#79197 - [coq] ocaml-5.0.0 incompatibility
Attached to Project:
Arch Linux
Opened by Yawning Angel (yawning) - Tuesday, 25 July 2023, 08:07 GMT
Last edited by Buggy McBugFace (bugbot) - Saturday, 25 November 2023, 20:19 GMT
Opened by Yawning Angel (yawning) - Tuesday, 25 July 2023, 08:07 GMT
Last edited by Buggy McBugFace (bugbot) - Saturday, 25 November 2023, 20:19 GMT
|
Details
Description:
The coq package is built with/against ocaml 4.14.0, while the packaged version of ocaml is 5.0.0. Additional info: * `coq 8.16.1-1`, `ocaml 5.0.0-1` Steps to reproduce: Install coq, try to build fiat-crypto. The build process will fail with: ``` CAMLOPT -c src/Rewriter/Util/plugins/ltac2_extra.ml File "src/Rewriter/Util/plugins/ltac2_extra.ml", line 1: Error: /usr/lib/ocaml/coq-core/plugins/ltac2/ltac2_plugin.cmi is not a compiled interface for this version of OCaml. It seems to be for an older version of OCaml. make[2]: *** [Makefile.coq:741: src/Rewriter/Util/plugins/ltac2_extra.cmx] Error 2 make[1]: *** [Makefile.coq:409: all] Error 2 make: *** No rule to make target 'rewriter', needed by '.Makefile.coq.d'. Stop. ``` Downgrading ocaml to `ocaml-4.14.0-1` (along with the various dependencies) makes the build succeed. |
This task depends upon
Closed by Buggy McBugFace (bugbot)
Saturday, 25 November 2023, 20:19 GMT
Reason for closing: Moved
Additional comments about closing: https://gitlab.archlinux.org/archlinux/p ackaging/packages/coq/issues/1
Saturday, 25 November 2023, 20:19 GMT
Reason for closing: Moved
Additional comments about closing: https://gitlab.archlinux.org/archlinux/p ackaging/packages/coq/issues/1
[1] https://github.com/mit-plv/fiat-crypto
[1] https://github.com/coq/coq/issues/17263
At least for my use case and tangentially related to this, fiat-crypto has additional dependencies on ocaml-findlib[2], and ocaml-zarith[3]. There is ocaml4-findlib[4] in AUR, but no ocaml4-zarith exists at present.
[1]: https://aur.archlinux.org/packages/ocaml4
[2]: https://archlinux.org/packages/extra/x86_64/ocaml-findlib/
[3]: https://archlinux.org/packages/extra/x86_64/ocaml-zarith/
[4]: https://aur.archlinux.org/packages/ocaml4-findlib