Merge PR #6504: Fix overlay selection for Circle CI.

11 files changed, 14 insertions, 39 deletions

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 23131c94c6..58c90ff11d 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -5,8 +5,17 @@ set -xe
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN=`pwd`/_install_ci/bin
-    export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
+    export CI_BRANCH="$CI_COMMIT_REF_NAME"
 else
+    if [ -n "${TRAVIS}" ];
+    then
+        export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
+        export CI_BRANCH="$TRAVIS_BRANCH"
+    elif [ -n "${CIRCLECI}" ];
+    then
+        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
+        export CI_BRANCH="$CIRCLE_BRANCH"
+    fi
     export COQBIN=`pwd`/bin
 fi
 export PATH="$COQBIN:$PATH"
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index af4a96f4ae..7716bcb59a 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,4 +1,4 @@
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
deleted file mode 100644
index 5c4dd1324f..0000000000
--- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then
-    formal_topology_CI_BRANCH=ci
-    formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git
-
-    HoTT_CI_BRANCH=coq-pr-1033
-    HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git
-
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
deleted file mode 100644
index cdca8e525a..0000000000
--- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then
-    ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer
-    ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh
deleted file mode 100644
index 6741cf26fb..0000000000
--- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then
-    ltac2_CI_BRANCH=master
-    ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2
-fi
diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
deleted file mode 100644
index c9f1272bed..0000000000
--- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then
-    ltac2_CI_BRANCH=localityfixyou
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh
deleted file mode 100644
index 68e1901f7f..0000000000
--- a/dev/ci/user-overlays/06217-coqdep-at-once.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then
-    UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git
-fi
diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh
deleted file mode 100644
index 7e9b5febdd..0000000000
--- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then
-    Equations_CI_BRANCH=fix-coq-6324
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh
deleted file mode 100644
index c0dcf79e1d..0000000000
--- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then
-    Equations_CI_BRANCH=econstr+fix_class
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
deleted file mode 100644
index 8aea7dee3a..0000000000
--- a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then
-    Equations_CI_BRANCH=interp+less_impstyle_p2
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 9146d3d521..9f0377ceea 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
 ```
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 ```
+
+(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh))