search

mit-plv / fiat-crypto

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

mac m1 build fail #1616

Closed zweite closed 1 year ago

zweite commented 1 year ago

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

JasonGross commented 1 year ago

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.

zweite commented 1 year ago

coqc --version

The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.14.0
brew install coq ocaml-findlib coreutils jq
JasonGross commented 1 year ago

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

zweite commented 1 year ago

Thanks for your help, I have solved my problem with ubuntu operating system.