aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/README-developers.md7
-rwxr-xr-xdev/ci/azure-build.sh2
-rwxr-xr-xdev/ci/ci-basic-overlay.sh14
-rwxr-xr-xdev/ci/ci-engine_bench.sh8
-rwxr-xr-xdev/ci/ci-sf.sh23
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile9
-rwxr-xr-xdev/ci/gitlab.bat4
-rw-r--r--dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh6
-rw-r--r--dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh6
-rw-r--r--dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh6
-rw-r--r--dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh12
-rw-r--r--dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh9
-rw-r--r--dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh15
-rw-r--r--dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh6
-rw-r--r--dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh24
-rw-r--r--dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh9
-rw-r--r--dev/ci/user-overlays/11948-proux01-hexadecimal.sh12
-rw-r--r--dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh15
-rw-r--r--dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh6
-rw-r--r--dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh6
-rw-r--r--dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh6
-rw-r--r--dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh9
22 files changed, 84 insertions, 130 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index d5c6096100..801e29ac95 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -179,6 +179,11 @@ but if you wish to save more time you can skip the job by setting
This means you will need to change its value when the Docker image
needs to be updated. You can do so for a single pipeline by starting
-it through the web interface.
+it through the web interface. Here is a direct link that you can use
+to trigger such a build:
+`https://gitlab.com/coq/coq/pipelines/new?var[SKIP_DOCKER]=false&ref=pr-XXXXX`.
+Note that this link will give a 404 error if you are not logged in or
+a member of the Coq organization on GitLab. To request to join the
+Coq organization, go to https://gitlab.com/coq to request access.
See also [`docker/README.md`](docker/README.md).
diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh
index 04c7d5db91..494651c5bf 100755
--- a/dev/ci/azure-build.sh
+++ b/dev/ci/azure-build.sh
@@ -4,4 +4,4 @@ set -e -x
cd $(dirname $0)/../..
-make -f Makefile.dune coq coqide-server
+dune build coq.install coqide-server.install
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index b87a9c0392..19ba9de245 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -239,6 +239,13 @@
: "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}"
########################################################################
+# Engine-Bench
+########################################################################
+: "${engine_bench_CI_REF:=master}"
+: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}"
+: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}"
+
+########################################################################
# fcsl-pcm
########################################################################
: "${fcsl_pcm_CI_REF:=master}"
@@ -351,3 +358,10 @@
: "${metacoq_CI_REF:=master}"
: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
+
+########################################################################
+# SF suite
+########################################################################
+: "${sf_CI_REF:=master}"
+: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
+: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh
new file mode 100755
index 0000000000..fda7649f88
--- /dev/null
+++ b/dev/ci/ci-engine_bench.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download engine_bench
+
+( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index b9d6215e60..d46e53717f 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,22 +3,9 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
+git_download sf
-# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
-# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-
-mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
-
-sf_lf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "lf.tgz") | .url')
-sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url')
-sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url')
-
-wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-
-( cd lf && make clean && make )
-( cd plf && make clean && make )
-( cd vfa && make clean && make )
+( cd lf-current && make clean && make )
+( cd plf-current && make clean && make )
+( cd vfa-current && make clean && make )
+# ( cd qc-current && make clean && make )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 9ee6496ee5..0d2f1dfbc7 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-06-V70"
+# CACHEKEY: "bionic_coq-V2020-05-19-V33"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -14,12 +14,13 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
# Dependencies of stdlib and sphinx doc
texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
+ fonts-freefont-otf \
# Dependencies of source-doc and coq-makefile
texlive-science tipa
# More dependencies of the sphinx doc
-RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \
- antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
+RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
+ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2
# We need to install OPAM 2.0 manually for now.
RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
@@ -57,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
# EDGE switch
ENV COMPILER_EDGE="4.10.0" \
- BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0"
+ BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2"
# EDGE+flambda switch, we install CI_OPAM as to be able to use
# `ci-template-flambda` with everything.
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 3998fc6514..dc6423332f 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -54,7 +54,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
-addon=flocq ^
-addon=interval ^
-addon=gappa_tool ^
- -addon=gappa
+ -addon=gappa ^
+ -addon=elpi ^
+ -addon=HB
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh
deleted file mode 100644
index c584438b21..0000000000
--- a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then
-
- quickchick_CI_REF=instance-no-bang
- quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh b/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh
new file mode 100644
index 0000000000..05192facbe
--- /dev/null
+++ b/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11566" ] || [ "$CI_BRANCH" = "exninfo+coercion" ]; then
+
+ mtac2_CI_REF=exninfo+coercion
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
deleted file mode 100644
index 8a734feada..0000000000
--- a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then
-
- quickchick_CI_REF=master+adapting-numTok-new-api-pr11703
- quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
deleted file mode 100644
index 6928925e54..0000000000
--- a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then
-
- equations_CI_REF=proof+more_naming_unif
- equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
- rewriter_CI_REF=proof+more_naming_unif
- rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
-
- elpi_CI_REF=proof+more_naming_unif
- elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh
deleted file mode 100644
index 8dae29adb6..0000000000
--- a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11812" ] || [ "$CI_BRANCH" = "export-hint-globality" ]; then
-
- equations_CI_REF="export-hint-globality"
- equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
- fiat_parsers_CI_REF="export-hint-globality"
- fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
-
-fi
diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
deleted file mode 100644
index e3a8eb07f3..0000000000
--- a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
-
- metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
- metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
-
- elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
- elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
- paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
- paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
- equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
- equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
deleted file mode 100644
index 4170799be7..0000000000
--- a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then
-
- elpi_CI_REF=partial-import
- elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
deleted file mode 100644
index cd6b408813..0000000000
--- a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
+++ /dev/null
@@ -1,24 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then
-
- coqhammer_CI_REF="evar-inst-list"
- coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
-
- elpi_CI_REF="evar-inst-list"
- elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
-
- equations_CI_REF="evar-inst-list"
- equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
- metacoq_CI_REF="evar-inst-list"
- metacoq_CI_GITURL=https://github.com/ppedrot/metacoq
-
- mtac2_CI_REF="evar-inst-list"
- mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
-
- quickchick_CI_REF="evar-inst-list"
- quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
-
- unicoq_CI_REF="evar-inst-list"
- unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
-
-fi
diff --git a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
new file mode 100644
index 0000000000..c9ddb3fb9f
--- /dev/null
+++ b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11922" ] || [ "$CI_BRANCH" = "rm-local-reductionops" ]; then
+
+ equations_CI_REF="rm-local-reductionops"
+ equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+ unicoq_CI_REF="rm-local-reductionops"
+ unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/11948-proux01-hexadecimal.sh b/dev/ci/user-overlays/11948-proux01-hexadecimal.sh
new file mode 100644
index 0000000000..0b3133d1f1
--- /dev/null
+++ b/dev/ci/user-overlays/11948-proux01-hexadecimal.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11948" ] || [ "$CI_BRANCH" = "hexadecimal" ]; then
+
+ stdlib2_CI_REF=hexadecimal
+ stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+ paramcoq_CI_REF=hexadecimal
+ paramcoq_CI_GITURL=https://github.com/proux01/paramcoq
+
+ metacoq_CI_REF=hexadecimal
+ metacoq_CI_GITURL=https://github.com/proux01/metacoq
+
+fi
diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
deleted file mode 100644
index 6bee3c7bb6..0000000000
--- a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
-
- fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
- fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
-
- mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
- mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
-
- metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
- metacoq_CI_GITURL=https://github.com/herbelin/template-coq
-
- unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
- unimath_CI_GITURL=https://github.com/herbelin/UniMath
-
-fi
diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
deleted file mode 100644
index b5faabcfe1..0000000000
--- a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then
-
- elpi_CI_REF=no-mod-univs
- elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
deleted file mode 100644
index 0f8daf418c..0000000000
--- a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then
-
- equations_CI_REF="refiner-rm-v82"
- equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
new file mode 100644
index 0000000000..50eaf0b109
--- /dev/null
+++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then
+
+ elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation
+ elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh b/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh
new file mode 100644
index 0000000000..3b3b20baf1
--- /dev/null
+++ b/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8855" ] || [ "$CI_BRANCH" = "master+more-search-options" ]; then
+
+ coqhammer_CI_REF=master+adapt-pr8855-search-api
+ coqhammer_CI_GITURL=https://github.com/herbelin/coqhammer
+
+ coq_dpdgraph_CI_REF=coq-master+adapt-pr8855-search-api
+ coq_dpdgraph_CI_GITURL=https://github.com/herbelin/coq-dpdgraph
+
+fi
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 12:40:01 +0000