ocaml-5.0.0 incompatibility
Task Info (Flyspray) | |
---|---|
Opened By | Yawning Angel (yawning) |
Task ID | 79197 |
Type | Bug Report |
Project | Arch Linux |
Category | Packages: Extra |
Version | None |
OS | All |
Opened | 2023-07-25 08:07:02 UTC |
Status | Assigned |
Assignee | Jürgen Hötzel (juergen) |
Assignee | Konstantin Gizdov (kgizdov) |
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.