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
Task Type Bug Report
Category Packages: Extra
Status Closed
Assigned To Jürgen Hötzel (juergen)
Konstantin Gizdov (kgizdov)
Architecture All
Severity Medium
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 0
Private No

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
Comment by Toolybird (Toolybird) - Tuesday, 25 July 2023, 21:15 GMT
Because it wasn't easy to find [1]

[1] https://github.com/mit-plv/fiat-crypto
Comment by Yawning Angel (yawning) - Wednesday, 26 July 2023, 05:21 GMT
Whoops sorry about that. Instead of the full build, `make standalone-ocaml` will be faster, and is sufficient to reproduce the failure.
Comment by loqs (loqs) - Wednesday, 26 July 2023, 15:19 GMT
coq 8.16.1 does not support ocaml 5.0 while coq 8.17 does it is recommended against due to performance issues [1] so creating an ocaml4 package may be required.

[1] https://github.com/coq/coq/issues/17263
Comment by Yawning Angel (yawning) - Wednesday, 26 July 2023, 15:45 GMT
Ah, that's unfortunate. There is ocaml4 in AUR[1].

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

Loading...