diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 45 | ||||
| -rw-r--r-- | dev/ci/appveyor.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 128 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 8 | ||||
| -rwxr-xr-x | dev/ci/ci-cross-crypto.sh | 9 | ||||
| -rwxr-xr-x | dev/ci/ci-elpi.sh | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat-crypto-legacy.sh | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-hott.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-math-comp.sh | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 19 | ||||
| -rwxr-xr-x | dev/ci/ci-sf.sh | 9 | ||||
| -rwxr-xr-x | dev/ci/ci-simple-io.sh | 1 | ||||
| -rw-r--r-- | dev/ci/docker/README.md | 36 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 53 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 263 | ||||
| -rw-r--r-- | dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh | 8 | ||||
| -rw-r--r-- | dev/ci/user-overlays/README.md | 8 |
19 files changed, 381 insertions, 221 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 43d680af..60a86362 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project: developer who merges the PR on Coq. There are plans to improve this, cf. [#6724](https://github.com/coq/coq/issues/6724). -Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file. +Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. Advanced GitLab CI information ------------------------------ @@ -136,15 +136,35 @@ rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci` and `make install` is run, then the `_install_ci` directory persists to and is used by the next jobs. -Artifacts can also be downloaded from the GitLab repository. -Currently, available artifacts are: -- the Coq executables and stdlib, in three copies varying in - architecture and OCaml version used to build Coq. -- the Coq documentation, built only in the `build:base` job. When submitting - a documentation PR, this can help reviewers checking the rendered result. +### Artifacts -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. +Build artifacts from GitLab can be linked / downloaded in a systematic +way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts) +for more information. For example, to access the documentation of the +`master` branch, you can do: + +https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + +Browsing artifacts is also possible: +https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + +Above, you can replace `master` and `job` by the desired GitLab branch and job name. + +Currently available artifacts are: + +- the Coq executables and stdlib, in four copies varying in + architecture and OCaml version used to build Coq: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + +- the Coq documentation, built in the `doc:*` jobs. When submitting + a documentation PR, this can help reviewers checking the rendered result: + + + Coq's Reference Manual [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + + Coq's Standard Library Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base + + Coq's ML API Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api ### GitLab and Windows @@ -152,6 +172,11 @@ If your repository has access to runners tagged `windows`, setting the secret variable `WINDOWS` to `enabled` will add jobs building Windows versions of Coq (32bit and 64bit). +If the secret variable `WINDOWS` is set to `enabled_all_addons`, +an extended set of addons will be added to the Windows installer. +This leads to a considerable runtime in CI so this is not enabled +by default for pipelines for pull requests. + The Windows jobs are enabled on Coq's repository, where pipelines for pull requests run. @@ -171,6 +196,6 @@ 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. See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 8f53877f..d2176e32 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -10,6 +10,6 @@ bash opam64/install.sh opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH eval "$(opam config env)" -opam install -y num ocamlfind camlp5 +opam install -y num ocamlfind camlp5 ounit 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 13367794..dd5555e4 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -9,7 +9,8 @@ ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_REF:=mathcomp-1.7.0}" +# Latest commit on master as of Sep 27, 2018 +: "${mathcomp_CI_REF:=5f8d45b54aa98732ec3de43d91814459d5a2f2e4}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" : "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" @@ -20,79 +21,95 @@ ######################################################################## # UniMath ######################################################################## -: "${UniMath_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${UniMath_CI_REF:=17a5f224feb42b562ded5fec79ea937dcb45764c}" : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" : "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" ######################################################################## # Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_REF:=v1.3-8.8}" +# Latest commit on master as of Sep 27, 2018 +: "${unicoq_CI_REF:=1cec038ab34e03109f5587a8aecda1f6c53495dd}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" -: "${mtac2_CI_REF:=v1.0.1-coq8.8}" +# Latest commit on master-sync as of Sep 27, 2018 +: "${mtac2_CI_REF:=e65c2560e5098df5e7333f19db97e9f39e46c3ee}" : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" ######################################################################## # Mathclasses + Corn ######################################################################## -: "${math_classes_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${math_classes_CI_REF:=0f530c713db886ab692bba49862a1cbcbebc8610}" : "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" : "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" -: "${Corn_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${Corn_CI_REF:=f505e489829a968074f53fe18b70a292ad94a9d0}" : "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" : "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" ######################################################################## # Iris ######################################################################## -: "${stdpp_CI_REF:=master}" +# std++ commit pinned in Iris +: "${stdpp_CI_REF:=4fb641edc8d74fbba01fed33d9acbc8a423ea601}" : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_REF:=master}" +# Iris commit pinned in LambdaRust +: "${Iris_CI_REF:=85425d47be677d05d74caff5e1a8a85289d96ae1}" : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${lambdaRust_CI_REF:=fd46e6625eef509a80896dccf6c976545b17ab90}" : "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" : "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" ######################################################################## # HoTT ######################################################################## -: "${HoTT_CI_REF:=V8.8}" +# Latest commit on master as of Sep 3, 2018 +: "${HoTT_CI_REF:=333face272e39175a1b342e14c86c316f572f51f}" : "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" : "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" ######################################################################## # Ltac2 ######################################################################## -: "${ltac2_CI_REF:=0.1}" +: "${ltac2_CI_REF:=v8.9}" : "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" : "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}" ######################################################################## # GeoCoq ######################################################################## -: "${GeoCoq_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${GeoCoq_CI_REF:=a13b48840898fec207b382ab42c0bf0b2f62024b}" : "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" : "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" ######################################################################## # Flocq ######################################################################## -: "${Flocq_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${Flocq_CI_REF:=ff6fc12f269ca055b7b6fd88247ac2697ff6e687}" : "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" : "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" ######################################################################## # Coquelicot ######################################################################## -# ATTENTION: The archive URL might depend on the version +# 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}" @@ -100,53 +117,64 @@ ######################################################################## # CompCert ######################################################################## -# Note: The latest release version of CompCert (3.3) does not compile with Coq 8.8.1 -# This is caused by a compatibility issue with OCaml 4.0.7 -: "${CompCert_CI_REF:=17f9d839df12511a7e327f2840855e70af5ede47}" +# Latest commit on master as of Sep 27, 2018 +: "${CompCert_CI_REF:=020be062488d755236f296fff760c7491e11997b}" : "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" : "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -# Note: The latest release version of VST (2.2) does not compile with Coq 8.8.1 -# Note: newer versions of VST have issues with buildability and licensing -: "${VST_CI_REF:=e49605cf1f1e5ae3bbec3d6554122427a94ae986}" +# Latest commit on master as of Dec 10, 2018 +: "${VST_CI_REF:=f6afb456db69df66c366c36b2d0218d92813f546}" : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" : "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" ######################################################################## +# cross-crypto +######################################################################## +# Latest commit on master as of Sep 27, 2018 +: "${cross_crypto_CI_REF:=453da7e0541798f36d82b6c67a3f4461cd5dc773}" +: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" +: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" + +######################################################################## # fiat_parsers ######################################################################## -: "${fiat_parsers_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${fiat_parsers_CI_REF:=a41e7ee1c5152aecedb354a112d5c8121a499d30}" : "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" : "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}" ######################################################################## # fiat_crypto ######################################################################## -: "${fiat_crypto_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${fiat_crypto_CI_REF:=059f186db67852ac17de78dab1987aab77dd4bdb}" : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## # formal-topology ######################################################################## -: "${formal_topology_CI_REF:=ci}" +# Latest commit on ci as of Sep 27, 2018 +: "${formal_topology_CI_REF:=a2f1aa04db253e4f90fb2aae724cfca42ccd53ab}" : "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_REF:=coq-v8.8}" +# Latest commit on coq-master as of Sep 27, 2018 +: "${coq_dpdgraph_CI_REF:=e14e2bc0108a593f7c64d9af3fc4aec9e8fb1397}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" : "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_REF:=master}" +# Latest commit on master as of Nov 5, 2018 +: "${CoLoR_CI_REF:=4ce3a9fb5f58501aef3c0727c8ba8cc38917399d}" : "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" : "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" @@ -160,77 +188,101 @@ ######################################################################## # TLC ######################################################################## -: "${tlc_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${tlc_CI_REF:=6bce3c31e5c74d9f953de3620deadd9f4cc04023}" : "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_REF:=V8.8.0}" +# Latest commit on master as of Sep 27, 2018 +: "${bignums_CI_REF:=f1a63cb4cce9a79e4406275fbb0ee2269947f8d2}" : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" : "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${bedrock2_CI_REF:=cbf50671ba2d9235060d4e4747d0860f127f3995}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" ######################################################################## # Equations ######################################################################## -: "${Equations_CI_REF:=v1.1-8.8}" +# Latest commit on master as of Sep 26, 2018 +: "${Equations_CI_REF:=477cb9d8aac85e03dad3f992f99646e14d803a0c}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" : "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_REF:=coq-v8.8}" +: "${Elpi_CI_REF:=coq-v8.9}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" : "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm ######################################################################## -: "${fcsl_pcm_CI_REF:=master}" +# Latest commit on master as of Sep 27, 2018 +: "${fcsl_pcm_CI_REF:=51ade0a882ae2ac7df071b41d468df1813504c81}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## +# pidetop +######################################################################## +# Latest commit on v8.9 as of Sep 27, 2018 +: "${pidetop_CI_REF:=ef42320bc0ab75f313e9476e8c8c945ae2116cb5}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" +: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" + +######################################################################## # ext-lib ######################################################################## -# Note: This is the latest commit of the v8.8 branch as of August 31st 2018 -: "${ext_lib_CI_REF:=5dd9cfa51f96fcb785c7c31d8c6bf55af5d93f27}" +# Latest commit on master as of Sep 27, 2018 +: "${ext_lib_CI_REF:=a9c138921fb8c2601e64f1a1702a689120d456f3}" : "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" : "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=0.2}" +# Latest commit on master as of Sep 27, 2018 +: "${simple_io_CI_REF:=e627c087ed8225d70aa7aafe882448fea31fef32}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" ######################################################################## # quickchick ######################################################################## -: "${quickchick_CI_REF:=v1.0.2}" +# Latest commit on master as of Sep 27, 2018 +: "${quickchick_CI_REF:=fae47245b75f049c462601d88e4df2e063841a3b}" : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## +# plugin_tutorial +######################################################################## +# Latest commit on master as of Sep 27, 2018 +: "${plugin_tutorial_CI_REF:=b303b75c18734accc9cd7efe82307b0424426e3f}" +: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" +: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" + +######################################################################## # menhirlib ######################################################################## -: "${menhirlib_CI_REF:=20180827}" +# Latest commit on master as of Sep 27, 2018 +: "${menhirlib_CI_REF:=9e4b304bdbcc1f8d433e005a46eb10480e7ae880}" : "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}" : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## # aac-tactics ######################################################################## -# Note: this is the latest commit of the v8.8 branch as of August 31st 2018 -: "${aactactis_CI_REF:=86ac28259030649ef51460e4de2441c8a1017751}" +# Latest commit on v8.9 as of Dec 17, 2018 +: "${aactactis_CI_REF:=c469b26e409b1bde6a64546df85226079796dbe7}" : "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}" : "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 6fc4293d..7af648f0 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -93,7 +93,7 @@ make() # this installs just the ssreflect library of math-comp install_ssreflect() { - echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + echo 'Installing ssreflect' git_download mathcomp @@ -102,14 +102,12 @@ install_ssreflect() make -f Makefile.coq ssreflect/all_ssreflect.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssr.install\\r' - } # this installs just the ssreflect + algebra library of math-comp install_ssralg() { - echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r' + echo 'Installing ssralg' git_download mathcomp @@ -118,6 +116,4 @@ install_ssralg() make -f Makefile.coq algebra/all_algebra.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssralg.install\\r' - } diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh new file mode 100755 index 00000000..900d12c1 --- /dev/null +++ b/dev/ci/ci-cross-crypto.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download cross_crypto + +( cd "${CI_BUILD_DIR}/cross_crypto" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 7f4ef77d..9b4a06fd 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,7 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -FORCE_GIT=1 git_download Elpi ( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index e0395754..6bf31383 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -10,4 +10,5 @@ fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-d fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" ( cd "${CI_BUILD_DIR}/fiat_crypto" && 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-hott.sh b/dev/ci/ci-hott.sh index 9a0726a1..7eeeb093 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download HoTT -( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 6960a8b9..bc49193b 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -9,13 +9,15 @@ install_ssreflect git_download lambdaRust # Extract required version of Iris -Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +# Iris is already pinned in ci-basic-overlays.sh +#Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris git_download Iris # Extract required version of std++ -stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +# std++ is already pinned in ci-basic-overlays.sh +#stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ git_download stdpp diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 74f1a627..a74f9fa4 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -1,5 +1,6 @@ #!/usr/bin/env bash +# $0 is not the safest way, but... ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 00000000..d22b9c8f --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download pidetop + +# Travis / Gitlab have different filesystem layout due to use of +# `-local`. We need to improve this divergence but if we use Dune this +# "local" oddity goes away automatically so not bothering... +if [ -d "$COQBIN/../lib/coq" ]; then + COQLIB="$COQBIN/../lib/coq/" +else + COQLIB="$COQBIN/../" +fi + +( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install ) + +echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 58bbb722..60436e67 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/ci-simple-io.sh b/dev/ci/ci-simple-io.sh index ddc1590d..e7bcd80d 100755 --- a/dev/ci/ci-simple-io.sh +++ b/dev/ci/ci-simple-io.sh @@ -1,7 +1,6 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" - . "${ci_dir}/ci-common.sh" git_download simple_io diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md new file mode 100644 index 00000000..919e2a73 --- /dev/null +++ b/dev/ci/docker/README.md @@ -0,0 +1,36 @@ +## Overall Docker Setup for Coq's CI. + +This directory provides Docker images to be used by Coq's CI. The +images do support Docker autobuild on `hub.docker.com` and Gitlab's +private registry. + +Gitlab CI will build and tag a Docker by default for every job if the +`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this +variable is usually set to `false` indeed to avoid booting a useless +job. + +## Manual Building + +You can also manually build and push any image: + +- Build the image `docker build -t base:$VERSION .` + +To upload/push to your hub: + +- Create a https://hub.docker.com account. +- Login into your space `docker login --username=$USER` +- Push the image: + + `docker tag base:$VERSION $USER/base:$VERSION` + + `docker push $USER/base:$VERSION` + +## Debugging / Misc + +To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>` + +Each `RUN` command creates an "layer", thus a Docker build is +incremental and it always help to put things updated more often at the +end. + +## Possible Improvements: + +- Use ARG for customizing versions, centralize variable setup; diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index da12f122..332597f3 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-v8.8-V2018-09-20" +# CACHEKEY: "bionic_coq-v8.9-V2018-10-22" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -8,52 +8,63 @@ ENV DEBIAN_FRONTEND="noninteractive" RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of the image, the test-suite and external projects - m4 automake autoconf time wget rsync git gcc-multilib opam \ + m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \ # Dependencies of lablgtk (for CoqIDE) libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk xindy texlive-science tipa hevea \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ - python3-setuptools python3-wheel python3-pip + # Dependencies of stdlib and sphinx doc + texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ + xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + python3-sphinx python3-sphinx-rtd-theme python3-sphinxcontrib.bibtex \ + # Dependencies of source-doc and coq-makefile + texlive-science tipa +# More dependencies of the sphinx doc RUN pip3 install antlr4-python3-runtime +# We need to install OPAM 2.0 manually for now. +RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam + # Basic OPAM setup ENV NJOBS="2" \ + OPAMJOBS="2" \ OPAMROOT=/root/.opamcache \ - OPAMROOTISOK="true" + OPAMROOTISOK="true" \ + OPAMYES="true" # Base opam is the set of base packages required by Coq ENV COMPILER="4.02.3" -RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update - # 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" \ - CI_OPAM="menhir.20180530 ppx_tools_versioned.5.2 ppx_deriving.4.1.5 ocaml-migrate-parsetree.1.0.11 ocamlgraph.1.8.8" +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \ + CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV CAMLP5_VER="6.14" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" -RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM && \ - opam install -j $NJOBS camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM +# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3 +RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ + opam install ocamlfind.1.8.0 && \ + opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM # base+32bit switch -RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER +RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ + opam install ocamlfind.1.8.0 && \ + opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" -RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE +RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ + opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE + +# 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 camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM -# BE+flambda switch -RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM && \ - opam install -j $NJOBS camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM +RUN opam clean -a -c diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index ee1b17b6..66f964a3 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -1,131 +1,132 @@ -@ECHO OFF - -REM This script builds and signs the Windows packages on Gitlab - -ECHO "Start Time" -TIME /T - -REM List currently used cygwin and target folders for debugging / maintenance purposes - -ECHO "Currently used cygwin folders" -DIR C:\cygwin* -ECHO "Currently used target folders" -DIR C:\coq* - -if %ARCH% == 32 ( - SET ARCHLONG=i686 - SET CYGROOT=C:\cygwin - SET SETUP=setup-x86.exe -) - -if %ARCH% == 64 ( - SET ARCHLONG=x86_64 - SET CYGROOT=C:\cygwin64 - SET SETUP=setup-x86_64.exe -) - -SET DESTCOQ=C:\coq%ARCH%_inst - -CALL :MakeUniqueFolder %CYGROOT% CYGROOT -CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ - -powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')" -SET CYGCACHE=%CYGROOT%\var\cache\setup -SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/% -SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% -SET COQREGTESTING=Y -SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin - -if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build -if exist %DESTCOQ%\ rd /s /q %DESTCOQ% - -call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ - -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^ - -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ - -addon=bignums ^ - -addon=equations ^ - -addon=ltac2 ^ - -addon=mtac2 ^ - -addon=mathcomp ^ - -addon=menhir ^ - -addon=menhirlib ^ - -addon=compcert ^ - -addon=vst ^ - -addon=aactactics ^ - -addon=extlib ^ - -addon=quickchick ^ - -addon=coquelicot ^ - -make=N ^ - -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit - -ECHO "Start Artifact Creation" -TIME /T - -mkdir artifacts - -CALL :CopyLogFiles - -copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit -REM The open source archive is only required for release builds -IF DEFINED WIN_CERTIFICATE_PATH ( - 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit -) ELSE ( - REM In non release builds, create a dummy file - ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt -) - -REM DO NOT echo the signing command below, as this would leak secrets in the logs -IF DEFINED WIN_CERTIFICATE_PATH ( - IF DEFINED WIN_CERTIFICATE_PASSWORD ( - ECHO Signing package - @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe - signtool verify /pa dev\nsis\*.exe - ) -) - -ECHO "Finished Artifact Creation" -TIME /T - -CALL :CleanupFolders - -ECHO "Finished Cleanup" -TIME /T - -GOTO :EOF - -:CopyLogFiles - ECHO Copy log files for artifact upload - MKDIR artifacts\buildlogs - COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs - MKDIR artifacts\filelists - COPY %CYGROOT%\build\filelists\* artifacts\filelists - MKDIR artifacts\flagfiles - COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles - GOTO :EOF - -:CleanupFolders - ECHO "Cleaning %CYGROOT%" - DEL /S /F /Q "%CYGROOT%" > NUL - ECHO "Cleaning %DESTCOQ%" - DEL /S /F /Q "%DESTCOQ%" > NUL - GOTO :EOF - -:MakeUniqueFolder - REM Create a uniquely named folder - REM This script is safe because folder creation is atomic - either we create it or fail - REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this) - REM %2 = name of the variable which receives the unique folder name - SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%" - MKDIR "%UNIQUENAME%" - IF ERRORLEVEL 1 GOTO :MakeUniqueFolder - SET "%2=%UNIQUENAME%" - GOTO :EOF - -:ErrorCopyLogFilesAndExit - CALL :CopyLogFiles - REM fall through - -:ErrorExit - CALL :CleanupFolders - ECHO ERROR %0 failed - EXIT /b 1 +@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+
+if %ARCH% == 32 (
+ SET ARCHLONG=i686
+ SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+ SET ARCHLONG=x86_64
+ SET SETUP=setup-x86_64.exe
+)
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+ -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
+ -addon=mathcomp ^
+ -addon=menhir ^
+ -addon=menhirlib ^
+ -addon=compcert ^
+ -addon=extlib ^
+ -addon=quickchick ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics ^
+ -make=N ^
+ -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
+
+CALL :CopyLogFiles
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
+REM The open source archive is only required for release builds
+IF DEFINED WIN_CERTIFICATE_PATH (
+ 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+) ELSE (
+ REM In non release builds, create a dummy file
+ ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
+)
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+ IF DEFINED WIN_CERTIFICATE_PASSWORD (
+ ECHO Signing package
+ @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+ signtool verify /pa dev\nsis\*.exe
+ )
+)
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+ ECHO Copy log files for artifact upload
+ MKDIR artifacts\buildlogs
+ COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
+ MKDIR artifacts\filelists
+ COPY %CYGROOT%\build\filelists\* artifacts\filelists
+ MKDIR artifacts\flagfiles
+ COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
+ GOTO :EOF
+
+:CleanupFolders
+ ECHO "Cleaning %CYGROOT%"
+ RMDIR /S /Q "%CYGROOT%"
+ ECHO "Cleaning %DESTCOQ%"
+ RMDIR /S /Q "%DESTCOQ%"
+ GOTO :EOF
+
+:MakeUniqueFolder
+ REM Create a uniquely named folder
+ REM This script is safe because folder creation is atomic - either we create it or fail
+ REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+ REM %2 = name of the variable which receives the unique folder name
+ SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+ MKDIR "%UNIQUENAME%"
+ IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+ SET "%2=%UNIQUENAME%"
+ GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+ CALL :CopyLogFiles
+ REM fall through
+
+:ErrorExit
+ CALL :CleanupFolders
+ ECHO ERROR %0 failed
+ EXIT /b 1
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index be0058b6..d812df3e 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,3 +1,5 @@ +#!/bin/sh + if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh new file mode 100644 index 00000000..575df074 --- /dev/null +++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=pure-sharing-flag + +if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index b8628979..68afe7ee 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,6 +1,8 @@ # Add overlays for your pull requests in this directory -An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh). +When your pull request breaks an external project we test in our CI and you +have prepared a branch with the fix, you can add an "overlay" to your pull +request to test it with the adapted version of the external project. An overlay is a file which defines where to look for the patched version so that testing is possible. It redefines some variables from @@ -22,10 +24,12 @@ and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). Example: `00669-maximedenes-ssr-merge.sh` containing ``` +#!/bin/sh + if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` -(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) |