[ci] GeoCoq now depends on math-comp's ssralg.

2 files changed, 21 insertions, 10 deletions

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 5b5cbd11ae..85df249d38 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -93,17 +93,26 @@ install_ssreflect()
   git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
 
   ( cd "${mathcomp_CI_DIR}/mathcomp" && \
-    sed -i.bak '/ssrtest/d'     Make && \
-    sed -i.bak '/odd_order/d'   Make && \
-    sed -i.bak '/all\/all.v/d'  Make && \
-    sed -i.bak '/character/d'   Make && \
-    sed -i.bak '/real_closed/d' Make && \
-    sed -i.bak '/solvable/d'    Make && \
-    sed -i.bak '/field/d'       Make && \
-    sed -i.bak '/fingroup/d'    Make && \
-    sed -i.bak '/algebra/d'     Make && \
-    make Makefile.coq && make -f Makefile.coq all && make install )
+    make Makefile.coq && \
+    make -f Makefile.coq ssreflect/all_ssreflect.vo && \
+    make -f Makefile.coq install )
 
   echo -en 'travis_fold:end:ssr.install\\r'
 
 }
+
+# this installs just the ssreflect + algebra library of math-comp
+install_ssralg()
+{
+  echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r'
+
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
+  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
+    make Makefile.coq && \
+    make -f Makefile.coq algebra/all_algebra.vo && \
+    make -f Makefile.coq install )
+
+  echo -en 'travis_fold:end:ssralg.install\\r'
+
+}
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 920272bcfb..24cd9c4272 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,4 +7,6 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
+install_ssralg
+
 ( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )