search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
717 stars 147 forks source link

Installation problems on Arch Linux: Package `coq-core.plugins.ltac' not found #1787

Closed defeo closed 11 months ago

defeo commented 11 months ago

I get the same error as #1558 when compiling on Arch:

CAMLC -c src/Rewriter/Util/plugins/ltac2_extra.mli
ocamlfind: Package `coq-core.plugins.ltac' not found

coq and ocaml-findlib installed through pacman.

Any ideas?

JasonGross commented 11 months ago

Looks like Arch recently upgraded their Coq package from 8.16 to 8.18, so I suspect the issue is that the META file is going misplaced in the Arch package. https://github.com/coq/coq/issues/15635 might have more hints, and Coq Zulip is probably a good place to ask for help on how the Arch package should be fixed. (In the meantime, you can use the same workaround as in #1558 and install Coq via opam)

JasonGross commented 11 months ago

Plausibly related: https://github.com/coq/coq/issues/15663

JasonGross commented 11 months ago

I guess the issue in Arch is a missing configure at https://gitlab.archlinux.org/archlinux/packaging/packages/coq/-/blob/main/PKGBUILD?ref_type=heads#L49 as in https://github.com/coq/coq/issues/15663#issuecomment-1654496159

Originally posted by @JasonGross in https://github.com/coq/coq/issues/15635#issuecomment-1866724665

I will email the Arch maintainer about this

JasonGross commented 11 months ago

You can work around the issue with

ln -s /usr/lib/coq /usr/lib/ocaml/coq
ln -s /usr/lib/coq-core /usr/lib/ocaml/coq-core
ln -s /usr/lib/coqide-server /usr/lib/ocaml/coqide-server
defeo commented 11 months ago

Wow! Thanks for the help, I couldn't hope for better assistance!

The symlinks indeed worked. I guess I can close this.