diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README-developers.md | 10 | ||||
| -rw-r--r-- | dev/ci/appveyor.bat | 84 |
2 files changed, 48 insertions, 46 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index fa8962a06f..6663fbecf8 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -10,12 +10,14 @@ 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 and with warnings as errors; it runs the test-suite and - tests the compilation of several external developments. + tests the compilation of several external developments. 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. - 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. + macOS. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index 85a71baf7f..341b875edc 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -1,42 +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 +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
|