diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 5 |
2 files changed, 10 insertions, 1 deletions
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 7b5811dc4a..589a826e02 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -9,4 +9,8 @@ GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} -( cd GeoCoq && ./configure.sh && make -j ${NJOBS} ) +( cd GeoCoq && \ + ./configure.sh && \ + sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + coq_makefile -f Make -o Makefile && \ + make -j ${NJOBS} ) 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 |