diff options
Diffstat (limited to 'dev/ci')
40 files changed, 1152 insertions, 0 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md new file mode 100644 index 00000000..43d680af --- /dev/null +++ b/dev/ci/README.md @@ -0,0 +1,176 @@ +Continuous Integration for the Coq Proof Assistant +================================================== + +Changes to Coq are systematically tested for regression and compatibility +breakage on our Continuous Integration (CI) platforms *before* integration, +so as to ensure better robustness and catch problems as early as possible. +These tests include the compilation of several external libraries / plugins. + +This document contains information for both external library / plugin authors, +who might be interested in having their development tested, and for Coq +developers / contributors, who must ensure that they don't break these +external developments accidentally. + +*Remark:* the CI policy outlined in this document is susceptible to evolve and +specific accommodations are of course possible. + +Information for external library / plugin authors +------------------------------------------------- + +You are encouraged to consider submitting your development for addition to +our CI. This means that: + +- Any time that a proposed change is breaking your development, Coq developers + will send you patches to adapt it or, at the very least, will work with you + to see how to adapt it. + +On the condition that: + +- At the time of the submission, your development works with Coq master branch. + +- Your development is publicly available in a git repository and we can easily + send patches to you (e.g. through pull / merge requests). + +- You react in a timely manner to discuss / integrate those patches. + +- You do not push, to the branches that we test, commits that haven't been + first tested to compile with the corresponding branch(es) of Coq. + +- You maintain a reasonable build time for your development, or you provide + a "lite" target that we can use. + +In case you forget to comply with these last three conditions, we would reach +out to you and give you a 30-day grace period during which your development +would be moved into our "allow failure" category. At the end of the grace +period, in the absence of progress, the development would be removed from our +CI. + +### Add your development by submitting a pull request + +Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding +variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the +corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. +Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an +example. **Do not hesitate to submit an incomplete pull request if you need +help to finish it.** + +You may also be interested in having your development tested in our +performance benchmark. Currently this is done by providing an OPAM package +in https://github.com/coq/opam-coq-archive and opening an issue at +https://github.com/coq/coq-bench/issues. + + +Information for developers +-------------------------- + +When you submit a pull request (PR) on Coq GitHub repository, this will +automatically launch a battery of CI tests. The PR will not be integrated +unless these tests pass. + +We are currently running tests on the following platforms: + +- GitLab CI is the main CI platform. It tests the compilation of Coq, of the + documentation, and of CoqIDE on Linux with several versions of OCaml / + camlp5, and with warnings as errors; it runs the test-suite and tests the + compilation of several external developments. + +- Travis CI is used to test the compilation of Coq and run the test-suite on + macOS. It also runs a linter that checks whitespace discipline. A + [pre-commit hook](../tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline without pain. + +- AppVeyor is used to test the compilation of Coq and run the test-suite on + Windows. + +You can anticipate the results of most of these tests prior to submitting your +PR by running GitLab CI on your private branches. To do so follow these steps: + +1. Log into GitLab CI (the easiest way is to sign in with your GitHub account). +2. Click on "New Project". +3. Choose "CI / CD for external repository" then click on "GitHub". +4. Find your fork of the Coq repository and click on "Connect". +5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project). +6. You are encouraged to go to the CI / CD general settings and increase the + timeout from 1h to 2h for better reliability. + +Now everytime you push (including force-push unless you changed the default +GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and +CI will be run. You will receive an e-mail with a report of the failures if +there are some. + +You can also run one CI target locally (using `make ci-somedev`). + +See also [`test-suite/README.md`](../../test-suite/README.md) for information about adding new tests to the test-suite. + +### Breaking changes + +When your PR breaks an external project we test in our CI, you must prepare a +patch (or ask someone to prepare a patch) to fix the project: + +1. Fork the external project, create a new branch, push a commit adapting + the project to your changes. +2. Test your pull request with your adapted version of the external project by + adding an overlay file to your pull request (cf. + [`dev/ci/user-overlays/README.md`](user-overlays/README.md)). +3. Fixes to external libraries (pure Coq projects) *must* be backward + compatible (i.e. they should also work with the development version of Coq, + and the latest stable version). This will allow you to open a PR on the + external project repository to have your changes merged *before* your PR on + Coq can be integrated. + + On the other hand, patches to plugins (projects linking to the Coq ML API) + can very rarely be made backward compatible and plugins we test will + generally have a dedicated branch per Coq version. + You can still open a pull request but the merging will be requested by the + 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. + +Advanced GitLab CI information +------------------------------ + +GitLab CI is set up to use the "build artifact" feature to avoid +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. + +As an exception to the above, jobs testing that compilation triggers +no OCaml warnings build Coq in parallel with other tests. + +### GitLab and Windows + +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). + +The Windows jobs are enabled on Coq's repository, where pipelines for +pull requests run. + +### GitLab and Docker + +System and opam packages are installed in a Docker image. The image is +automatically built and uploaded to your GitLab registry, and is +loaded by subsequent jobs. + +**IMPORTANT**: When updating Coq's CI docker image, you must modify +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) +and [`Dockerfile`](docker/bionic_coq/Dockerfile) + +The Docker building job reuses the uploaded image if it is available, +but if you wish to save more time you can skip the job by setting +`SKIP_DOCKER` to `true`. + +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.. + +See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat new file mode 100644 index 00000000..85a71baf --- /dev/null +++ b/dev/ci/appveyor.bat @@ -0,0 +1,42 @@ +REM This script either runs the test suite with OPAM (if USEOPAM is true) or +REM builds the Coq binary packages for windows (if USEOPAM is false). + +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 CYGCACHE=%CYGROOT%\var\cache\setup +SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/% +SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/% +SET DESTCOQ=C:\coq%ARCH%_inst +SET COQREGTESTING=Y + +if %USEOPAM% == false ( + call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ + -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ + -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -addon=bignums -make=N ^ + -setup %CYGROOT%\%SETUP% || GOTO ErrorExit + copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit + 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit +) + +if %USEOPAM% == true ( + %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^ + -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time + %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit +) + +GOTO :EOF + +:ErrorExit + ECHO ERROR %0 failed + EXIT /b 1 diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh new file mode 100644 index 00000000..8f53877f --- /dev/null +++ b/dev/ci/appveyor.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +set -e -x + +APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c + +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz +tar -xf opam64.tar.xz +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 + +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 new file mode 100755 index 00000000..13367794 --- /dev/null +++ b/dev/ci/ci-basic-overlay.sh @@ -0,0 +1,236 @@ +#!/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 + +######################################################################## +# MathComp +######################################################################## +: "${mathcomp_CI_REF:=mathcomp-1.7.0}" +: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" +: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" + +: "${oddorder_CI_REF:=master}" +: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" +: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" + +######################################################################## +# UniMath +######################################################################## +: "${UniMath_CI_REF:=master}" +: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" +: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" + +######################################################################## +# Unicoq + Mtac2 +######################################################################## +: "${unicoq_CI_REF:=v1.3-8.8}" +: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" +: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" + +: "${mtac2_CI_REF:=v1.0.1-coq8.8}" +: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" +: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" + +######################################################################## +# 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}" + +: "${Corn_CI_REF:=master}" +: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" +: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" + +######################################################################## +# Iris +######################################################################## +: "${stdpp_CI_REF:=master}" +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" + +: "${Iris_CI_REF:=master}" +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" + +: "${lambdaRust_CI_REF:=master}" +: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" +: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" + +######################################################################## +# HoTT +######################################################################## +: "${HoTT_CI_REF:=V8.8}" +: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" + +######################################################################## +# Ltac2 +######################################################################## +: "${ltac2_CI_REF:=0.1}" +: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" +: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}" + +######################################################################## +# GeoCoq +######################################################################## +: "${GeoCoq_CI_REF:=master}" +: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" +: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" + +######################################################################## +# Flocq +######################################################################## +: "${Flocq_CI_REF:=master}" +: "${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 +: "${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}" + +######################################################################## +# 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}" +: "${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}" +: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" + +######################################################################## +# 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}" + +######################################################################## +# 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}" + +######################################################################## +# formal-topology +######################################################################## +: "${formal_topology_CI_REF:=ci}" +: "${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}" +: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" +: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" + +######################################################################## +# CoLoR +######################################################################## +: "${CoLoR_CI_REF:=master}" +: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" +: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" + +######################################################################## +# SF +######################################################################## +: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}" +: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}" +: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}" + +######################################################################## +# TLC +######################################################################## +: "${tlc_CI_REF:=master}" +: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" + +######################################################################## +# Bignums +######################################################################## +: "${bignums_CI_REF:=V8.8.0}" +: "${bignums_CI_GITURL:=https://github.com/coq/bignums}" +: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" + +######################################################################## +# bedrock2 +######################################################################## +: "${bedrock2_CI_REF:=master}" +: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" +: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" + +######################################################################## +# Equations +######################################################################## +: "${Equations_CI_REF:=v1.1-8.8}" +: "${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_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" + +######################################################################## +# 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}" + +######################################################################## +# ext-lib +######################################################################## +# Note: This is the latest commit of the v8.8 branch as of August 31st 2018 +: "${ext_lib_CI_REF:=5dd9cfa51f96fcb785c7c31d8c6bf55af5d93f27}" +: "${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}" +: "${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}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" +: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" + +######################################################################## +# menhirlib +######################################################################## +: "${menhirlib_CI_REF:=20180827}" +: "${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}" +: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}" +: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh new file mode 100755 index 00000000..52059462 --- /dev/null +++ b/dev/ci/ci-bedrock2.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download bedrock2 + +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh new file mode 100755 index 00000000..756f54df --- /dev/null +++ b/dev/ci/ci-bignums.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download bignums + +( cd "${CI_BUILD_DIR}/bignums" && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh new file mode 100755 index 00000000..dc696f69 --- /dev/null +++ b/dev/ci/ci-color.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download CoLoR + +( cd "${CI_BUILD_DIR}/CoLoR" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh new file mode 100644 index 00000000..6fc4293d --- /dev/null +++ b/dev/ci/ci-common.sh @@ -0,0 +1,123 @@ +#!/usr/bin/env bash + +set -xe + +# default value for NJOBS +: "${NJOBS:=1}" +export NJOBS + +if [ -n "${GITLAB_CI}" ]; +then + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" + export COQBIN="$PWD/_install_ci/bin" + export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi +else + if [ -n "${TRAVIS}" ]; + then + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" + else # assume local + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH + fi + export OCAMLPATH="$PWD:$OCAMLPATH" + export COQBIN="$PWD/bin" +fi +export PATH="$COQBIN:$PATH" + +# Coq's tools need an ending slash :S, we should fix them. +export COQBIN="$COQBIN/" + +ls "$COQBIN" + +# Where we download and build external developments +CI_BUILD_DIR="$PWD/_build_ci" + +for overlay in "${ci_dir}"/user-overlays/*.sh; do + # shellcheck source=/dev/null + . "${overlay}" +done +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" + +# [git_download project] will download [project] and unpack it +# in [$CI_BUILD_DIR/project] if the folder does not exist already; +# if it does, it will do nothing except print a warning (this can be +# useful when building locally). +# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty +# (local build), it uses git clone to perform the download. +git_download() +{ + local PROJECT=$1 + local DEST="$CI_BUILD_DIR/$PROJECT" + + if [ -d "$DEST" ]; then + echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." + elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + git clone "$GITURL" "$DEST" + cd "$DEST" + git checkout "$REF" + else # When possible, we download tarballs to reduce bandwidth and latency + local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" + local ARCHIVEURL="${!ARCHIVEURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + mkdir -p "$DEST" + cd "$DEST" + wget "$ARCHIVEURL/$REF.tar.gz" + tar xvfz "$REF.tar.gz" --strip-components=1 + rm -f "$REF.tar.gz" + fi +} + +make() +{ + # +x: add x only if defined + if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; + then + # Not submake and parallel make requested + command make -j "$NJOBS" "$@" + else + command make "$@" + fi +} + +# this installs just the ssreflect library of math-comp +install_ssreflect() +{ + echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + + git_download mathcomp + + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ + make Makefile.coq && \ + make -f Makefile.coq ssreflect/all_ssreflect.vo && \ + make -f Makefile.coq install ) + + 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' + + git_download mathcomp + + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ + make Makefile.coq && \ + make -f Makefile.coq algebra/all_algebra.vo && \ + make -f Makefile.coq install ) + + echo -en 'travis_fold:end:ssralg.install\\r' + +} diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh new file mode 100755 index 00000000..01c35ceb --- /dev/null +++ b/dev/ci/ci-compcert.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download CompCert + +( cd "${CI_BUILD_DIR}/CompCert" && \ + ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh new file mode 100755 index 00000000..2373ea6c --- /dev/null +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coq_dpdgraph + +( cd "${CI_BUILD_DIR}/coq_dpdgraph" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh new file mode 100755 index 00000000..5d881749 --- /dev/null +++ b/dev/ci/ci-coquelicot.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +FORCE_GIT=1 +git_download Coquelicot + +( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh new file mode 100755 index 00000000..7d5d70cf --- /dev/null +++ b/dev/ci/ci-corn.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download Corn + +( cd "${CI_BUILD_DIR}/Corn" && make && make install ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh new file mode 100755 index 00000000..ca759c7b --- /dev/null +++ b/dev/ci/ci-cpdt.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +wget http://adam.chlipala.net/cpdt/cpdt.tgz +tar xvfz cpdt.tgz + +( cd cpdt && make clean && make ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh new file mode 100755 index 00000000..7f4ef77d --- /dev/null +++ b/dev/ci/ci-elpi.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +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-equations.sh b/dev/ci/ci-equations.sh new file mode 100755 index 00000000..998d50fa --- /dev/null +++ b/dev/ci/ci-equations.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download Equations + +( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ + make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh new file mode 100755 index 00000000..5eb167d9 --- /dev/null +++ b/dev/ci/ci-ext-lib.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download ext_lib + +( cd "${CI_BUILD_DIR}/ext_lib" && make && make install) diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh new file mode 100755 index 00000000..cb951630 --- /dev/null +++ b/dev/ci/ci-fcsl-pcm.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +git_download fcsl_pcm + +( cd "${CI_BUILD_DIR}/fcsl_pcm" && make ) diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh new file mode 100755 index 00000000..e0395754 --- /dev/null +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_crypto + +fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" +fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" + +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh new file mode 100755 index 00000000..7e8013be --- /dev/null +++ b/dev/ci/ci-fiat-crypto.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_crypto + +# We need a larger stack size to not overflow ocamlopt+flambda when +# building the executables. +# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 + +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + ulimit -s 32768 && make new-pipeline c-files ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 00000000..ac74ebf6 --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_parsers + +( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh new file mode 100755 index 00000000..e87483df --- /dev/null +++ b/dev/ci/ci-flocq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download Flocq + +( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh new file mode 100755 index 00000000..8be5a06e --- /dev/null +++ b/dev/ci/ci-formal-topology.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download formal_topology + +( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh new file mode 100755 index 00000000..8c573184 --- /dev/null +++ b/dev/ci/ci-geocoq.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssralg + +git_download GeoCoq + +( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh new file mode 100755 index 00000000..9a0726a1 --- /dev/null +++ b/dev/ci/ci-hott.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download HoTT + +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh new file mode 100755 index 00000000..6960a8b9 --- /dev/null +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -0,0 +1,30 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +# Setup lambdaRust first +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/') + +# 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/') + +# Setup std++ +git_download stdpp + +# Build std++ +( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) + +# Build and validate Iris +( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) + +# Build lambdaRust +( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh new file mode 100755 index 00000000..4df22bf2 --- /dev/null +++ b/dev/ci/ci-ltac2.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download ltac2 + +( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh new file mode 100755 index 00000000..ae31a8e7 --- /dev/null +++ b/dev/ci/ci-math-classes.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download math_classes + +( cd "${CI_BUILD_DIR}/math_classes" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh new file mode 100755 index 00000000..74f1a627 --- /dev/null +++ b/dev/ci/ci-math-comp.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download mathcomp + +( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) + +git_download oddorder + +( cd "${CI_BUILD_DIR}/oddorder" && make ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh new file mode 100755 index 00000000..7075d4d7 --- /dev/null +++ b/dev/ci/ci-mtac2.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download unicoq + +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) + +git_download mtac2 + +( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh new file mode 100755 index 00000000..08686d7c --- /dev/null +++ b/dev/ci/ci-quickchick.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +git_download quickchick + +( cd "${CI_BUILD_DIR}/quickchick" && make && make install) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh new file mode 100755 index 00000000..58bbb722 --- /dev/null +++ b/dev/ci/ci-sf.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" || exit 1 +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 vfa && make clean && make ) diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple-io.sh new file mode 100755 index 00000000..ddc1590d --- /dev/null +++ b/dev/ci/ci-simple-io.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +. "${ci_dir}/ci-common.sh" + +git_download simple_io + +( cd "${CI_BUILD_DIR}/simple_io" && make build && make install) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh new file mode 100755 index 00000000..a2f0bea5 --- /dev/null +++ b/dev/ci/ci-tlc.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download tlc + +( cd "${CI_BUILD_DIR}/tlc" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh new file mode 100755 index 00000000..a7644fee --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download UniMath + +( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh new file mode 100755 index 00000000..0fec1920 --- /dev/null +++ b/dev/ci/ci-vst.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download VST + +( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh new file mode 100755 index 00000000..12a70176 --- /dev/null +++ b/dev/ci/ci-wrapper.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash + +# Use this script to preserve the exit code of $CI_SCRIPT when piping +# it to `tee time-of-build.log`. We have a separate script, because +# this only works in bash, which we don't require project-wide. + +set -eo pipefail + +function travis_fold { + if [ -n "${TRAVIS}" ]; + then + echo "travis_fold:$1:$2" + fi +} + +CI_NAME="$1" +CI_SCRIPT="ci-${CI_NAME}.sh" + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +# assume this script is in dev/ci/, cd to the root Coq directory +cd "${DIR}/../.." + +export TIMED=1 +"${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log +travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' +python ./tools/make-one-time-file.py time-of-build.log +travis_fold 'end' 'coq.test.timing' diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile new file mode 100644 index 00000000..da12f122 --- /dev/null +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -0,0 +1,59 @@ +# CACHEKEY: "bionic_coq-v8.8-V2018-09-20" +# ^^ Update when modifying this file. + +FROM ubuntu:bionic +LABEL maintainer="e@x80.org" + +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 \ + # 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 + +RUN pip3 install antlr4-python3-runtime + +# Basic OPAM setup +ENV NJOBS="2" \ + OPAMROOT=/root/.opamcache \ + OPAMROOTISOK="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" + +# 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 + +# base+32bit switch +RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ + opam install -j $NJOBS $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 + +# 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 diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat new file mode 100755 index 00000000..ee1b17b6 --- /dev/null +++ b/dev/ci/gitlab.bat @@ -0,0 +1,131 @@ +@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 diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh new file mode 100644 index 00000000..be0058b6 --- /dev/null +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -0,0 +1,4 @@ +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 diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md new file mode 100644 index 00000000..b8628979 --- /dev/null +++ b/dev/ci/user-overlays/README.md @@ -0,0 +1,31 @@ +# 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). + +An overlay is a file which defines where to look for the patched version so that +testing is possible. It redefines some variables from +[`ci-basic-overlay.sh`](../ci-basic-overlay.sh): +give the name of your branch / commit using a `_CI_REF` variable and the +location of your fork using a `_CI_GITURL` variable. +The `_CI_GITURL` variable should be the URL of the repository without a +trailing `.git`. +If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is +necessary to redefine the `_CI_ARCHIVEURL` variable as well. + +Moreover, the file contains very simple logic to test the pull request number +or branch name and apply it only in this case. + +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: `00669-maximedenes-ssr-merge.sh` containing + +``` +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)) |