这里的EasyCrypt指的是那个密码学的辅助证明工具.
其实他的github上说明已经挺详细的了,但还是会有一点坑,记录一下.
PS:据说里面有个script
目录里有安装脚本的(不过我没试过,逃)
首先安装包管理工具opam
:
# e.g. ubuntu 18.04
sudo add-apt-repository ppa:avsm/ppa
sudo apt-get update
sudo apt-get install ocaml ocaml-native-compilers camlp4-extra opam
opam init
eval `opam config env`
克隆github上的仓库:
git clone https://github.com/EasyCrypt/easycrypt.git
cd easycrypt
指定编译器(ocaml
?)版本,就是仓库的README
的“Via OPAM”对应的第0点,但上面指定的版本是个变量$OVERSION
,这里应该换成跟他一样的4.07.0
,不然会有奇怪的错误(不过其实4.07.0
以上的好像也行,像我如果还要编EasyUC
的话就需要4.08.0
);然后后面第1点没啥问题,就一起写了:
opam switch create easycrypt 4.08.0
opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
第2点的话据说在opam=2.1.0
及以上的版本已经不需要depext
了,所以可以忽略;第三点的话需要注意alt-ergo
的版本要跟他的2.4.0
一样(在“Note on Prover Versions”里有说- -):
opam install --deps-only easycrypt
opam pin alt-ergo 2.4.0
然后第4点的z3=4.8.10
和cvc4=1.8
其实是要自己安装的,对应的github上都有release,注意版本就好,然后加到path
中(这里我直接放bin
里了):
# z3
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip
# unzip and cd ...
ln -s /path/to/z3-4.8.10-x64-ubuntu-18.04/bin/z3 /path/to/bin
# cvc4
wget https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
chmod +x ./cvc4-1.8-x86_64-linux-opt
ln -s /path/to/cvc4-1.8-x86_64-linux-opt /path/to/bin
然后why3 config
一下,没报错的话就没啥问题了:
why3 config detect
接着就可以愉快地make
了,在make
的时候会报两个错,都是跟Option
相关的,根据这里的说法,Option
改名为BatOption
了,打开报错的文件把“Option”改成“BatOption”就好(比如我编的版本是src/ecHiGoal.ml: 695
和src/ecTheoryReplay.ml: 839
),都改完后再make
就没啥问题了;
然后make install
是可以指定目录的,比如我装在~/.local
里(已经加到path
里的)就不用sudo
了:
# change Option to BatOption
make
make check
make examples
make PREFIX=~/.local install
easycrypt --help
如果能运行的话就是安装成功了;
另外说一下easycrypt
后面接文件运行时有时会没有输出的(特别是如果证明是对的话),所以需要获取它的返回值,用echo $?
,或者:
if easycrypt path/to/xxx.ec; then echo yes; else echo no; fi
Links:
原文链接:https://tover.xyz/p/easy-crypt-install/
(赶了几天作业(ddl),拖了几天才转了,逃