diff options
Diffstat (limited to 'dev/ci')
31 files changed, 191 insertions, 89 deletions
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 01769aeddb..06b617d4c1 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is to give merge permissions to someone from the Coq team as to help with these kind of merges. +### OCaml and plugin-specific considerations + +Developments that link against Coq's OCaml API [most of them are known +as "plugins"] do have some special requirements: + +- Coq's OCaml API is not stable. We hope to improve this in the future + but as of today you should expect to have to merge a fair amount of + "overlays", usually in the form of Pull Requests from Coq developers + in order to keep your plugin compatible with Coq master. + + In order to alleviate the load, you can delegate the merging of such + compatibility pull requests to Coq developers themselves, by + granting access to the plugin repository or by using `bots` such as + [Bors](https://github.com/apps/bors) that allow for automatic + management of Pull Requests. + +- Plugins in the CI should compile with the OCaml flags that Coq + uses. In particular, warnings that are considered fatal by the Coq + developers _must_ be also fatal for plugin CI code. + ### Add your development by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh deleted file mode 100644 index f26e0904bc..0000000000 --- a/dev/ci/appveyor.sh +++ /dev/null @@ -1,17 +0,0 @@ -#!/bin/bash - -set -e -x - -APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c -NJOBS=2 - -wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz -tar -xf opam64.tar.xz -bash opam64/install.sh - -opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing -eval "$(opam env)" -opam install -j $NJOBS -y num ocamlfind ounit - -# Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-argosy.sh b/dev/ci/ci-argosy.sh new file mode 100755 index 0000000000..6137526bf4 --- /dev/null +++ b/dev/ci/ci-argosy.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download argosy + +( cd "${CI_BUILD_DIR}/argosy" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 62335ea5d0..95fceb773a 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -81,13 +81,6 @@ : "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}" ######################################################################## -# Ltac2 -######################################################################## -: "${ltac2_CI_REF:=master}" -: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" -: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}" - -######################################################################## # GeoCoq ######################################################################## : "${GeoCoq_CI_REF:=master}" @@ -104,15 +97,9 @@ ######################################################################## # Coquelicot ######################################################################## -# The URL for downloading a tgz snapshot of the master branch is -# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz -# See https://gforge.inria.fr/scm/browser.php?group_id=3599 -# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently, -# we use a fixed version, which has a download path which does fit to our standard mechanism. -# ATTENTION: The archive URL might depend on the version! -: "${Coquelicot_CI_REF:=coquelicot-3.0.2}" -: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" -: "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}" +: "${coquelicot_CI_REF:=master}" +: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" +: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" ######################################################################## # CompCert @@ -261,7 +248,7 @@ : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" ######################################################################## -# relation-algebra +# relation_algebra ######################################################################## : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" @@ -296,3 +283,10 @@ : "${stdlib2_CI_REF:=master}" : "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" : "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" + +######################################################################## +# argosy +######################################################################## +: "${argosy_CI_REF:=master}" +: "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}" +: "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 2d242d80a4..2ac78d3c2b 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index b4d2a9ca4e..7aa265cf90 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -108,10 +108,9 @@ install_ssreflect() git_download mathcomp - ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ - make Makefile.coq && \ - make -f Makefile.coq ssreflect/all_ssreflect.vo && \ - make -f Makefile.coq install ) + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \ + make && \ + make install ) } @@ -123,8 +122,11 @@ install_ssralg() git_download mathcomp ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ - make Makefile.coq && \ - make -f Makefile.coq algebra/all_algebra.vo && \ - make -f Makefile.coq install ) + make -C ssreflect && \ + make -C ssreflect install && \ + make -C fingroup && \ + make -C fingroup install && \ + make -C algebra && \ + make -C algebra install ) } diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 5d8817491d..6cb8dad604 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")" install_ssreflect -FORCE_GIT=1 -git_download Coquelicot +git_download coquelicot -( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh deleted file mode 100755 index 4df22bf249..0000000000 --- a/dev/ci/ci-ltac2.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download ltac2 - -( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install ) diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation_algebra.sh index 84bed5bdfe..84bed5bdfe 100755 --- a/dev/ci/ci-relation-algebra.sh +++ b/dev/ci/ci-relation_algebra.sh diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index e553cbed1b..8eebb3af64 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-03-12-V1" +# CACHEKEY: "bionic_coq-V2019-04-20-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.05.0" # `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.6.2 ounit.2.0.8 odoc.1.4.0" \ - CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8" + CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 5f819f31f9..6c4ccfc14d 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -41,7 +41,6 @@ IF "%WINDOWS%" == "enabled_all_addons" ( SET EXTRA_ADDONS=^
-addon=bignums ^
-addon=equations ^
- -addon=ltac2 ^
-addon=mtac2 ^
-addon=mathcomp ^
-addon=menhir ^
@@ -49,9 +48,9 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot ^
-addon=vst ^
-addon=aactactics
+REM -addon=coquelicot ^
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix index 1d931c858e..d813ddd8d7 100644 --- a/dev/ci/nix/bignums.nix +++ b/dev/ci/nix/bignums.nix @@ -1,5 +1,5 @@ { ocamlPackages }: { - buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ]; + buildInputs = [ ocamlPackages.ocaml ]; } diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix new file mode 100644 index 0000000000..d379bfa73d --- /dev/null +++ b/dev/ci/nix/coquelicot.nix @@ -0,0 +1,9 @@ +{ autoconf, automake, ssreflect }: + +{ + buildInputs = [ autoconf automake ]; + coqBuildInputs = [ ssreflect ]; + configure = "./autogen.sh && ./configure"; + make = "./remake"; + clean = "./remake clean"; +} diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 17070e66ee..a9cc91170f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -72,6 +72,7 @@ let projects = { CoLoR = callPackage ./CoLoR.nix {}; CompCert = callPackage ./CompCert.nix {}; coq_dpdgraph = callPackage ./coq_dpdgraph.nix {}; + coquelicot = callPackage ./coquelicot.nix {}; Corn = callPackage ./Corn.nix {}; cross_crypto = callPackage ./cross_crypto.nix {}; Elpi = callPackage ./Elpi.nix {}; diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix index e153043557..71028ec2dc 100644 --- a/dev/ci/nix/flocq.nix +++ b/dev/ci/nix/flocq.nix @@ -4,4 +4,5 @@ buildInputs = [ autoconf automake ]; configure = "./autogen.sh && ./configure"; make = "./remake"; + clean = "./remake clean"; } diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch index 6d96d94dfc..6d2f6470b1 100644 --- a/dev/ci/nix/unicoq/unicoq-num.patch +++ b/dev/ci/nix/unicoq/unicoq-num.patch @@ -4,19 +4,6 @@ Date: Thu Nov 29 08:59:22 2018 +0000 Make explicit dependency to num -diff --git a/Make b/Make -index 550dc6a..8aa1309 100644 ---- a/Make -+++ b/Make -@@ -9,7 +9,7 @@ src/logger.ml - src/munify.mli - src/munify.ml - src/unitactics.mlg --src/unicoq.mllib -+src/unicoq.mlpack - theories/Unicoq.v - test-suite/munifytest.v - test-suite/microtests.v diff --git a/Makefile.local b/Makefile.local new file mode 100644 index 0000000..88be365 @@ -24,21 +11,3 @@ index 0000000..88be365 +++ b/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package num -diff --git a/src/unicoq.mllib b/src/unicoq.mllib -deleted file mode 100644 -index 2b84e2d..0000000 ---- a/src/unicoq.mllib -+++ /dev/null -@@ -1,3 +0,0 @@ --Logger --Munify --Unitactics -diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack -new file mode 100644 -index 0000000..2b84e2d ---- /dev/null -+++ b/src/unicoq.mlpack -@@ -0,0 +1,3 @@ -+Logger -+Munify -+Unitactics diff --git a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh new file mode 100644 index 0000000000..67f6f8610a --- /dev/null +++ b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then + + ltac2_CI_REF=master-parsing-decimal + ltac2_CI_GITURL=https://github.com/proux01/ltac2 + + quickchick_CI_REF=master-parsing-decimal + quickchick_CI_GITURL=https://github.com/proux01/QuickChick + + Corn_CI_REF=master-parsing-decimal + Corn_CI_GITURL=https://github.com/proux01/corn + + HoTT_CI_REF=master-parsing-decimal + HoTT_CI_GITURL=https://github.com/proux01/HoTT + + stdlib2_CI_REF=master-parsing-decimal + stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 + +fi diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh new file mode 100644 index 0000000000..c04621114f --- /dev/null +++ b/dev/ci/user-overlays/08829-proj-syntax-check.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then + lambdaRust_CI_REF=proj-syntax-check + lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust + lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive +fi diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh new file mode 100644 index 0000000000..dc39ea5ef0 --- /dev/null +++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then + + equations_CI_BRANCH=master+fix-evars_of_term-pr8893 + equations_CI_REF=master+fix-evars_of_term-pr8893 + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh new file mode 100644 index 0000000000..12be1b676a --- /dev/null +++ b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then + + HoTT_CI_REF=rm-hardwired-hint-db + HoTT_CI_GITURL=https://github.com/vbgl/HoTT + + ltac2_CI_REF=rm-hardwired-hint-db + ltac2_CI_GITURL=https://github.com/vbgl/ltac2 + + UniMath_CI_REF=rm-hardwired-hint-db + UniMath_CI_GITURL=https://github.com/vbgl/UniMath + +fi diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh new file mode 100644 index 0000000000..1e1d36d54a --- /dev/null +++ b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then + + elpi_CI_REF=recarg-cleanup + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + quickchick_CI_REF=recarg-cleanup + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh new file mode 100644 index 0000000000..b17454fc4c --- /dev/null +++ b/dev/ci/user-overlays/09733-gares-quotations.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then + + ltac2_CI_REF=quotations + ltac2_CI_GITURL=https://github.com/gares/ltac2 + +fi diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh new file mode 100644 index 0000000000..4b49011de3 --- /dev/null +++ b/dev/ci/user-overlays/09815-token-type.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then + ltac2_CI_REF=token-type + ltac2_CI_GITURL=https://github.com/proux01/ltac2 +fi diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh new file mode 100644 index 0000000000..bb14a8c204 --- /dev/null +++ b/dev/ci/user-overlays/09870-vbgl-recordops.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then + + elpi_CI_REF=pr-9870 + elpi_CI_GITURL=https://github.com/vbgl/coq-elpi + +fi diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh new file mode 100644 index 0000000000..01d3068591 --- /dev/null +++ b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then + + elpi_CI_REF=pretyping-rm-global + elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + coqhammer_CI_REF=pretyping-rm-global + coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer + + equations_CI_REF=pretyping-rm-global + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + + ltac2_CI_REF=pretyping-rm-global + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + paramcoq_CI_REF=pretyping-rm-global + paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq + + mtac2_CI_REF=pretyping-rm-global + mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 + +fi diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh new file mode 100644 index 0000000000..9a6e25d893 --- /dev/null +++ b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then + + elpi_CI_REF=overlay-elpi1.2-coq-master + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh new file mode 100644 index 0000000000..9f9cc19e83 --- /dev/null +++ b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then + + relation_algebra_CI_REF=cleanup-logic-convert-hyp + relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra + +fi diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh new file mode 100644 index 0000000000..0e1449f36c --- /dev/null +++ b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then + + unicoq_CI_REF=whd-for-evar-conv-no-stack + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + +fi diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh new file mode 100644 index 0000000000..2015935dd9 --- /dev/null +++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then + + elpi_CI_REF=canonical-disable-hint + elpi_CI_GITURL=https://github.com/vbgl/coq-elpi + +fi diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh new file mode 100644 index 0000000000..4032b1c6b5 --- /dev/null +++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then + + paramcoq_CI_REF=run_tactic_gen + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + +fi diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh new file mode 100644 index 0000000000..bc8aa33565 --- /dev/null +++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then + + unicoq_CI_REF=detype-anonymous + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + +fi |