diff options
| author | Emilio Jesus Gallego Arias | 2017-02-07 15:38:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-07 15:38:54 +0100 |
| commit | c176063e57d1555fa7acd273dd151e35a01e58d1 (patch) | |
| tree | 4a1bd65bfcdfb68b5819c377a5e8d67939bbc6b1 /dev/ci | |
| parent | 0a1c83768a6b0199afa1ad4fb633c9ede4a84d20 (diff) | |
[travis] [External CI] iris-coq: fix dependencies
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index c1306e070d..e97e2c19e3 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -24,6 +24,11 @@ git clone --depth 1 https://github.com/math-comp/math-comp.git # echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc # echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +# Setup stdpp +git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git + +( cd coq-stdpp && make -j ${NJOBS} && make install ) + # Setup Iris git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git |