aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/ci-common.sh28
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile4
-rwxr-xr-xdev/ci/gitlab.bat15
-rw-r--r--dev/ci/user-overlays/08552-gares-elpi-11.sh5
4 files changed, 35 insertions, 17 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 7af648f0a6..4acc0e86cf 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,6 +8,7 @@ export NJOBS
if [ -n "${GITLAB_CI}" ];
then
+ # Gitlab build, Coq installed into `_install_ci`
export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
export COQBIN="$PWD/_install_ci/bin"
export CI_BRANCH="$CI_COMMIT_REF_NAME"
@@ -15,18 +16,29 @@ then
then
export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
fi
+elif [ -n "${TRAVIS}" ];
+then
+ # Travis build, `-local` passed to `configure`
+ export OCAMLPATH="$PWD:$OCAMLPATH"
+ export COQBIN="$PWD/bin"
+ export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
+ export CI_BRANCH="$TRAVIS_BRANCH"
+elif [ -d "$PWD/_build/install/default/" ];
+then
+ # Dune build
+ export OCAMLPATH="$PWD/_build/install/default/lib/"
+ export COQBIN="$PWD/_build/install/default/bin"
+ export COQLIB="$PWD/_build/install/default/lib/coq"
+ CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+ export CI_BRANCH
else
- if [ -n "${TRAVIS}" ];
- then
- export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
- export CI_BRANCH="$TRAVIS_BRANCH"
- else # assume local
- CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
- export CI_BRANCH
- fi
+ # We assume we are in `-profile devel` build, thus `-local` is set
export OCAMLPATH="$PWD:$OCAMLPATH"
export COQBIN="$PWD/bin"
+ CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+ export CI_BRANCH
fi
+
export PATH="$COQBIN:$PATH"
# Coq's tools need an ending slash :S, we should fix them.
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index b04161918e..8d0f69626e 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-23-V01"
+# CACHEKEY: "bionic_coq-V2018-09-24-V01"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.02.3"
# `num` does not have a version number as the right version to install varies
# with the compiler version.
ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \
- CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8"
+ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
ENV CAMLP5_VER="6.14" \
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 31bd65af08..a848c49d75 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -8,23 +8,24 @@ TIME /T
REM List currently used cygwin and target folders for debugging / maintenance purposes
ECHO "Currently used cygwin folders"
-DIR C:\cygwin*
+DIR C:\ci\cygwin*
ECHO "Currently used target folders"
-DIR C:\coq*
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
if %ARCH% == 32 (
SET ARCHLONG=i686
- SET CYGROOT=C:\cygwin
SET SETUP=setup-x86.exe
)
if %ARCH% == 64 (
SET ARCHLONG=x86_64
- SET CYGROOT=C:\cygwin64
SET SETUP=setup-x86_64.exe
)
-SET DESTCOQ=C:\coq%ARCH%_inst
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
CALL :MakeUniqueFolder %CYGROOT% CYGROOT
CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
@@ -93,9 +94,9 @@ GOTO :EOF
:CleanupFolders
ECHO "Cleaning %CYGROOT%"
- DEL /S /F /Q "%CYGROOT%" > NUL
+ RMDIR /S /Q "%CYGROOT%"
ECHO "Cleaning %DESTCOQ%"
- DEL /S /F /Q "%DESTCOQ%" > NUL
+ RMDIR /S /Q "%DESTCOQ%"
GOTO :EOF
:MakeUniqueFolder
diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh
new file mode 100644
index 0000000000..c08f44fc50
--- /dev/null
+++ b/dev/ci/user-overlays/08552-gares-elpi-11.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then
+ Elpi_CI_REF=coq-master-elpi-1.1
+fi