aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/appveyor.sh2
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-sf.sh9
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile6
-rw-r--r--dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh15
5 files changed, 22 insertions, 12 deletions
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index d2176e326c..84fec71f7a 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -12,4 +12,4 @@ opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $A
eval "$(opam config env)"
opam install -y num ocamlfind camlp5 ounit
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
+cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 50d4d21637..f422030b53 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -238,7 +238,7 @@
########################################################################
# plugin_tutorial
########################################################################
-: "${plugin_tutorial_CI_REF:=master}"
+: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}"
: "${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-sf.sh b/dev/ci/ci-sf.sh
index 58bbb7229f..60436e672c 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -8,11 +8,6 @@ wget -qO- "${sf_lf_CI_TARURL}" | tar xvz
wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
-sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
-sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
-
-( cd lf && make clean && make )
-
-( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
-
+( cd lf && make clean && make )
+( cd plf && make clean && make )
( cd vfa && make clean && make )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index f257c62dd3..098c950b32 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-04-V2"
+# CACHEKEY: "bionic_coq-V2018-10-23-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
# Common OPAM packages.
# `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 odoc.1.2.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \
CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
@@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
ENV COMPILER_EDGE="4.07.0" \
CAMLP5_VER_EDGE="7.06" \
COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
- BASE_OPAM_EDGE="dune-release.0.3.0"
+ BASE_OPAM_EDGE="dune-release.1.1.0"
RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
new file mode 100644
index 0000000000..b3a9f67e00
--- /dev/null
+++ b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
+
+ # ltac2_CI_REF=rm-section-path
+ # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+ plugin_tutorial_CI_REF=vernac+monify_hook
+ plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
+
+ Elpi_CI_REF=vernac+monify_hook
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ Equations_CI_REF=vernac+monify_hook
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi