1 files changed, 31 insertions, 19 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index d7a356930e..85df249d38 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,8 +8,13 @@ export NJOBS
 
 if [ -n "${GITLAB_CI}" ];
 then
+    export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
+    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
+    then
+        export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+    fi
 else
     if [ -n "${TRAVIS}" ];
     then
@@ -20,8 +25,10 @@ else
         export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
         export CI_BRANCH="$CIRCLE_BRANCH"
     else # assume local
-        export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+        CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+        export CI_BRANCH
     fi
+    export OCAMLPATH="$PWD:$OCAMLPATH"
     export COQBIN="$PWD/bin"
 fi
 export PATH="$COQBIN:$PATH"
@@ -35,10 +42,10 @@ ls "$COQBIN"
 CI_BUILD_DIR="$PWD/_build_ci"
 
 # shellcheck source=ci-basic-overlay.sh
-source "${ci_dir}/ci-basic-overlay.sh"
+. "${ci_dir}/ci-basic-overlay.sh"
 for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
-    source "${overlay}"
+    . "${overlay}"
 done
 
 mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
@@ -66,11 +73,6 @@ git_checkout()
     echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
-checkout_mathcomp()
-{
-  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
-}
-
 make()
 {
     # +x: add x only if defined
@@ -88,19 +90,29 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp "${mathcomp_CI_DIR}"
+  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'
+
+}