diff options
Diffstat (limited to 'dev/ci')
32 files changed, 298 insertions, 484 deletions
diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh index 494651c5bf..1b02cd45ed 100755 --- a/dev/ci/azure-build.sh +++ b/dev/ci/azure-build.sh @@ -4,4 +4,5 @@ set -e -x cd $(dirname $0)/../.. +eval $(opam env) dune build coq.install coqide-server.install diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 18fdd83218..8bcbd90f0b 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -1,54 +1,71 @@ #!/usr/bin/env bash -# This is the basic overlay set for repositories in the CI. - -# Maybe we should just use Ruby to have real objects... - -# : "${foo:=bar}" sets foo to "bar" if it is unset or null +# This is the list of repositories used by the CI scripts, unless overridden +# by a call to the "overlay" function in ci-common + +declare -a projects # the list of project repos that can be be overlayed + +# checks if the given argument is a known project +function is_in_projects { + for x in "${projects[@]}"; do + if [ "$1" = "$x" ]; then return 0; fi; + done + return 1 +} + +# project <name> <giturl> <ref> [<archiveurl>] +# [<archiveurl>] defaults to <giturl>/archive on github.com +# and <giturl>/-/archive on gitlab +function project { + + local var_ref=${1}_CI_REF + local var_giturl=${1}_CI_GITURL + local var_archiveurl=${1}_CI_ARCHIVEURL + local giturl=$2 + local ref=$3 + local archiveurl=$4 + case $giturl in + *github.com*) archiveurl=${archiveurl:-$giturl/archive} ;; + *gitlab*) archiveurl=${archiveurl:-$giturl/-/archive} ;; + esac + + # register the project in the list of projects + projects[${#projects[*]}]=$1 + + # bash idiom for setting a variable if not already set + : "${!var_ref:=$ref}" + : "${!var_giturl:=$giturl}" + : "${!var_archiveurl:=$archiveurl}" + +} ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_REF:=master}" -: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" -: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" +project mathcomp "https://github.com/math-comp/math-comp" "master" -: "${fourcolor_CI_REF:=master}" -: "${fourcolor_CI_GITURL:=https://github.com/math-comp/fourcolor}" -: "${fourcolor_CI_ARCHIVEURL:=${fourcolor_CI_GITURL}/archive}" +project fourcolor "https://github.com/math-comp/fourcolor" "master" -: "${oddorder_CI_REF:=master}" -: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" -: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" +project oddorder "https://github.com/math-comp/odd-order" "master" ######################################################################## # UniMath ######################################################################## -: "${unimath_CI_REF:=master}" -: "${unimath_CI_GITURL:=https://github.com/UniMath/UniMath}" -: "${unimath_CI_ARCHIVEURL:=${unimath_CI_GITURL}/archive}" +project unimath "https://github.com/UniMath/UniMath" "master" ######################################################################## # Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_REF:=master}" -: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" -: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" +project unicoq "https://github.com/unicoq/unicoq" "master" -: "${mtac2_CI_REF:=master}" -: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" -: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" +project mtac2 "https://github.com/Mtac2/Mtac2" "master" ######################################################################## # Mathclasses + Corn ######################################################################## -: "${math_classes_CI_REF:=master}" -: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" -: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" +project math_classes "https://github.com/coq-community/math-classes" "master" -: "${corn_CI_REF:=master}" -: "${corn_CI_GITURL:=https://github.com/coq-community/corn}" -: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}" +project corn "https://github.com/coq-community/corn" "master" ######################################################################## # Iris @@ -56,342 +73,238 @@ # NB: stdpp and Iris refs are gotten from the opam files in the Iris # and lambdaRust repos respectively. -: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}" -: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" +project stdpp "https://gitlab.mpi-sws.org/iris/stdpp" "" -: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" -: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}" +project iris "https://gitlab.mpi-sws.org/iris/iris" "" -: "${autosubst_CI_REF:=coq86-devel}" -: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}" -: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}" +project autosubst "https://github.com/coq-community/autosubst" "master" -: "${iris_string_ident_CI_REF:=master}" -: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}" -: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}" +project iris_string_ident "https://gitlab.mpi-sws.org/iris/string-ident" "master" -: "${iris_examples_CI_REF:=master}" -: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}" -: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}" +project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master" ######################################################################## # HoTT ######################################################################## -: "${hott_CI_REF:=master}" -: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}" -: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}" +project hott "https://github.com/HoTT/HoTT" "master" ######################################################################## # CoqHammer ######################################################################## -: "${coqhammer_CI_REF:=master}" -: "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}" -: "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}" +project coqhammer "https://github.com/lukaszcz/coqhammer" "master" ######################################################################## # GeoCoq ######################################################################## -: "${geocoq_CI_REF:=master}" -: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" -: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}" +project geocoq "https://github.com/GeoCoq/GeoCoq" "master" ######################################################################## # Flocq ######################################################################## -: "${flocq_CI_REF:=master}" -: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" -: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}" +project flocq "https://gitlab.inria.fr/flocq/flocq" "flocq-3" ######################################################################## # coq-performance-tests ######################################################################## -: "${coq_performance_tests_CI_REF:=master}" -: "${coq_performance_tests_CI_GITURL:=https://github.com/coq-community/coq-performance-tests}" -: "${coq_performance_tests_CI_ARCHIVEURL:=${coq_performance_tests_CI_GITURL}/archive}" +project coq_performance_tests "https://github.com/coq-community/coq-performance-tests" "master" ######################################################################## # coq-tools ######################################################################## -: "${coq_tools_CI_REF:=master}" -: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}" -: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}" +project coq_tools "https://github.com/JasonGross/coq-tools" "master" ######################################################################## # Coquelicot ######################################################################## -: "${coquelicot_CI_REF:=master}" -: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" -: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" +project coquelicot "https://gitlab.inria.fr/coquelicot/coquelicot" "master" ######################################################################## # Coq-interval ######################################################################## -: "${interval_CI_REF:=master}" -: "${interval_CI_GITURL:=https://gitlab.inria.fr/coqinterval/interval}" -: "${interval_CI_ARCHIVEURL:=${interval_CI_GITURL}/-/archive}" +project interval "https://gitlab.inria.fr/coqinterval/interval" "master" ######################################################################## # Gappa stand alone tool ######################################################################## -: "${gappa_tool_CI_REF:=master}" -: "${gappa_tool_CI_GITURL:=https://gitlab.inria.fr/gappa/gappa}" -: "${gappa_tool_CI_ARCHIVEURL:=${gappa_tool_CI_GITURL}/-/archive}" +project gappa_tool "https://gitlab.inria.fr/gappa/gappa" "master" ######################################################################## # Gappa plugin ######################################################################## -: "${gappa_plugin_CI_REF:=master}" -: "${gappa_plugin_CI_GITURL:=https://gitlab.inria.fr/gappa/coq}" -: "${gappa_plugin_CI_ARCHIVEURL:=${gappa_plugin_CI_GITURL}/-/archive}" +project gappa "https://gitlab.inria.fr/gappa/coq" "master" ######################################################################## # CompCert ######################################################################## -: "${compcert_CI_REF:=master}" -: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}" -: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}" +project compcert "https://github.com/AbsInt/CompCert" "master" ######################################################################## # VST ######################################################################## -: "${vst_CI_REF:=master}" -: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" -: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" +project vst "https://github.com/PrincetonUniversity/VST" "master" ######################################################################## # cross-crypto ######################################################################## -: "${cross_crypto_CI_REF:=master}" -: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" -: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" +project cross_crypto "https://github.com/mit-plv/cross-crypto" "master" ######################################################################## # rewriter ######################################################################## -: "${rewriter_CI_REF:=master}" -: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}" -: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}" +project rewriter "https://github.com/mit-plv/rewriter" "master" ######################################################################## # fiat_parsers ######################################################################## -: "${fiat_parsers_CI_REF:=master}" -: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" -: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}" +project fiat_parsers "https://github.com/mit-plv/fiat" "master" ######################################################################## # fiat_crypto ######################################################################## -: "${fiat_crypto_CI_REF:=master}" -: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" -: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" +project fiat_crypto "https://github.com/mit-plv/fiat-crypto" "master" ######################################################################## # 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}" +project fiat_crypto_legacy "https://github.com/mit-plv/fiat-crypto" "sp2019latest" ######################################################################## # coq_dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_REF:=coq-master}" -: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" -: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" +project coq_dpdgraph "https://github.com/Karmaki/coq-dpdgraph" "coq-master" ######################################################################## # CoLoR ######################################################################## -: "${color_CI_REF:=master}" -: "${color_CI_GITURL:=https://github.com/fblanqui/color}" -: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" +project color "https://github.com/fblanqui/color" "master" ######################################################################## # TLC ######################################################################## -: "${tlc_CI_REF:=master-for-coq-ci}" -: "${tlc_CI_GITURL:=https://github.com/charguer/tlc}" -: "${tlc_CI_ARCHIVEURL:=${tlc_CI_GITURL}/archive}" +project tlc "https://github.com/charguer/tlc" "master-for-coq-ci" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_REF:=master}" -: "${bignums_CI_GITURL:=https://github.com/coq/bignums}" -: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" +project bignums "https://github.com/coq/bignums" "master" ######################################################################## # coqprime ######################################################################## -: "${coqprime_CI_REF:=master}" -: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}" -: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" +project coqprime "https://github.com/thery/coqprime" "master" ######################################################################## # bbv ######################################################################## -: "${bbv_CI_REF:=master}" -: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}" -: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}" +project bbv "https://github.com/mit-plv/bbv" "master" ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=tested}" -: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" -: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" +project bedrock2 "https://github.com/mit-plv/bedrock2" "tested" ######################################################################## # Equations ######################################################################## -: "${equations_CI_REF:=master}" -: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" -: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" +project equations "https://github.com/mattam82/Coq-Equations" "master" ######################################################################## # Elpi + Hierarchy Builder ######################################################################## -: "${elpi_CI_REF:=coq-master}" -: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" -: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" +project elpi "https://github.com/LPCIC/coq-elpi" "coq-master" -: "${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}" +project hierarchy_builder "https://github.com/math-comp/hierarchy-builder" "coq-master" ######################################################################## # Engine-Bench ######################################################################## -: "${engine_bench_CI_REF:=master}" -: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}" -: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}" +project engine_bench "https://github.com/mit-plv/engine-bench" "master" ######################################################################## # fcsl-pcm ######################################################################## -: "${fcsl_pcm_CI_REF:=master}" -: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" -: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" +project fcsl_pcm "https://github.com/imdea-software/fcsl-pcm" "master" ######################################################################## # ext-lib ######################################################################## -: "${ext_lib_CI_REF:=master}" -: "${ext_lib_CI_GITURL:=https://github.com/coq-community/coq-ext-lib}" -: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" +project ext_lib "https://github.com/coq-community/coq-ext-lib" "master" ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=master}" -: "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" -: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" +project simple_io "https://github.com/Lysxia/coq-simple-io" "master" ######################################################################## # quickchick ######################################################################## -: "${quickchick_CI_REF:=master}" -: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" -: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" +project quickchick "https://github.com/QuickChick/QuickChick" "master" ######################################################################## # 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}" +project reduction_effects "https://github.com/coq-community/reduction-effects" "master" ######################################################################## # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -: "${menhirlib_CI_REF:=20201122}" -: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}" -: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" +project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122" ######################################################################## # aac_tactics ######################################################################## -: "${aac_tactics_CI_REF:=master}" -: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}" +project aac_tactics "https://github.com/coq-community/aac-tactics" "master" ######################################################################## # paramcoq ######################################################################## -: "${paramcoq_CI_REF:=master}" -: "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}" -: "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" +project paramcoq "https://github.com/coq-community/paramcoq" "master" ######################################################################## # relation_algebra ######################################################################## -: "${relation_algebra_CI_REF:=master}" -: "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" -: "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" +project relation_algebra "https://github.com/damien-pous/relation-algebra" "master" ######################################################################## # StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft ######################################################################## -: "${struct_tact_CI_REF:=master}" -: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" -: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" +project struct_tact "https://github.com/uwplse/StructTact" "master" -: "${inf_seq_ext_CI_REF:=master}" -: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" -: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" +project inf_seq_ext "https://github.com/DistributedComponents/InfSeqExt" "master" -: "${cheerios_CI_REF:=master}" -: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" -: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" +project cheerios "https://github.com/uwplse/cheerios" "master" -: "${verdi_CI_REF:=master}" -: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" -: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" +project verdi "https://github.com/uwplse/verdi" "master" -: "${verdi_raft_CI_REF:=master}" -: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" -: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" +project verdi_raft "https://github.com/uwplse/verdi-raft" "master" ######################################################################## # stdlib2 ######################################################################## -: "${stdlib2_CI_REF:=master}" -: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" -: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" +project stdlib2 "https://github.com/coq/stdlib2" "master" ######################################################################## # argosy ######################################################################## -: "${argosy_CI_REF:=master}" -: "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}" -: "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}" +project argosy "https://github.com/mit-pdos/argosy" "master" ######################################################################## # perennial ######################################################################## -: "${perennial_CI_REF:=coq/tested}" -: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" -: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" +project perennial "https://github.com/mit-pdos/perennial" "coq/tested" ######################################################################## # metacoq ######################################################################## -: "${metacoq_CI_REF:=master}" -: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" -: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" +project metacoq "https://github.com/MetaCoq/metacoq" "master" ######################################################################## # SF suite ######################################################################## -: "${sf_CI_REF:=master}" -: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}" -: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}" +project sf "https://github.com/DeepSpec/sf" "master" ######################################################################## # Coqtail ######################################################################## -: "${coqtail_CI_REF:=master}" -: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}" -: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}" +project coqtail "https://github.com/whonore/Coqtail" "master" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 1a4ebc0e90..8d8f78e10c 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -49,24 +49,38 @@ ls -l "$CI_BUILD_DIR" || true declare -A overlays -overlay() +# overlay <project> <giturl> <ref> <prnumber> [<prbranch>] +# creates an overlay for project using a given url and branch which is +# active for prnumber or prbranch. prbranch defaults to ref. +function overlay() { local project=$1 local ov_url=$2 local ov_ref=$3 - - overlays[${project}_URL]=$ov_url - overlays[${project}_REF]=$ov_ref + local ov_prnumber=$4 + local ov_prbranch=$5 + : "${ov_prbranch:=$ov_ref}" + + if [ "$CI_PULL_REQUEST" = "$ov_prnumber" ] || [ "$CI_BRANCH" = "$ov_prbranch" ]; then + if ! is_in_projects "$project"; then + echo "Error: $1 is not a known project which can be overlayed" + exit 1 + fi + + overlays[${project}_URL]=$ov_url + overlays[${project}_REF]=$ov_ref + fi } set +x +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" + for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null - . "${overlay}" + # the directoy can be empty + if [ -e "${overlay}" ]; then . "${overlay}"; fi done - -# shellcheck source=ci-basic-overlay.sh -. "${ci_dir}/ci-basic-overlay.sh" set -x # [git_download project] will download [project] and unpack it diff --git a/dev/ci/ci-coq_performance_tests.sh b/dev/ci/ci-coq_performance_tests.sh index fde8df8e3d..2fa4d5c776 100755 --- a/dev/ci/ci-coq_performance_tests.sh +++ b/dev/ci/ci-coq_performance_tests.sh @@ -5,4 +5,9 @@ ci_dir="$(dirname "$0")" git_download coq_performance_tests -( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf-Sanity && make validate && make install ) +# run make -k; make again if make fails so that the failing file comes last, so that it's easier to find the error messages in the CI log +function make_full() { + if ! make -k "$@"; then make -k "$@"; exit 1; fi +} + +( cd "${CI_BUILD_DIR}/coq_performance_tests" && make_full coq perf-Sanity && make validate && make install ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 4f185db813..d8caf8ee87 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -7,6 +7,6 @@ git_download elpi ( cd "${CI_BUILD_DIR}/elpi" && make && make install ) -git_download elpi_hb +git_download hierarchy_builder -( cd "${CI_BUILD_DIR}/elpi_hb" && make && make install ) +( cd "${CI_BUILD_DIR}/hierarchy_builder" && make && make install ) diff --git a/dev/ci/ci-gappa.sh b/dev/ci/ci-gappa.sh index c346354b70..1af37aa7c1 100755 --- a/dev/ci/ci-gappa.sh +++ b/dev/ci/ci-gappa.sh @@ -7,6 +7,6 @@ git_download gappa_tool ( cd "${CI_BUILD_DIR}/gappa_tool" && ( if [ ! -x ./configure ]; then autoreconf && touch stamp-config_h.in && ./configure --prefix=${CI_INSTALL_DIR}; fi ) && ./remake "-j${NJOBS}" && ./remake install ) -git_download gappa_plugin +git_download gappa -( cd "${CI_BUILD_DIR}/gappa_plugin" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) +( cd "${CI_BUILD_DIR}/gappa" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md index 16c4ac37d9..ed51c8afd3 100644 --- a/dev/ci/docker/README.md +++ b/dev/ci/docker/README.md @@ -4,31 +4,29 @@ 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. -The Gitlab CI will build a docker image unless the CI environment variable +The Gitlab CI will build a Docker image unless the CI environment variable `SKIP_DOCKER` is set to `true`. This image will be stored in the [Gitlab container registry](https://gitlab.com/coq/coq/container_registry) under the name given by the `CACHEKEY` variable from the [Gitlab CI configuration file](../../../.gitlab-ci.yml). -In Coq's default CI, `SKIP_DOCKER` is set so as to avoid running a lengthy redundant job. +`SKIP_DOCKER` is set to "true" in `https://gitlab.com/coq/coq` to avoid running +a lengthy redundant job. For efficiency, users should enable that setting +in forked repositories after the initial Docker build in the fork succeeds. -It can be used to regenerate a fresh Docker image on Gitlab through the following steps. -- Change the `CACHEKEY` variable to a fresh name in the CI configuration in a new commit. -- Push this commit to a Github PR. This will trigger a Gitlab CI run that will - immediately fail, as the Docker image is missing and the `SKIP_DOCKER` +The steps to generate a new Docker image are: +- Update the `CACHEKEY` variable in .gitlab-ci.yml with the date and md5. +- Submit the change in a PR. This triggers a Gitlab CI run that + immediately fails, as the Docker image is missing and the `SKIP_DOCKER` default value prevents rebuilding the image. -- Run a new pipeline on Gitlab with that PR branch, using the green "Run pipeline" - button on the [web interface](https://gitlab.com/coq/coq/pipelines), - with the `SKIP_DOCKER` environment variable set to `false`. This will run a `docker-boot` process, and - once completed, a new Docker image will be available in the container registry, - with the name set in `CACHEKEY`. +- Run a new pipeline on Gitlab with that PR branch (e.g. "pr-99999"), using the green + "Run pipeline" button on the [web interface](https://gitlab.com/coq/coq/pipelines), + with the `SKIP_DOCKER` environment variable set to `false`. This will run a + `docker-boot` process, and once completed, a new Docker image will be available in + the container registry, with the name set in `CACHEKEY`. - Any pipeline with the same `CACHEKEY` will now automatically reuse that image without rebuilding it from scratch. -For documentation purposes, we also require keeping in sync the `CACHEKEY` comment -from the first line of the [Dockerfile](bionic_coq/Dockerfile) in the same -commit. - In case you do not have the rights to run Gitlab CI pipelines, you should ask the ci-maintainers Github team to do it for you. diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 1aefebb007..8f14625c63 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -44,7 +44,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.12.0" + BASE_ONLY_OPAM="elpi.1.13.0" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" @@ -71,3 +71,6 @@ RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM $CI_OPAM RUN opam clean -a -c + +# set the locale for the benefit of Python +ENV LANG C.UTF-8 diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat deleted file mode 100755 index dc6423332f..0000000000 --- a/dev/ci/gitlab.bat +++ /dev/null @@ -1,141 +0,0 @@ -@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%
-SET CYGCACHE=C:\ci\cache\cgwin
-
-CALL :MakeUniqueFolder %CYGROOT% CYGROOT
-CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
-
-powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%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 "%WINDOWS%" == "enabled_all_addons" (
- SET EXTRA_ADDONS=^
- -addon=bignums ^
- -addon=equations ^
- -addon=mtac2 ^
- -addon=mathcomp ^
- -addon=menhir ^
- -addon=menhirlib ^
- -addon=compcert ^
- -addon=extlib ^
- -addon=quickchick ^
- -addon=coquelicot ^
- -addon=vst ^
- -addon=aactactics ^
- -addon=flocq ^
- -addon=interval ^
- -addon=gappa_tool ^
- -addon=gappa ^
- -addon=elpi ^
- -addon=HB
-) ELSE (
- SET "EXTRA_ADDONS= "
-)
-
-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% ^
- %EXTRA_ADDONS% ^
- -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/platform-windows.bat b/dev/ci/platform-windows.bat new file mode 100755 index 0000000000..513aec5f94 --- /dev/null +++ b/dev/ci/platform-windows.bat @@ -0,0 +1,105 @@ +REM @ECHO OFF
+
+REM SET ARCH=64
+REM SET PLATFORM=https://github.com/coq/platform/archive/v8.13.zip
+REM SET CI_PROJECT_DIR=C:\root
+
+REM This script builds a minimal Windows platform 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:\
+ECHO "Powershell version"
+powershell -Command "Get-Host"
+ECHO "Git installation of Mingw"
+DIR "C:\Program Files\Git\mingw64\bin\*.exe"
+
+ECHO "--------- START -------"
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+
+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\Git\mingw64\bin
+
+
+ECHO "Downloading %PLATFORM%"
+curl -L -o platform.zip "%PLATFORM%"
+7z x platform.zip
+
+cd platform-*
+
+call coq_platform_make_windows.bat ^
+ -arch=%ARCH% ^
+ -destcyg=%CYGROOT% ^
+ -cygcache=%CYGCACHE% ^
+ -extent=i ^
+ -parallel=p ^
+ -jobs=2 ^
+ -switch=d || GOTO ErrorCopyLogFilesAndExit
+
+cd ..
+
+SET BASH=%CYGROOT%\bin\bash
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+MKDIR %CI_PROJECT_DIR%\artifacts
+%BASH% --login -c "cd coq-platform && windows/create_installer_windows.sh && cp windows_installer/*.exe %CI_PROJECT_DIR_CFMT%/artifacts" || GOTO ErrorCopyLogFilesAndExit
+TIME /T
+
+CALL :CopyLogFiles
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+ ECHO Copy log files for artifact upload
+ REM This is currently not supported by the opam based build scripts
+ GOTO :EOF
+
+:CleanupFolders
+ ECHO "Cleaning %CYGROOT%"
+ RMDIR /S /Q "%CYGROOT%"
+ 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
+ RMDIR "%UNIQUENAME%"
+ 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/09710-ppedrot-compact-case-repr.sh b/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh new file mode 100644 index 0000000000..dc57e6efb9 --- /dev/null +++ b/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh @@ -0,0 +1,9 @@ +overlay coq_dpdgraph https://github.com/ppedrot/coq-dpdgraph compact-case-repr 13563 +overlay coqhammer https://github.com/ppedrot/coqhammer compact-case-repr 13563 +overlay elpi https://github.com/ppedrot/coq-elpi compact-case-repr 13563 +overlay equations https://github.com/ppedrot/Coq-Equations compact-case-repr 13563 +overlay metacoq https://github.com/ppedrot/metacoq compact-case-repr 13563 +overlay mtac2 https://github.com/ppedrot/Mtac2 compact-case-repr 13563 +overlay paramcoq https://github.com/ppedrot/paramcoq compact-case-repr 13563 +overlay relation_algebra https://github.com/ppedrot/relation-algebra compact-case-repr 13563 +overlay unicoq https://github.com/ppedrot/unicoq compact-case-repr 13563 diff --git a/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh b/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh deleted file mode 100644 index d9b49ad0d1..0000000000 --- a/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12218" ] || [ "$CI_BRANCH" = "numeral-notations-non-inductive" ]; then - - stdlib2_CI_REF=numeral-notations-non-inductive - stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 - - hott_CI_REF=numeral-notations-non-inductive - hott_CI_GITURL=https://github.com/proux01/HoTT - - paramcoq_CI_REF=numeral-notations-non-inductive - paramcoq_CI_GITURL=https://github.com/proux01/paramcoq - - quickchick_CI_REF=numeral-notations-non-inductive - quickchick_CI_GITURL=https://github.com/proux01/QuickChick - - metacoq_CI_REF=numeral-notations-non-inductive - metacoq_CI_GITURL=https://github.com/proux01/metacoq - -fi diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh deleted file mode 100644 index fb5947d218..0000000000 --- a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then - - mtac2_CI_REF=janno/coq-12449 - mtac2_CI_GITURL=https://github.com/mtac2/mtac2 - -fi diff --git a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh deleted file mode 100644 index b7d21ed59c..0000000000 --- a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then - - elpi_CI_REF=record+refactor - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -# mtac2_CI_REF=record+refactor -# mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh deleted file mode 100644 index 1473f6df8b..0000000000 --- a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12653" ] || [ "$CI_BRANCH" = "cumul-syntax" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi cumul-syntax - - overlay equations https://github.com/SkySkimmer/Coq-Equations cumul-syntax - - overlay mtac2 https://github.com/SkySkimmer/Mtac2 cumul-syntax - - overlay paramcoq https://github.com/SkySkimmer/paramcoq cumul-syntax - - overlay rewriter https://github.com/SkySkimmer/rewriter cumul-syntax - - overlay metacoq https://github.com/SkySkimmer/metacoq cumul-syntax - -fi diff --git a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh deleted file mode 100644 index 7680e8da78..0000000000 --- a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12873" ] || [ "$CI_BRANCH" = "master+minifix-unification-error-reporting-recheck-applications" ]; then - - equations_CI_REF=master+fix12873-better-unification - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh b/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh deleted file mode 100644 index 8b223719ea..0000000000 --- a/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13075" ] || [ "$CI_BRANCH" = "explicit-names-quotient" ]; then - - elpi_CI_REF=explicit-names-quotient - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - coq_dpdgraph_CI_REF=explicit-names-quotient - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh deleted file mode 100644 index f16cf1497e..0000000000 --- a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance - -fi diff --git a/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh b/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh deleted file mode 100644 index 2f70f43a2b..0000000000 --- a/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13139" ] || [ "$CI_BRANCH" = "clean-hint-constr" ]; then - - equations_CI_REF=clean-hint-constr - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - fiat_parsers_CI_REF=clean-hint-constr - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat - -fi diff --git a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh deleted file mode 100644 index 7d55cf6883..0000000000 --- a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then - - elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh b/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh new file mode 100644 index 0000000000..27e7cee42e --- /dev/null +++ b/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13299" ] || [ "$CI_BRANCH" = "preserve-universes-notation" ]; then + + elpi_CI_REF=overlay-universes-in-notations + elpi_CI_GITURL=https://github.com/jashug/coq-elpi + +fi diff --git a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh deleted file mode 100644 index 3bdbcf7d6e..0000000000 --- a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then - - overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single - overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single - -fi diff --git a/dev/ci/user-overlays/13321-ppedrot-mv-evaluable-global-ref-out-of-kernel.sh b/dev/ci/user-overlays/13321-ppedrot-mv-evaluable-global-ref-out-of-kernel.sh new file mode 100644 index 0000000000..0f62d0ee9f --- /dev/null +++ b/dev/ci/user-overlays/13321-ppedrot-mv-evaluable-global-ref-out-of-kernel.sh @@ -0,0 +1 @@ +overlay equations https://github.com/ppedrot/Coq-Equations mv-evaluable-global-ref-out-of-kernel 13321 diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh deleted file mode 100644 index 95f0de2bd3..0000000000 --- a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then - - unicoq_CI_REF=master+adapting-coq-pr13386 - unicoq_CI_GITURL=https://github.com/herbelin/unicoq - - elpi_CI_REF=coq-master+adapting-coq-pr13386 - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh deleted file mode 100644 index 0bf806085e..0000000000 --- a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then - - overlay equations https://github.com/SkySkimmer/Coq-Equations intern-univs - - overlay paramcoq https://github.com/SkySkimmer/paramcoq intern-univs - - overlay elpi https://github.com/SkySkimmer/coq-elpi intern-univs -fi diff --git a/dev/ci/user-overlays/13481-elpi-1.12.sh b/dev/ci/user-overlays/13481-elpi-1.12.sh deleted file mode 100644 index a6be2e3a1a..0000000000 --- a/dev/ci/user-overlays/13481-elpi-1.12.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13481" ] || [ "$CI_BRANCH" = "elpi-1.12" ]; then - - elpi_CI_REF=coq-master+elpi.1.12 - elpi_hb_CI_REF=coq-master+coq-elpi-1.7.0+elpi-1.12 - -fi diff --git a/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh new file mode 100644 index 0000000000..4c8cdbbb45 --- /dev/null +++ b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then + + overlay perennial https://github.com/herbelin/perennial master+adapt13512-fresness-names-apply-in-introduction-pattern + +fi diff --git a/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh new file mode 100644 index 0000000000..aa686ea619 --- /dev/null +++ b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13537" ] || [ "$CI_BRANCH" = "lazy-subst-kernel" ]; then + + overlay mtac2 https://github.com/ppedrot/Mtac2 lazy-subst-kernel + +fi diff --git a/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh new file mode 100644 index 0000000000..69bd038b78 --- /dev/null +++ b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh @@ -0,0 +1 @@ +overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725 diff --git a/dev/ci/user-overlays/13844-gares-command-loc.sh b/dev/ci/user-overlays/13844-gares-command-loc.sh new file mode 100644 index 0000000000..d9a1736532 --- /dev/null +++ b/dev/ci/user-overlays/13844-gares-command-loc.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/LPCIC/coq-elpi command-loc 13844 diff --git a/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh new file mode 100644 index 0000000000..6847bde6d8 --- /dev/null +++ b/dev/ci/user-overlays/13847-gares-elpi-1.13-coq-elpi-1.9.0.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.0 13847 diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 3f9ad5e878..cf1d71c1cd 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -5,30 +5,29 @@ 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. This is done by calling the -`overlay` command for each project with the project name (as used in -the variables in [`ci-basic-overlay.sh`](../ci-basic-overlay.sh)), the -location of your fork and the branch containing the patch on your -fork. - -Moreover, the file contains very simple logic to test the pull request number -or branch name and apply it only in this case. - +version so that testing is possible. The name of your overlay file should start with a five-digit pull request number, followed by a dash, anything (for instance your GitHub nickname and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). -Example: `13128-SkySkimmer-noinstance.sh` containing - +This file must contain one or more invocation of the `overlay` function: ``` -if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance +overlay <project> <giturl> <ref> <prnumber> [<prbranch>] +``` +Each call creates an overlay for `project` using a given `giturl` and +`ref` which is active for `prnumber` or `prbranch` (`prbranch` defaults +to `ref`). -fi +Example of an overlay for the project `elpi` that uses the branch `noinstance` +from the fork of `SkySkimmer` and is active for pull request `13128` +``` +overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128 ``` -(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) +Such a file can be created automatically using the scripts +[`create_overlays.sh`](../../dev/tools/create_overlays.sh). +See also the list of projects for which one can write an overlay in +the file [`ci-basic-overlay.sh`](../ci-basic-overlay.sh). ### Branching conventions |