4 files changed, 47 insertions, 15 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 63d5541f48..8620b01b26 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -226,3 +226,10 @@
 : "${quickchick_CI_REF:=master}"
 : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}"
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${plugin_tutorial_CI_REF:=master}"
+: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
+: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
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/ci-plugin-tutorial.sh b/dev/ci/ci-plugin-tutorial.sh
new file mode 100755
index 0000000000..6c26a71a21
--- /dev/null
+++ b/dev/ci/ci-plugin-tutorial.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download plugin_tutorial
+
+( cd "${CI_BUILD_DIR}/plugin_tutorial" && \
+  pushd tuto0 && make && popd          && \
+  pushd tuto1 && make && popd          && \
+  pushd tuto2 && make && popd          && \
+  pushd tuto3 && make && popd          )
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