diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | dev/ci/README.md | 77 | ||||
| -rw-r--r-- | dev/ci/gitlab.bat | 50 | ||||
| -rwxr-xr-x | dev/tools/check-owners-pr.sh | 32 | ||||
| -rwxr-xr-x | dev/tools/check-owners.sh | 138 | ||||
| -rw-r--r-- | dev/tools/coqdev.el | 12 |
6 files changed, 278 insertions, 35 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f4ec218b6b..3608f7305d 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -970,6 +970,10 @@ function make_lablgtk { # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch log2 make world + + # lablgtk does not escape FINDLIBDIR path, which can contain backslashes + sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make + log2 make install log2 make clean build_post diff --git a/dev/ci/README.md b/dev/ci/README.md index bb13587e94..87f03aa994 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -36,9 +36,8 @@ On the condition that: - 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. -- Your development compiles in less than 35 minutes with just two threads. - If this is not the case, consider adding a "lite" target that compiles just - part of it. +- 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 @@ -54,9 +53,10 @@ Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at set the corresponding variables in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding target to [`Makefile.ci`](/Makefile.ci); add new jobs to -[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that -this new target is run. **Do not hesitate to submit an incomplete pull request -if you need help to finish it.** +[`.gitlab-ci.yml`](/.gitlab-ci.yml), +[`.circleci/config.yml`](/.circleci/config.yml) and +[`.travis.yml`](/.travis.yml) so that this new target is run. **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 @@ -71,24 +71,38 @@ 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. -Currently, we have two CI platforms: +We are currently running tests on the following platforms: -- Travis is the main CI platform. It tests the compilation of Coq, of the +- 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. It also tests the compilation - of Coq on OS X. + compilation of several external developments. + +- Circle CI runs tests that are redundant with GitLab CI and may be removed + eventually. + +- 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](/dev/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 these tests prior to submitting your PR -by having them run of your fork of Coq, on GitHub or GitLab. This can be -especially helpful given that our Travis platform is often overloaded and -therefore there can be a significant delay before these tests are actually -run on your PR. To take advantage of this, simply create a Travis account -and link it to your GitHub account, or activate the pipelines on your GitLab -fork. +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. 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`). @@ -97,36 +111,29 @@ so that it doesn't, or provide a branch fixing these developments (or at least work with the author of the development / other Coq developers to prepare these fixes). Then, add an overlay in [`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there) -in a separate commit in your PR. +as part of your PR. The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are -backward-compatible), drop the overlay commit and merge the PR on Coq then. +backward-compatible), and merge the PR on Coq then. See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. -Travis specific information ---------------------------- - -Travis rebuilds all of Coq's executables and stdlib for each job. Coq -is built with `./configure -local`, then used for the job's test. - - -GitLab specific information ---------------------------- +Advanced GitLab CI information +------------------------------ -GitLab is set up to use the "build artifact" feature to avoid -rebuilding Coq. In one job, Coq is built with `./configure -prefix -install` and `make install` is run, then the `install` directory +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, in two different copies varying in the OCaml - version used to build Coq + 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. +no OCaml warnings build Coq in parallel with other tests. diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat new file mode 100644 index 0000000000..70278e6d09 --- /dev/null +++ b/dev/ci/gitlab.bat @@ -0,0 +1,50 @@ +@ECHO OFF + +REM This script builds and signs the Windows packages on Gitlab + +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 +) + +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 DESTCOQ=C:\coq%ARCH%_inst +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 -make=N ^ + -setup %CI_PROJECT_DIR%\%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 + +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 + ) +) + +GOTO :EOF + +:ErrorExit + ECHO ERROR %0 failed + EXIT /b 1 diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh new file mode 100755 index 0000000000..d2910279b5 --- /dev/null +++ b/dev/tools/check-owners-pr.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env sh + +usage() { + { echo "usage: $0 PR [ARGS]..." + echo "A wrapper around check-owners.sh to check owners for a PR." + echo "Assumes upstream is the canonical Coq repository." + echo "Assumes the PR is against master." + echo + echo " PR: PR number" + echo " ARGS: passed through to check-owners.sh" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi;; + "") + usage + exit 1;; +esac + +PR="$1" +shift + +# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first +git fetch upstream "+refs/pull/$PR/head" master + +head=$(git rev-parse FETCH_HEAD) +base=$(git merge-base upstream/master "$head") + +git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@" diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh new file mode 100755 index 0000000000..1a97508abb --- /dev/null +++ b/dev/tools/check-owners.sh @@ -0,0 +1,138 @@ +#!/usr/bin/env bash + +# Determine CODEOWNERS of the files given in argument +# For a given commit range: +# git diff --name-only -z COMMIT1 COMMIT2 | xargs -0 dev/tools/check-owners.sh [opts] + +# NB: gitignore files will be messed up if you interrupt the script. +# You should be able to just move the .gitignore.bak files back manually. + +usage() { + { echo "usage: $0 [--show-patterns] [--owner OWNER] [FILE]..." + echo " --show-patterns: instead of printing file names print the matching patterns (more compact)" + echo " --owner: show only files/patterns owned by OWNER (use Nobody to see only non-owned files)" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi +esac + +if ! [ -e .github/CODEOWNERS ]; then + >&2 echo "No CODEOWNERS set up or calling from wrong directory." + exit 1 +fi + +files=() +show_patterns=false + +target_owner="" + +while [[ "$#" -gt 0 ]]; do + case "$1" in + "--show-patterns") + show_patterns=true + shift;; + "--owner") + if [[ "$#" = 1 ]]; then + >&2 echo "Missing argument to --owner" + usage + exit 1 + elif [[ "$target_owner" != "" ]]; then + >&2 echo "Only one --owner allowed" + usage + exit 1 + fi + target_owner="$2" + shift 2;; + *) + files+=("$@") + break;; + esac +done + +# CODEOWNERS uses .gitignore patterns so we want to use git to parse it +# The only available tool for that is git check-ignore +# However it provides no way to use alternate .gitignore files +# so we rename them temporarily + +find . -name .gitignore -print0 | while IFS= read -r -d '' f; do + if [ -e "$f.bak" ]; then + >&2 echo "$f.bak exists!" + exit 1 + else + mv "$f" "$f.bak" + fi +done + +# CODEOWNERS is not quite .gitignore patterns: +# after the pattern is the owner (space separated) +# git would interpret that as a big pattern containing spaces +# so we create a valid .gitignore by removing all but the first field + +while read -r pat _; do + printf '%s\n' "$pat" >> .gitignore +done < .github/CODEOWNERS + +# associative array [file => owner] +declare -A owners + +for f in "${files[@]}"; do + data=$(git check-ignore --verbose --no-index "./$f") + code=$? + + if [[ "$code" = 1 ]] || ! [[ "$data" =~ .gitignore:.* ]] ; then + # no match, or match from non tracked gitignore (eg global gitignore) + if [ "$target_owner" != "" ] && [ "$target_owner" != Nobody ] ; then + owner="" + else + owner="Nobody" + pat="$f" # no patterns for unowned files + fi + else + # data looks like [.gitignore:$line:$pattern $file] + # extract the line to look it up in CODEOWNERS + data=${data#'.gitignore:'} + line=${data%%:*} + + # NB: supports multiple owners + # Does not support secondary owners declared in comment + read -r pat fowners < <(sed "${line}q;d" .github/CODEOWNERS) + + owner="" + if [ "$target_owner" != "" ]; then + for o in $fowners; do # do not quote: multiple owners possible + if [ "$o" = "$target_owner" ]; then + owner="$o" + fi + done + else + owner="$fowners" + fi + fi + + if [ "$owner" != "" ]; then + if $show_patterns; then + owners[$pat]="$owner" + else + owners[$f]="$owner" + fi + fi +done + +for f in "${!owners[@]}"; do + printf '%s: %s\n' "$f" "${owners[$f]}" +done | sort -k 2 -k 1 # group by owner + +# restore gitignore files +rm .gitignore +find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do + base=${f%.bak} + if [ -e "$base" ]; then + >&2 echo "$base exists!" + else + mv "$f" "$base" + fi +done diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 62fdaec802..9dd12087a6 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -103,5 +103,17 @@ Note that this function is executed before _Coqproject is read if it exists." 2 (3 . 4) (5 . 6))) (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) +(defvar bug-reference-bug-regexp) +(defvar bug-reference-url-format) +(defun coqdev-setup-bug-reference-mode () + "Setup `bug-reference-bug-regexp' and `bug-reference-url-format' for Coq. + +This does not enable `bug-reference-mode'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local bug-reference-bug-regexp "#\\(?2:[0-9]+\\)") + (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) + (provide 'coqdev) ;;; coqdev ends here |