diff options
Diffstat (limited to 'dev/ci')
51 files changed, 168 insertions, 347 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 9ed7180807..6a740b9033 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -43,9 +43,10 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab ### Breaking changes When your PR breaks an external project we test in our CI, you must -prepare a patch (or ask someone to prepare a patch) to fix the -project. There is experimental support for an improved workflow, see -[the next section](#experimental-automatic-overlay-creation-and-building), below +prepare a patch (or ask someone—possibly the project author—to +prepare a patch) to fix the project. There is experimental support for +an improved workflow, see [the next +section](#experimental-automatic-overlay-creation-and-building), below are the steps to manually prepare a patch: 1. Fork the external project, create a new branch, push a commit adapting diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 06b617d4c1..994ff87674 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -1,36 +1,40 @@ Information for external library / Coq plugin authors ----------------------------------------------------- -You are encouraged to consider submitting your development for addition to +You are encouraged to consider submitting your project for addition to Coq's CI. This means that: -- Any time that a proposed change is breaking your development, Coq developers - will send you patches to adapt it or, at the very least, will work with you - to see how to adapt it. +- Any time that a proposed change is breaking your project, Coq + developers and contributors will send you patches to adapt it or + will explain how to adapt it and work with you to ensure that you + manage to do it. On the condition that: -- At the time of the submission, your development works with Coq's +- At the time of the submission, your project works with Coq's `master` branch. -- Your development is publicly available in a git repository and we can easily +- Your project is publicly available in a git repository and we can easily send patches to you (e.g. through pull / merge requests). - You react in a timely manner to discuss / integrate those patches. + When seeking your help for preparing such patches, we will accept + that it takes longer than when we are just requesting to integrate a + simple (and already fully prepared) patch. - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. - For that, we recommend setting a CI system for you development, see + For that, we recommend setting a CI system for you project, see [supported CI images for Coq](#supported-ci-images-for-coq) below. -- You maintain a reasonable build time for your development, or you provide +- You maintain a reasonable build time for your project, or you provide a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach -out to you and give you a 30-day grace period during which your development +out to you and give you a 30-day grace period during which your project would be moved into our "allow failure" category. At the end of the grace -period, in the absence of progress, the development would be removed from our +period, in the absence of progress, the project would be removed from our CI. ### Timely merging of overlays @@ -47,7 +51,7 @@ these kind of merges. ### OCaml and plugin-specific considerations -Developments that link against Coq's OCaml API [most of them are known +Projects 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 @@ -65,7 +69,7 @@ as "plugins"] do have some special requirements: 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 your project by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the @@ -75,7 +79,7 @@ Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an example. **Do not hesitate to submit an incomplete pull request if you need help to finish it.** -You may also be interested in having your development tested in our +You may also be interested in having your project tested in our performance benchmark. Currently this is done by providing an OPAM package in https://github.com/coq/opam-coq-archive and opening an issue at https://github.com/coq/coq-bench/issues. @@ -83,13 +87,13 @@ https://github.com/coq/coq-bench/issues. ### Recommended branching policy. It is sometimes the case that you will need to maintain a branch of -your development for particular Coq versions. This is in fact very -likely if your development includes a Coq ML plugin. +your project for particular Coq versions. This is in fact very likely +if your project includes a Coq ML plugin. -We thus recommend a branching convention that mirrors Coq's branching -policy. Then, you would have a `master` branch that follows Coq's -`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so -on. +For such projects, we recommend a branching convention that mirrors +Coq's branching policy. Then, you would have a `master` branch that +follows Coq's `master`, a `v8.8` branch that works with Coq's `v8.8` +branch and so on. This convention will be supported by tools in the future to make some developer commands work more seamlessly. @@ -101,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/azure-opam.sh b/dev/ci/azure-opam.sh index ee6c62673b..7b3e2703b8 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.09.0+mingw64c +OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c 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 diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87122e0fb5..c18e556da8 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -165,13 +165,6 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# fiat_crypto_legacy -######################################################################## -: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" -: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" -: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" - -######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" @@ -207,9 +200,16 @@ : "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" ######################################################################## +# bbv +######################################################################## +: "${bbv_CI_REF:=master}" +: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}" +: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}" + +######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=master}" +: "${bedrock2_CI_REF:=tested}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" @@ -221,12 +221,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 ######################################################################## @@ -256,6 +260,13 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## +# reduction-effects +######################################################################## +: "${reduction_effects_CI_REF:=master}" +: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}" +: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}" + +######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" @@ -326,3 +337,10 @@ : "${perennial_CI_REF:=master}" : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" + +######################################################################## +# metacoq +######################################################################## +: "${metacoq_CI_REF:=master}" +: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" +: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bbv.sh b/dev/ci/ci-bbv.sh new file mode 100755 index 0000000000..6892cea3e4 --- /dev/null +++ b/dev/ci/ci-bbv.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download bbv + +( cd "${CI_BUILD_DIR}/bbv" && make && make install ) 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-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 6cb8dad604..ffe92dcecf 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -7,4 +7,4 @@ install_ssreflect git_download coquelicot -( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/coquelicot" && autoreconf -i -s && ./configure && ./remake "-j${NJOBS}" ) 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/ci-equations.sh b/dev/ci/ci-equations.sh index 871d033f5b..30047e624b 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download equations -( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci) +( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install ) diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh deleted file mode 100755 index 2af4b58201..0000000000 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -FORCE_GIT=1 -git_download fiat_crypto_legacy - -fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" -fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" - -( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ - ./etc/ci/remove_autogenerated.sh && \ - make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 000c418137..811fefda35 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -9,11 +9,15 @@ git_download fiat_crypto # We need a larger stack size to not overflow ocamlopt+flambda when # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_STACKSIZE=32768 -fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1" +# fiat-crypto is not guaranteed to build with the latest version of +# bedrock2, so we use the pinned version of bedrock2, but the external +# version of other developments +fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite" fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && \ + ulimit -s ${fiat_crypto_CI_STACKSIZE} && \ make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh new file mode 100755 index 0000000000..1302065961 --- /dev/null +++ b/dev/ci/ci-metacoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download metacoq + +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 7075d4d7f6..e08dcf07ab 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,10 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download unicoq - -( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) - git_download mtac2 ( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh new file mode 100755 index 0000000000..6b6de3fa2f --- /dev/null +++ b/dev/ci/ci-reduction_effects.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download reduction_effects + +( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 2b1d2298f2..b9d6215e60 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -4,7 +4,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2 -data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) + +# "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}" diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh new file mode 100755 index 0000000000..36acb115e9 --- /dev/null +++ b/dev/ci/ci-unicoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download unicoq + +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index b8f9d99702..e56e4d38ea 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-12-08-V82" +# CACHEKEY: "bionic_coq-V2020-03-19-V29" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -18,7 +18,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc -RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ +RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. @@ -37,12 +37,12 @@ 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.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.8.0" + BASE_ONLY_OPAM="elpi.1.10.2" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" +ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" # Must add this to COQIDE_OPAM{,_EDGE} when we update the opam # packages "lablgtk3-gtksourceview3" @@ -56,13 +56,12 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.09.0" \ - COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12" +ENV COMPILER_EDGE="4.09.1" \ + BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM $CI_OPAM RUN opam clean -a -c diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index a9cc91170f..c8ea59f08a 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; }) let unicoq = callPackage ./unicoq { inherit coq; }; in +let StructTact = coqPackages.StructTact.overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master"; + }); in + +let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master"; + }); in + +let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/verdi/tarball/master"; + }); in + let callPackage = newScope { inherit coq bignums coq-ext-lib coqprime corn iris math-classes - mathcomp simple-io ssreflect stdpp unicoq; + mathcomp simple-io ssreflect stdpp unicoq Verdi; }; in # Environments for building CI libraries with this Coq @@ -77,7 +91,6 @@ let projects = { cross_crypto = callPackage ./cross_crypto.nix {}; Elpi = callPackage ./Elpi.nix {}; fiat_crypto = callPackage ./fiat_crypto.nix {}; - fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; flocq = callPackage ./flocq.nix {}; formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; @@ -89,6 +102,7 @@ let projects = { mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; quickchick = callPackage ./quickchick.nix {}; + verdi-raft = callPackage ./verdi-raft.nix {}; VST = callPackage ./VST.nix {}; }; in diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 0f0ee91387..1105fba7a6 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ -{ coqprime }: +{ ocamlPackages }: { - coqBuildInputs = [ coqprime ]; + buildInputs = with ocamlPackages; [ ocaml findlib ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; - make = "make new-pipeline c-files"; + make = "make c-files printlite lite && make -j 1 coq"; } diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix deleted file mode 100644 index 3248665579..0000000000 --- a/dev/ci/nix/fiat_crypto_legacy.nix +++ /dev/null @@ -1,6 +0,0 @@ -{}: - -{ - configure = "./etc/ci/remove_autogenerated.sh"; - make = "make print-old-pipeline-lite old-pipeline-lite lite-display"; -} diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix new file mode 100644 index 0000000000..6a98f4ef47 --- /dev/null +++ b/dev/ci/nix/verdi-raft.nix @@ -0,0 +1,5 @@ +{ Verdi }: +{ + coqBuildInputs = [ Verdi ]; + configure = "./configure"; +} diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh deleted file mode 100644 index 242b177d71..0000000000 --- a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh +++ /dev/null @@ -1,23 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then - - fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726 - fiat_parsers_CI_REF=master+change-for-coq-pr8726 - fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat - - elpi_CI_BRANCH=coq-master+fix-global-pr8726 - elpi_CI_REF=coq-master+fix-global-pr8726 - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - - equations_CI_BRANCH=master+fix-global-pr8726 - equations_CI_REF=master+fix-global-pr8726 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - mtac2_CI_BRANCH=master+fix-global-pr8726 - mtac2_CI_REF=master+fix-global-pr8726 - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - - paramcoq_CI_BRANCH=master+fix-global-pr8726 - paramcoq_CI_REF=master+fix-global-pr8726 - paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq - -fi diff --git a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh deleted file mode 100644 index e4cf74aa51..0000000000 --- a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9566" ] || [ "$CI_BRANCH" = "proof_global+move_termination_routine_out" ]; then - - aac_tactics_CI_REF=proof_global+move_termination_routine_out - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - equations_CI_REF=proof_global+move_termination_routine_out - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - paramcoq_CI_REF=proof_global+move_termination_routine_out - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh deleted file mode 100644 index 3029f3019c..0000000000 --- a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9645" ] || [ "$CI_BRANCH" = "proof+sayonara_baby" ]; then - - equations_CI_REF=proof+sayonara_baby - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+sayonara_baby - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+sayonara_baby - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh deleted file mode 100644 index a0e9085afd..0000000000 --- a/dev/ci/user-overlays/09867-primitive-floats.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then - - unicoq_CI_REF=primitive-floats - unicoq_CI_GITURL=https://github.com/validsdp/unicoq - - elpi_CI_REF=primitive-floats - elpi_CI_GITURL=https://github.com/validsdp/coq-elpi - - coqhammer_CI_REF=primitive-floats - coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer - -fi diff --git a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh deleted file mode 100644 index c8cf85e73e..0000000000 --- a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10231" ] || [ "$CI_BRANCH" = "master+locating-warning-different-implicit-term-type" ]; then - - equations_CI_REF=master+fix-manual-implicit-pr10231 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - mtac2_CI_REF=master+fix-manual-implicit-pr10231 - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - -fi diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh deleted file mode 100644 index d133bc9993..0000000000 --- a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then - - elpi_CI_REF=proof+recthms - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=proof+recthms - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+recthms - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+recthms - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=proof+recthms - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh deleted file mode 100644 index c5f1510357..0000000000 --- a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then - - mtac2_CI_REF=vernac-when-sideff - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - equations_CI_REF=vernac-when-sideff - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh deleted file mode 100644 index 2c3f490c03..0000000000 --- a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then - - equations_CI_REF=rm-kernel-sideeff-role - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh b/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh deleted file mode 100644 index 288e14c866..0000000000 --- a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10337" ] || [ "$CI_BRANCH" = "vernac+qed_special_case_inject_proof" ]; then - - paramcoq_CI_REF=vernac+qed_special_case_inject_proof - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - equations_CI_REF=vernac+qed_special_case_inject_proof - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh deleted file mode 100644 index 735b2ebbc3..0000000000 --- a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10362" ] || [ "$CI_BRANCH" = "delay-poly-opaque" ]; then - - paramcoq_CI_REF=delay-poly-opaque - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - - elpi_CI_REF=delay-poly-opaque - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - coqhammer_CI_REF=delay-poly-opaque - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - coq_dpdgraph_CI_REF=delay-poly-opaque - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh deleted file mode 100644 index 3122f953de..0000000000 --- a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10406" ] || [ "$CI_BRANCH" = "desync-entry-proof" ]; then - - equations_CI_REF=desync-entry-proof - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - quickchick_CI_REF=desync-entry-proof - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - -fi diff --git a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh deleted file mode 100644 index 0ec0c3673a..0000000000 --- a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10419" ] || [ "$CI_BRANCH" = "heads+test" ]; then - - elpi_CI_REF=heads+test - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=heads+test - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=heads+test - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=heads+test - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=heads+test - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh deleted file mode 100644 index 3a2f4e1001..0000000000 --- a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10434" ] || [ "$CI_BRANCH" = "proof+hook_record" ]; then - - equations_CI_REF=proof+hook_record - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+hook_record - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+hook_record - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh deleted file mode 100644 index 00f544f894..0000000000 --- a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10441" ] || [ "$CI_BRANCH" = "static-poly-section" ]; then - - ext_lib_CI_REF=static-poly-section - ext_lib_CI_GITURL=https://github.com/ppedrot/coq-ext-lib - -fi diff --git a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh deleted file mode 100644 index 10526a9ffe..0000000000 --- a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh +++ /dev/null @@ -1,10 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10476" ] || [ "$CI_BRANCH" = "rm-library-optim" ]; then - - sf_lf_CI_TARURL=https://www.maximedenes.fr/download/lf.tgz - sf_plf_CI_TARURL=https://www.maximedenes.fr/download/plf.tgz - sf_vfa_CI_TARURL=https://www.maximedenes.fr/download/vfa.tgz - - vst_CI_REF=fix-export - vst_CI_GITURL=https://github.com/maximedenes/VST - -fi diff --git a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh b/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh deleted file mode 100644 index 7001c3d0c8..0000000000 --- a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10516" ] || [ "$CI_BRANCH" = "proof+dup_save" ]; then - - elpi_CI_REF=proof+dup_save - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh deleted file mode 100644 index 413805e8e9..0000000000 --- a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then - - elpi_CI_REF=feedback-added-axiom - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh deleted file mode 100644 index 21ff60493b..0000000000 --- a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then - - coqhammer_CI_REF=errors+private - coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - -fi diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh deleted file mode 100644 index 0c47f6a60b..0000000000 --- a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then - - elpi_CI_REF=api+varkind - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - quickchick_CI_REF=api+varkind - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh deleted file mode 100644 index 6dc44aa627..0000000000 --- a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then - - equations_CI_REF=proofs+declare_unif - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh deleted file mode 100644 index f4840c2a83..0000000000 --- a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then - - equations_CI_REF=proof+private_entry - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh deleted file mode 100644 index a5f6551474..0000000000 --- a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then - - elpi_CI_REF=library+to_vernac_step2 - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh deleted file mode 100644 index d7af6b7a36..0000000000 --- a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then - - elpi_CI_REF=sprop-default-on - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - coq_dpdgraph_CI_REF=sprop-default-on - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh deleted file mode 100644 index bb65beb043..0000000000 --- a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh +++ /dev/null @@ -1,19 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then - - elpi_CI_REF=expose-comind-univ - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=expose-comind-univ - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - paramcoq_CI_REF=expose-comind-univ - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - mtac2_CI_REF=expose-comind-univ - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - rewriter_CI_REF=cleanup-comind-univ - rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter - - -fi diff --git a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh deleted file mode 100644 index 7845654375..0000000000 --- a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11051" ] || [ "$CI_BRANCH" = "elpi-1.8" ]; then - - elpi_CI_REF="coq-master+v1.2" - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh deleted file mode 100644 index fb66217487..0000000000 --- a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then - - quickchick_CI_REF=master+adapt-coq-pr11141 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi diff --git a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh deleted file mode 100644 index e0d9dc6469..0000000000 --- a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11172" ] || [ "$CI_BRANCH" = "master+coercion-notation-interleaved-printing" ]; then - - elpi_CI_REF=coq-master+mini-fix-mkGApp - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -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 new file mode 100644 index 0000000000..8a734feada --- /dev/null +++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh @@ -0,0 +1,6 @@ +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 new file mode 100644 index 0000000000..6928925e54 --- /dev/null +++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh @@ -0,0 +1,12 @@ +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 new file mode 100644 index 0000000000..8dae29adb6 --- /dev/null +++ b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh @@ -0,0 +1,9 @@ +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 |