Spracherkennung für: .yml vermutete Sprache: Latech {Latech[49] HTML[204] CS[237]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
image: "$IMAGE"
stages:
- docker
- build
- test
- deploy
# some default values
variables:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
CACHEKEY: "bionic_coq-v8.10-V2019-06-24-V1"
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: ""
GIT_DEPTH: "10"
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"
tags:
- docker
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"]="ocaml-base-compiler.$COMPILER" ["edge"]="$COMPILER_EDGE" )
- opam switch set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
- eval $(opam env)
- opam list
- opam config list
################ GITLAB CACHING ######################
# - use artifacts between jobs #
######################################################
# TODO figure out how to build doc for installed Coq
.build-template:
stage: build
artifacts:
name: "$CI_JOB_NAME"
paths:
- _install_ci
- config/Makefile
- config/coq_config.py
- 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 -warn-error yes -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" world $EXTRA_TARGET
- make test-suite/misc/universes/all_stdlib.v
- echo 'end:coq:build'
- echo 'start:coq.install'
- make install install-byte $EXTRA_INSTALL
- make install-byte
- cp bin/fake_ide _install_ci/bin/
- echo 'end:coq.install'
- set +e
# Template for building Coq + stdlib, typical use: overload the switch
.dune-template:
stage: build
dependencies: []
script:
- set -e
- make -f Makefile.dune world
- set +e
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
artifacts:
name: "$CI_JOB_NAME"
paths:
- _build/
expire_in: 1 week
.dune-ci-template:
stage: test
dependencies:
- build:edge+flambda:dune:dev
script:
- set -e
- echo 'start:coq.test'
- make -f Makefile.dune "$DUNE_TARGET"
- echo 'end:coq.test'
- set +e
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
artifacts:
name: "$CI_JOB_NAME"
expire_in: 1 month
# 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.
.doc-template:
stage: test
dependencies:
- not-a-real-job
script:
- SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/"'
- make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
- make install-doc-sphinx
artifacts:
name: "$CI_JOB_NAME"
paths:
- _install_ci/share/doc/coq/
# set dependencies when using
.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)/
- export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
- make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
paths:
- test-suite/logs
variables:
timeout: ""
# set dependencies when using
.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 -silent -o -m -coqlib lib/coq/
.ci-template:
stage: test
script:
- set -e
- echo 'start:coq.test'
- make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
- echo 'end:coq.test'
- set +e
dependencies:
- build:base
.ci-template-flambda:
extends: .ci-template
dependencies:
- build:edge+flambda
variables:
OPAM_SWITCH: "edge"
OPAM_VARIANT: "+flambda"
.windows-template:
stage: test
artifacts:
name: "%CI_JOB_NAME%"
paths:
- artifacts
when: always
expire_in: 1 week
dependencies: []
tags:
- windows
before_script: []
script:
- call dev/ci/gitlab.bat
only:
variables:
- $WINDOWS =~ /enabled/
.deploy-template:
stage: deploy
before_script:
- which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
- eval $(ssh-agent -s)
- mkdir -p ~/.ssh
- chmod 700 ~/.ssh
- ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts
- git config --global user.name "coqbot"
- git config --global user.email "[email protected]"
build:base:
extends: .build-template
variables:
COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
# coqdoc for stdlib, until we know how to build it from installed Coq
EXTRA_TARGET: "stdlib"
EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable"
# no coqide for 32bit: libgtk installation problems
build:base+32bit:
extends: .build-template
variables:
OPAM_VARIANT: "+32bit"
COQ_EXTRA_CONF: "-native-compiler yes"
build:edge+flambda:
extends: .build-template
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts "
COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"
build:edge+flambda:dune:dev:
extends: .dune-template
build:base+async:
extends: .build-template
stage: test
variables:
COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
COQUSERFLAGS: "-async-proofs on"
timeout: 100m
allow_failure: true # See https://github.com/coq/coq/issues/9658
only:
variables:
- $UNRELIABLE =~ /enabled/
build:quick:
extends: .build-template
variables:
COQ_EXTRA_CONF: "-native-compiler no"
QUICK: "1"
timeout: 100m
allow_failure: true # See https://github.com/coq/coq/issues/9637
only:
variables:
- $UNRELIABLE =~ /enabled/
windows64:
extends: .windows-template
variables:
ARCH: "64"
windows32:
extends: .windows-template
variables:
ARCH: "32"
lint:
image: docker:git
stage: test
script:
- apk add bash
- dev/lint-repository.sh
dependencies: []
before_script: []
variables:
# we need an unknown amount of history for per-commit linting
GIT_DEPTH: ""
pkg:opam:
stage: test
# OPAM will build out-of-tree so no point in importing artifacts
dependencies: []
script:
- set -e
- opam pin add --kind=path coq.$COQ_VERSION .
- opam pin add --kind=path coqide-server.$COQ_VERSION .
- opam pin add --kind=path coqide.$COQ_VERSION .
- set +e
variables:
COQ_VERSION: "8.10"
OPAM_SWITCH: "edge"
OPAM_VARIANT: "+flambda"
.nix-template:
image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
stage: test
variables:
# By default we use coq.cachix.org as an extra substituter but this can be overridden
EXTRA_SUBSTITUTERS: https://coq.cachix.org
EXTRA_PUBLIC_KEYS: coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI=
# The following variables should not be overridden
GIT_STRATEGY: none
NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
dependencies: [] # We don't need to download build artifacts
before_script: [] # We don't want to use the shared 'before_script'
script:
- cat /proc/{cpu,mem}info || true
# Use current worktree as tmpdir to allow exporting artifacts in case of failure
- export TMPDIR=$PWD
# We build an expression rather than a direct URL to not be dependent on
# the URL location; we are forced to put the public key of cache.nixos.org
# because there is no --extra-trusted-public-key option.
- nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
paths:
- nix-build-coq.drv-0/*/test-suite/logs
pkg:nix:deploy:
extends: .nix-template
environment:
name: cachix
url: https://coq.cachix.org
before_script:
# Install Cachix as documented at https://github.com/cachix/cachix
- nix-env -iA cachix --prebuilt-only -f https://cachix.org/api/v1/install
only:
- master
- /^v.*\..*$/
pkg:nix:deploy:channel:
extends: .deploy-template
environment:
name: cachix
url: https://coq.cachix.org
only:
refs: # Repeat conditions from pkg:nix:deploy
- master
- /^v.*\..*$/
variables:
- $CACHIX_DEPLOYMENT_KEY
dependencies:
- pkg:nix:deploy
script:
- echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
- git fetch --unshallow
- git branch -v
- git push [email protected]:coq/coq-on-cachix "${CI_COMMIT_SHA}":"${CI_COMMIT_REF_NAME}"
pkg:nix:
extends: .nix-template
except:
- master
- /^v.*\..*$/
doc:refman:
extends: .doc-template
dependencies:
- build:base
doc:refman:dune:
extends: .dune-ci-template
variables:
DUNE_TARGET: refman-html
artifacts:
paths:
- _build/default/doc/sphinx_build/html
doc:stdlib:dune:
extends: .dune-ci-template
variables:
DUNE_TARGET: stdlib-html
artifacts:
paths:
- _build/default/doc/stdlib/html
doc:refman:deploy:
extends: .deploy-template
environment:
name: deployment
url: https://coq.github.io/
only:
variables:
- $DOCUMENTATION_DEPLOY_KEY
dependencies:
- doc:ml-api:odoc
- doc:refman:dune
- doc:stdlib:dune
script:
- echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
- git clone [email protected]:coq/doc.git _deploy
- rm -rf _deploy/$CI_COMMIT_REF_NAME/api
- rm -rf _deploy/$CI_COMMIT_REF_NAME/refman
- rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib
- mkdir -p _deploy/$CI_COMMIT_REF_NAME
- cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api
- cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman
- cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib
- cd _deploy/$CI_COMMIT_REF_NAME/
- git add api refman stdlib
- git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
- git push # TODO: rebase and retry on failure
doc:ml-api:odoc:
extends: .dune-ci-template
variables:
DUNE_TARGET: apidoc
artifacts:
paths:
- _build/default/_doc/
test-suite:base:
extends: .test-suite-template
dependencies:
- build:base
test-suite:base+32bit:
extends: .test-suite-template
dependencies:
- build:base+32bit
variables:
OPAM_VARIANT: "+32bit"
test-suite:edge+flambda:
extends: .test-suite-template
dependencies:
- build:edge+flambda
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
test-suite:egde:dune:dev:
stage: test
dependencies:
- build:edge+flambda:dune:dev
script: make -f Makefile.dune test-suite
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
paths:
- _build/default/test-suite/logs
test-suite:edge+trunk+make:
stage: test
dependencies: []
script:
- opam switch create 4.09.0 --empty
- eval $(opam env)
- opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
- opam update
- opam install ocaml-variants=4.09.0+trunk
- opam pin add -n ocamlfind --dev
- opam install num
- eval $(opam env)
# We avoid problems with warnings:
- ./configure -profile devel -warn-error no
- make -j "$NJOBS" world
- make -j "$NJOBS" test-suite UNIT_TESTS=
variables:
OPAM_SWITCH: base
artifacts:
name: "$CI_JOB_NAME.logs"
when: always
paths:
- test-suite/logs
expire_in: 1 week
allow_failure: true
test-suite:edge+trunk+dune:
stage: test
dependencies: []
script:
- opam switch create 4.09.0 --empty
- eval $(opam env)
- opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
- opam update
- opam install ocaml-variants=4.09.0+trunk
- opam pin add -n ocamlfind --dev
- opam pin add dune --dev # ounit lablgtk conf-gtksourceview
- opam install dune num
- eval $(opam env)
# We use the release profile to avoid problems with warnings
- make -f Makefile.dune trunk
- export COQ_UNIT_TEST=noop
- dune runtest --profile=ocaml409
variables:
OPAM_SWITCH: base
artifacts:
name: "$CI_JOB_NAME.logs"
when: always
paths:
- _build/log
- _build/default/test-suite/logs
expire_in: 1 week
allow_failure: true
test-suite:base+async:
extends: .test-suite-template
dependencies:
- build:base
variables:
COQFLAGS: "-async-proofs on -async-proofs-cache force"
timeout: 100m
allow_failure: true
only:
variables:
- $UNRELIABLE =~ /enabled/
validate:base:
extends: .validate-template
dependencies:
- build:base
validate:base+32bit:
extends: .validate-template
dependencies:
- build:base+32bit
variables:
OPAM_VARIANT: "+32bit"
validate:edge+flambda:
extends: .validate-template
dependencies:
- build:edge+flambda
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
validate:quick:
extends: .validate-template
dependencies:
- build:quick
only:
variables:
- $UNRELIABLE =~ /enabled/
# Libraries are by convention the projects that depend on Coq
# but not on its ML API
library:ci-argosy:
extends: .ci-template
library:ci-bedrock2:
extends: .ci-template
library:ci-color:
extends: .ci-template-flambda
library:ci-compcert:
extends: .ci-template-flambda
library:ci-coquelicot:
extends: .ci-template
library:ci-cross-crypto:
extends: .ci-template
library:ci-fcsl-pcm:
extends: .ci-template
library:ci-fiat-crypto:
extends: .ci-template-flambda
library:ci-fiat-crypto-legacy:
extends: .ci-template-flambda
library:ci-flocq:
extends: .ci-template
library:ci-corn:
extends: .ci-template-flambda
library:ci-geocoq:
extends: .ci-template-flambda
library:ci-hott:
extends: .ci-template
library:ci-iris-lambda-rust:
extends: .ci-template-flambda
library:ci-math-comp:
extends: .ci-template-flambda
library:ci-sf:
extends: .ci-template
library:ci-stdlib2:
extends: .ci-template-flambda
library:ci-unimath:
extends: .ci-template-flambda
library:ci-verdi-raft:
extends: .ci-template-flambda
library:ci-vst:
extends: .ci-template-flambda
# Plugins are by definition the projects that depend on Coq's ML API
plugin:ci-aac_tactics:
extends: .ci-template
plugin:ci-bignums:
extends: .ci-template
plugin:ci-coq_dpdgraph:
extends: .ci-template
plugin:ci-coqhammer:
extends: .ci-template
plugin:ci-elpi:
extends: .ci-template
plugin:ci-equations:
extends: .ci-template
plugin:ci-fiat_parsers:
extends: .ci-template
plugin:ci-ltac2:
extends: .ci-template
plugin:ci-mtac2:
extends: .ci-template
plugin:ci-paramcoq:
extends: .ci-template
plugin:plugin-tutorial:
stage: test
dependencies: []
script:
- ./configure -local -warn-error yes
- make -j "$NJOBS" plugin-tutorial
plugin:ci-quickchick:
extends: .ci-template-flambda
plugin:ci-relation_algebra:
extends: .ci-template
[ Dauer der Verarbeitung: 0.93 Sekunden
]
