diff options
| -rw-r--r-- | .gitlab-ci.yml | 312 | ||||
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | Makefile.doc | 4 | ||||
| -rw-r--r-- | README.ci | 39 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 13 | ||||
| -rw-r--r-- | test-suite/Makefile | 9 | ||||
| -rw-r--r-- | test-suite/coq-makefile/template/init.sh | 2 |
7 files changed, 368 insertions, 16 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml new file mode 100644 index 000000000..9ba39abdb --- /dev/null +++ b/.gitlab-ci.yml @@ -0,0 +1,312 @@ +image: ocaml/opam:ubuntu + +# this doesn't seem to work +cache: + paths: + - .opamcache + +stages: + - build + - test + +variables: + # some default values + NJOBS: "2" + COMPILER: "system" + CAMLP5_VER: "6.14" + + # some useful values + COMPILER_32BIT: "4.02.3+32bit" + + COMPILER_BLEEDING_EDGE: "4.04.1" + CAMLP5_VER_BLEEDING_EDGE: "6.17" + + COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" + #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" + COQIDE_OPAM: "lablgtk-extras" + COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa" + COQDOC_OPAM: "hevea" + + +before_script: + - ls # figure out if artifacts are around + - printenv +# - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi + - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -qq && sudo apt-get install -y -qq ${EXTRA_PACKAGES}; fi + + # setup cache + - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi + - ln -s $(readlink -f .opamcache) ~/.opam + + - opam switch ${COMPILER} + - eval $(opam config env) + - opam config list + - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} + - rm -rf ~/.opam/log/ + - opam list + +# TODO figure out how to build doc for installed coq +.build-template: &build-template + stage: build + artifacts: + name: "$CI_JOB_NAME" + paths: + - install + - config/Makefile + expire_in: 1 week + script: + - set -e + + - echo 'start:coq.config' + - ./configure -prefix "$(pwd)/install" ${EXTRA_CONF} + - echo 'end:coq.config' + + - echo 'start:coq.build' + - make -j ${NJOBS} + - echo 'end:coq:build' + + - echo 'start:coq.install' + - make install + - cp bin/fake_ide install/bin/ + - echo 'end:coq.install' + + - set +e + variables: &build-variables + EXTRA_CONF: "-native-compiler yes -coqide opt" + EXTRA_PACKAGES: "$COQIDE_PACKAGES" + EXTRA_OPAM: "$COQIDE_OPAM" + +.warnings-template: &warnings-template + # keep warnings in test stage so we can test things even when warnings occur + stage: test + dependencies: [] + script: + - set -e + + - echo 'start:coq.config' + - ./configure -local ${EXTRA_CONF} + - echo 'end:coq.config' + + - echo 'start:coq.build' + - make -j ${NJOBS} coqocaml + - echo 'end:coq:build' + + - set +e + variables: &warnings-variables + EXTRA_CONF: "-native-compiler yes -coqide opt" + EXTRA_PACKAGES: "$COQIDE_PACKAGES" + EXTRA_OPAM: "$COQIDE_OPAM" + +.test-suite-template: &test-suite-template + stage: test + script: + - set -e + - cd test-suite + - make clean + # careful with the ending / + - make -j ${NJOBS} BIN=$(readlink -f ../install/bin)/ LIB=$(readlink -f ../install/lib/coq)/ all + - cat summary.log + - set +e + +.validate-template: &validate-template + stage: test + script: + - cd install + - find lib/coq/ -name '*.vo' -print0 > vofiles + - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done + - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/ + +.documentation-template: &documentation-template + stage: test + script: + - ./configure -prefix "$(pwd)/install" ${EXTRA_CONF} + - cp install/lib/coq/tools/coqdoc/coqdoc.sty . + + - INSTALLDIR=$(readlink -f install) + - LIB="$INSTALLDIR/lib/coq" + # WTF using a newline makes make sigsev + # see https://gitlab.com/SkySkimmer/coq/builds/17313312 + - DOCVFILES=$(find "$LIB/" -name '*.v' -printf "%p ") + - DOCLIGHTDIRS="$LIB/theories/Init/ $LIB/theories/Logic/ $LIB/theories/Unicode/ $LIB/theories/Arith/" + - DOCLIGHTVOFILES=$(find $DOCLIGHTDIRS -name '*.vo' -printf "%p ") + + - make doc QUICK=true COQDOC_NOBOOT=true COQTEX="$INSTALLDIR/bin/coq-tex" COQDOC="$INSTALLDIR/bin/coqdoc" VFILES="$DOCVFILES" THEORIESLIGHTVO="$DOCLIGHTVOFILES" + + - make install-doc + artifacts: + name: "$CI_JOB_NAME" + paths: + - install/share/doc + expire_in: 1 week + +.ci-template: &ci-template + stage: test + script: + - set -e + - echo 'start:coq.test' + - make -f Makefile.ci -j ${NJOBS} ${TEST_TARGET} + - echo 'end:coq.test' + - set +e + dependencies: + - build + variables: &ci-template-vars + TEST_TARGET: "$CI_JOB_NAME" + +build: + <<: *build-template + +# no coqide for 32bit: libgtk installation problems +build:32bit: + <<: *build-template + variables: + EXTRA_CONF: "-native-compiler yes" + EXTRA_PACKAGES: "gcc-multilib" + COMPILER: "$COMPILER_32BIT" + +build:bleeding-edge: + <<: *build-template + variables: + <<: *build-variables + COMPILER: "$COMPILER_BLEEDING_EDGE" + CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + +warnings: + <<: *warnings-template + +# warnings:32bit: +# <<: *warnings-template +# variables: +# <<: *warnings-variables +# EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT" +# COMPILER: "$COMPILER_32BIT" + +warnings:bleeding-edge: + <<: *warnings-template + variables: + <<: *warnings-variables + COMPILER: "$COMPILER_BLEEDING_EDGE" + CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + +test-suite: + <<: *test-suite-template + dependencies: + - build + +test-suite:32bit: + <<: *test-suite-template + dependencies: + - build:32bit + variables: + COMPILER: "$COMPILER_32BIT" + EXTRA_PACKAGES: "gcc-multilib" + +test-suite:bleeding-edge: + <<: *test-suite-template + dependencies: + - build:bleeding-edge + variables: + COMPILER: "$COMPILER_BLEEDING_EDGE" + CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + +documentation: + <<: *documentation-template + dependencies: + - build + variables: + EXTRA_PACKAGES: "$COQDOC_PACKAGES" + EXTRA_OPAM: "$COQDOC_OPAM" + +documentation:bleeding-edge: + <<: *documentation-template + dependencies: + - build:bleeding-edge + variables: + COMPILER: "$COMPILER_BLEEDING_EDGE" + CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + EXTRA_PACKAGES: "$COQDOC_PACKAGES" + EXTRA_OPAM: "$COQDOC_OPAM" + +validate: + <<: *validate-template + dependencies: + - build + +validate:32bit: + <<: *validate-template + dependencies: + - build:32bit + variables: + COMPILER: "$COMPILER_32BIT" + EXTRA_PACKAGES: "gcc-multilib" + +ci-bedrock-src: + <<: *ci-template + +ci-bedrock-facade: + <<: *ci-template + +ci-color: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_PACKAGES: "subversion" + +ci-compcert: + <<: *ci-template + +ci-coquelicot: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_PACKAGES: "autoconf" + +ci-geocoq: + <<: *ci-template + allow_failure: true + +# ci-fiat-crypto: +# <<: *ci-template +# # out of memory error +# allow_failure: true + +ci-fiat-parsers: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_PACKAGES: "python" + +ci-flocq: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_PACKAGES: "autoconf" + +ci-formal-topology: + <<: *ci-template + +ci-hott: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_PACKAGES: "autoconf" + +ci-iris-coq: + <<: *ci-template + +ci-math-classes: + <<: *ci-template + +ci-math-comp: + <<: *ci-template + +ci-sf: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_PACKAGES: "wget" + +ci-unimath: + <<: *ci-template + +ci-vst: + <<: *ci-template @@ -53,8 +53,9 @@ FIND_VCS_CLAUSE:='(' \ -name 'debian' -o \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ - -name '_build_ci' \ - -name 'coq-makefile' \ + -name '_build_ci' -o \ + -name 'coq-makefile' -o \ + -name '.opamcache' \ ')' -prune -o define find diff --git a/Makefile.doc b/Makefile.doc index 39c3255f5..c31d81c8b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -38,7 +38,11 @@ HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple export TEXINPUTS:=$(HEVEALIB): +ifdef COQDOC_NOBOOT +COQTEXOPTS:=-n 72 -sl -small +else COQTEXOPTS:=-boot -n 72 -sl -small +endif DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex @@ -6,15 +6,16 @@ Introduction The Coq Travis CI infrastructure is meant to provide lightweight automatics testing of pull requests. +If you are on GitLab, their integrated CI is also set up. More comprehensive testing is the responsability of Coq's [Jenkins CI server](https://ci.inria.fr/coq/) see, [XXX: add document] for instructions on how to add your development to Jenkins. -How to submit your development for Coq Travis CI -================================================ +How to submit your development for Coq CI +========================================= -Travis CI provides a convenient way to perform testing of Coq changes +CI provides a convenient way to perform testing of Coq changes versus a set of curated libraries. Are you an author of a Coq library who would be interested in having @@ -25,7 +26,7 @@ is easy, all that you need to do is: 1.- Put you development in a public repository tracking coq trunk. 2.- Make sure that your development builds in less than 35 minutes. -3.- Submit a PR adding you development. +3.- Submit a PR adding your development. 4.- ? 5.- Profit! Your library is now part of Coq's continous integration! @@ -39,8 +40,8 @@ have. Maintaining your contribution manually [current method] ====================================== -To add your contribution to the Coq Travis CI set, add a script for -building your library to `dev/ci/`, update `.travis.yml` and +To add your contribution to the Coq CI set, add a script for building +your library to `dev/ci/`, update `.travis.yml`, `.gitlab-ci.yml` and `Makefile.ci`. Then, submit a PR. Maintaining your contribution as an OPAM package [work in progress] [to be implemented] @@ -75,3 +76,29 @@ The `.overlay` file will contain a set of variables that will be used to do the corresponding `opam pin` or to overload the corresponding git repositories, etc... +Since pull requests only happen on GitHub there is no need to test the +corresponding GitLab CI variables. + +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 +=========================== + +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 +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 + +As an exception to the above, jobs testing that compilation triggers +no Ocaml warnings build Coq in parallel with other tests. diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2711b7eca..f1e1515d4 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,11 +2,18 @@ set -xe +if [ -n "${GITLAB_CI}" ]; +then + export COQBIN=`pwd`/install/bin +else + export COQBIN=`pwd`/bin +fi +export PATH="$COQBIN:$PATH" + # Coq's tools need an ending slash :S, we should fix them. -export COQBIN=`pwd`/bin/ -export PATH=`pwd`/bin:$PATH +export COQBIN="$COQBIN/" -ls `pwd`/bin +ls "$COQBIN" # Where we clone and build external developments CI_BUILD_DIR=`pwd`/_build_ci diff --git a/test-suite/Makefile b/test-suite/Makefile index c2d6e540c..570bf3222 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -27,10 +27,10 @@ # Default value when called from a freshly compiled Coq, but can be # easily overridden -BIN := ../bin/ +BIN := $(shell cd ..; readlink -f bin)/ LIB := $(shell cd ..; pwd) -coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqtopbyte := $(BIN)coqtop.byte @@ -440,7 +440,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -488,9 +488,10 @@ coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) coq-makefile/%.log : coq-makefile/%/run.sh @echo "TEST coq-makefile/$*" $(HIDE)(\ + export COQBIN=$(BIN);\ cd coq-makefile/$* && \ ./run.sh 2>&1; \ - if [ $$? = 0 ]; then \ + if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ else \ diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index bfd2c1b95..c952d41a3 100644 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -1,5 +1,5 @@ -export PATH=../../../bin/:$PATH +export PATH=$COQBIN:$PATH rm -rf theories src Makefile Makefile.conf tmp git clean -dfx || true |