aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/README-users.md5
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rw-r--r--dev/ci/ci-common.sh2
-rwxr-xr-xdev/ci/ci-elpi.sh4
-rw-r--r--dev/ci/user-overlays/11764-ppedrot-simplify-template.sh18
5 files changed, 33 insertions, 2 deletions
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
index 6649820f22..994ff87674 100644
--- a/dev/ci/README-users.md
+++ b/dev/ci/README-users.md
@@ -105,5 +105,10 @@ images for testing against Coq master. Using these images is highly
recommended:
- For Docker, see: https://github.com/coq-community/docker-coq
+
+ The https://github.com/coq-community/docker-coq/wiki/CI-setup wiki
+ page contains additional information and templates to help setting
+ Docker-based CI up for your Coq project
+
- For Nix, see the setup at
https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 60c266699c..bd7ee46358 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -214,12 +214,16 @@
: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}"
########################################################################
-# Elpi
+# Elpi + Hierarchy Builder
########################################################################
: "${elpi_CI_REF:=coq-master}"
: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}"
+: "${elpi_hb_CI_REF:=coq-master}"
+: "${elpi_hb_CI_GITURL:=https://github.com/math-comp/hierarchy-builder}"
+: "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}"
+
########################################################################
# fcsl-pcm
########################################################################
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 7aa265cf90..f0dbe485f7 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -19,7 +19,7 @@ then
elif [ -d "$PWD/_build/install/default/" ];
then
# Dune build
- export OCAMLPATH="$PWD/_build/install/default/lib/"
+ export OCAMLPATH="$PWD/_build/install/default/lib/:$OCAMLPATH"
export COQBIN="$PWD/_build/install/default/bin"
export COQLIB="$PWD/_build/install/default/lib/coq"
CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
index d60bf34ba2..4f185db813 100755
--- a/dev/ci/ci-elpi.sh
+++ b/dev/ci/ci-elpi.sh
@@ -6,3 +6,7 @@ ci_dir="$(dirname "$0")"
git_download elpi
( cd "${CI_BUILD_DIR}/elpi" && make && make install )
+
+git_download elpi_hb
+
+( cd "${CI_BUILD_DIR}/elpi_hb" && make && make install )
diff --git a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh
new file mode 100644
index 0000000000..f8871ae158
--- /dev/null
+++ b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "11764" ] || [ "$CI_BRANCH" = "simplify-template" ]; then
+
+ elpi_CI_REF="simplify-template"
+ elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+ equations_CI_REF="simplify-template"
+ equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+ paramcoq_CI_REF="simplify-template"
+ paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq
+
+ mtac2_CI_REF="simplify-template"
+ mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+ rewriter_CI_REF="simplify-template"
+ rewriter_CI_GITURL=https://github.com/ppedrot/rewriter
+
+fi