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

validsdp · Jun 10, 2018 · f713d98 · f713d98
1 parent 51a56b1
commit f713d98
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 10 deletions.
diff --git 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
@@ -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 )
Original file line number	Diff line number	Diff line change
Expand Up		@@ -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 )