image: "$IMAGE" stages: - docker - build - test # some default values variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] CACHEKEY: "bionic_coq-V2018-05-07-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" # Used to select special compiler switches such as flambda, 32bits, etc... OPAM_VARIANT: "" docker-boot: stage: docker image: docker:stable services: - docker:dind before_script: [] script: - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY" - cd dev/ci/docker/bionic_coq/ - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi - docker build -t "$IMAGE" . - docker push "$IMAGE" except: variables: - $SKIP_DOCKER == "true" before_script: - cat /proc/{cpu,mem}info || true - ls -a # figure out if artifacts are around - printenv -0 | sort -z | tr '\0' '\n' - declare -A switch_table - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_BE" ) - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT" - eval $(opam config env) - opam list - opam config list ################ GITLAB CACHING ###################### # - use artifacts between jobs # ###################################################### # TODO figure out how to build doc for installed Coq .build-template: &build-template stage: build artifacts: name: "$CI_JOB_NAME" paths: - _install_ci - config/Makefile - test-suite/misc/universes/all_stdlib.v expire_in: 1 week script: - set -e - echo 'start:coq.clean' - make clean # ensure that `make clean` works on a fresh clone - echo 'end:coq.clean' - echo 'start:coq.config' - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" - echo 'end:coq.config' - echo 'start:coq.build' - make -j "$NJOBS" byte - make -j "$NJOBS" - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' - echo 'start:coq.install' - make install - make install-byte - cp bin/fake_ide _install_ci/bin/ - echo 'end:coq.install' - set +e .warnings-template: &warnings-template # keep warnings in test stage so we can test things even when warnings occur stage: test script: - set -e - echo 'start:coq.clean' - make clean # ensure that `make clean` works on a fresh clone - echo 'end:coq.clean' - echo 'start:coq.config' - ./configure -local ${COQ_EXTRA_CONF} - echo 'end:coq.config' - echo 'start:coq.build' - make -j "$NJOBS" coqocaml - echo 'end:coq:build' - set +e variables: &warnings-variables COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that # purpose, we add a spurious dependency `not-a-real-job` that must be # overridden otherwise the CI will fail. # set dependencies when using .test-suite-template: &test-suite-template stage: test dependencies: - not-a-real-job script: - cd test-suite - make clean # careful with the ending / - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure paths: - test-suite/logs # set dependencies when using .validate-template: &validate-template stage: test dependencies: - not-a-real-job script: - cd _install_ci - 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/ .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:base variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" .ci-template-flambda: &ci-template-flambda <<: *ci-template dependencies: - build:edge+flambda variables: <<: *ci-template-vars OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" .windows-template: &windows-template stage: test artifacts: name: "%CI_JOB_NAME%" paths: - dev\nsis\*.exe - coq-opensource-archive-windows-*.zip expire_in: 1 week dependencies: [] tags: - windows before_script: [] script: - call dev/ci/gitlab.bat only: variables: - $WINDOWS == "enabled" build:base: <<: *build-template variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" # no coqide for 32bit: libgtk installation problems build:base+32bit: <<: *build-template variables: OPAM_VARIANT: "+32bit" COQ_EXTRA_CONF: "-native-compiler yes" build:edge: <<: *build-template variables: OPAM_SWITCH: edge COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" build:edge+flambda: <<: *build-template variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" windows64: <<: *windows-template variables: ARCH: "64" windows32: <<: *windows-template variables: ARCH: "32" warnings:base: <<: *warnings-template # warnings:32bit: # <<: *warnings-template # variables: # <<: *warnings-variables warnings:edge: <<: *warnings-template variables: <<: *warnings-variables OPAM_SWITCH: edge test-suite:base: <<: *test-suite-template dependencies: - build:base test-suite:base+32bit: <<: *test-suite-template dependencies: - build:base+32bit variables: OPAM_VARIANT: "+32bit" test-suite:edge: <<: *test-suite-template dependencies: - build:edge variables: OPAM_SWITCH: edge test-suite:edge+flambda: <<: *test-suite-template dependencies: - build:edge+flambda variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" validate:base: <<: *validate-template dependencies: - build:base validate:base+32bit: <<: *validate-template dependencies: - build:base+32bit variables: OPAM_VARIANT: "+32bit" validate:edge: <<: *validate-template dependencies: - build:edge variables: OPAM_SWITCH: edge validate:edge+flambda: <<: *validate-template dependencies: - build:edge+flambda variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" ci-bignums: <<: *ci-template ci-color: <<: *ci-template-flambda ci-compcert: <<: *ci-template-flambda ci-coq-dpdgraph: <<: *ci-template ci-coquelicot: <<: *ci-template ci-cross-crypto: <<: *ci-template ci-elpi: <<: *ci-template ci-equations: <<: *ci-template ci-fcsl-pcm: <<: *ci-template ci-fiat-crypto: <<: *ci-template-flambda ci-fiat-parsers: <<: *ci-template ci-flocq: <<: *ci-template ci-formal-topology: <<: *ci-template-flambda ci-geocoq: <<: *ci-template-flambda ci-hott: <<: *ci-template ci-iris-lambda-rust: <<: *ci-template-flambda ci-ltac2: <<: *ci-template ci-math-comp: <<: *ci-template-flambda ci-mtac2: <<: *ci-template ci-pidetop: <<: *ci-template ci-sf: <<: *ci-template ci-unimath: <<: *ci-template-flambda ci-vst: <<: *ci-template-flambda