mac m1 build fail
zweite opened this issue · 4 comments
env:
mac-m1
cmd:
make -j8 standalone
fail info:
....
Makefile.local-late:8: warning: overriding commands for target `src/Rewriter/Util/plugins/StrategyTactic.v'
Makefile.local-late:8: warning: ignoring old commands for target `src/Rewriter/Util/plugins/StrategyTactic.v'
Makefile.local-late:8: warning: overriding commands for target `src/Rewriter/Util/plugins/Ltac2Extra.v'
Makefile.local-late:8: warning: ignoring old commands for target `src/Rewriter/Util/plugins/Ltac2Extra.v'
CAMLC -c src/Rewriter/Util/plugins/ltac2_extra.mli
ocamlfind: Package `coq-core.plugins.ltac' not found
make[2]: *** [src/Rewriter/Util/plugins/ltac2_extra.cmi] Error 2
make[1]: *** [all] Error 2
make: *** No rule to make target `.Makefile.coq.d', needed by `src/StandaloneOCamlMain.vo'. Stop.
I hope to optimize the calculation of p192 through fiat-crypto, but I have encountered some problems when building fiat-crypto. I am looking for your help
This looks like it might be an issue with the version of Coq you're using? What version are you using, and how did you install it?
Also, I think the newest version of the Coq Platform might be able to install Fiat Crypto for you.
coqc --version
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.14.0
brew install coq ocaml-findlib coreutils jq
Hmm, this version of Coq would work. I think we use opam to install Coq on our Mac CI. Otherwise, it looks like it might be an issue with the packaging of Coq in brew?
I don't have a Mac, so I've asked about this on Zulip
Thanks for your help, I have solved my problem with ubuntu operating system.