You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
After cloning the project to my local environment, I have encountered some issues during the process of compiling and installing dependencies:
The make command provided in the README, which corresponds to the makefile file, is placed in the BigInt directory. However, the BigInt directory is parallel to Coqprime, resulting in an error when executing make install-coqprime due to the corresponding directory not being found.
About Requirements , the recommended version of Coq is 8.15.2, but the recommended version for coq-rewriter is 8.17 or later.
It appears that there is a lack of a master _CoqProject file to compile coqprime, BigInt/src, fiat-crypto, and Rewriter together. Additionally, after cloning Rewriter to my local environment, where should the related Rewriter directories be arranged?
I would greatly appreciate any guidance or advice you could offer on these matters.
The text was updated successfully, but these errors were encountered:
After cloning the project to my local environment, I have encountered some issues during the process of compiling and installing dependencies:
The
make
command provided in the README, which corresponds to themakefile
file, is placed in the BigInt directory. However, the BigInt directory is parallel to Coqprime, resulting in an error when executingmake install-coqprime
due to the corresponding directory not being found.About
Requirements
, the recommended version of Coq is 8.15.2, but the recommended version for coq-rewriter is 8.17 or later.It appears that there is a lack of a master
_CoqProject
file to compile coqprime, BigInt/src, fiat-crypto, and Rewriter together. Additionally, after cloning Rewriter to my local environment, where should the related Rewriter directories be arranged?I would greatly appreciate any guidance or advice you could offer on these matters.
The text was updated successfully, but these errors were encountered: