Installation problems on macOS: Package `coq-core.plugins.ltac' not found
tarcieri opened this issue · 2 comments
tarcieri commented
I've encountered the following attempting to install on macOS (Ventura 13.2, both ARM and Intel):
CAMLC -c src/Rewriter/Util/plugins/ltac2_extra.mli
ocamlfind: Package `coq-core.plugins.ltac' not found
coq and ocaml-findlib were installed via Homebrew.
It seems similar to this?
(Also separately, have you considered having a Dockerfile that provides a reproducible build on e.g. Ubuntu?)
andres-erbsen commented
The Coq issue you linked seems indeed related -- perhaps the Homebrew package for Coq does not have the META file in the right location. If you're willing to use OPAM, we have CI-tested installation steps here. Alternatively, the Coq Platform also includes Fiat Cryptography.
tarcieri commented
I resolved the issue by installing with opam, which worked great