diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/README.md | 27 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh | 6 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 5 |
4 files changed, 38 insertions, 4 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 87f03aa994..dee3d2aff7 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -96,7 +96,8 @@ PR by running GitLab CI on your private branches. To do so follow these steps: 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. You are encouraged to go to the CI / CD general settings and increase the +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 @@ -137,3 +138,27 @@ Currently, available artifacts are: 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. + +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. diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 189734a0bc..2a14ed352a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ]; then 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 diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 0000000000..517088a247 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 84ff94c66a..a466124c1c 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -109,9 +109,8 @@ There are two cases to consider: The merge script passes option `-S` to `git merge` to ensure merge commits are signed. Consequently, it depends on the GnuPG command utility being -installed and a GPG key being available. Here is a short tutorial to -creating your own GPG key: -<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. The script depends on a few other utilities. If you are a Nix user, the simplest way of getting them is to run `nix-shell` first. |