|
|
|
|
Quelle .gitlab-ci.yml
Sprache: unbekannt
|
|
image: $BASE_IMAGE
include:
- local: '/dev/ci/gitlab-modes/protected-mode.yml'
rules:
- if: $CI_COMMIT_BRANCH == "master"
- if: $CI_COMMIT_BRANCH =~ /^v.*\..*$/
- local: "/dev/ci/gitlab-modes/normal-mode.yml"
rules:
- if: $CI_COMMIT_BRANCH != "master" && $CI_COMMIT_BRANCH !~ /^v.*\..*$/
- local: "/dev/ci/gitlab-modes/tagged-runners.yml"
rules:
- if: $TAGGED_RUNNERS
- local: "/dev/ci/gitlab-modes/untagged-runners.yml"
rules:
- if: $TAGGED_RUNNERS == null
- local: '/dev/bench/gitlab-bench.yml'
stages:
- docker
- build-0
- build-1
- build-2
- build-3+
- deploy
- stats
# We set "needs" to contain all transitive dependencies. We include the
# transitive dependencies as otherwise we don't get their artifacts
# (eg if color had just needs: bignums it wouldn't get the artifact containing coq)
# some default values
variables:
# Format: image_name-V$DATE-$hash
# $DATE is so we can tell what's what in the image list
# The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
# echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
# echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
BASE_CACHEKEY: "old_ubuntu_lts-v9.1-V2025-04-29-b90c41d539"
EDGE_CACHEKEY: "edge_ubuntu-v9.1-V2025-04-07-dee2054641"
BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
# Used to select special compiler switches such as flambda, 32bits, etc...
OPAM_VARIANT: ""
GIT_DEPTH: "10"
before_script:
- dev/ci/gitlab-section.sh start before_script before_script
- cat /proc/{cpu,mem}info || true
- ulimit -s
- ls -a # figure out if artifacts are around
- printenv -0 | sort -z | tr '\0' '\n'
- opam switch set -y "${COMPILER}${OPAM_VARIANT}"
- eval $(opam env)
- opam list
- opam config list
- dune printenv --root .
- dev/tools/check-cachekey.sh
- dev/tools/list-potential-artifacts.sh > downloaded_artifacts.txt
- if [ -d saved_build_ci ]; then mv saved_build_ci _build_ci; fi
- dev/ci/gitlab-section.sh end before_script
# Regular "release" build of Rocq, with final installed layout
.build-template:
stage: build-0
interruptible: true
extends: .auto-use-tags
variables:
ROCQIDE: "opt"
artifacts:
name: "$CI_JOB_NAME"
paths:
- _install_ci
# All those are for the test-suite jobs, to be discarded soon
- config/Makefile
- config/coq_config.py
- config/coq_config.ml
- config/coq_byte_config.ml
- config/dune.c_flags
expire_in: 1 week
script:
- cp dev/ci/dune-workspace.ci dune-workspace
- PKGS=rocq-runtime,coq-core,rocq-core,coqide-server,rocq-devtools
- if [ "$ROCQIDE" != "no" ]; then PKGS=${PKGS},rocqide; fi
- dev/ci/gitlab-section.sh start coq.clean coq.clean
- make clean # ensure that `make clean` works on a fresh clone
- dev/ci/gitlab-section.sh end coq.clean
- dev/ci/gitlab-section.sh start coq.config coq.config
- ./configure -relocatable $COQ_EXTRA_CONF
- dev/ci/gitlab-section.sh end coq.config
- dev/ci/gitlab-section.sh start coq.build coq.build
- make dunestrap
- dune build -p $PKGS
- dev/ci/gitlab-section.sh end coq.build
- dev/ci/gitlab-section.sh start coq.install coq.install
- dune install --prefix="$(pwd)/_install_ci" $(sed -e 's/,/ /g' <<< ${PKGS})
- dev/ci/gitlab-section.sh end coq.install
# Developer build, with build layout. Faster and useful for those
# jobs needing _build
.build-template:base:dev:
stage: build-0
interruptible: true
extends: .auto-use-tags
script:
- cp dev/ci/dune-workspace.ci dune-workspace
- make $DUNE_TARGET
- tar cfj _build.tar.bz2 _build
variables:
DUNE_TARGET: "world rocqide"
artifacts:
name: "$CI_JOB_NAME"
when: always
paths:
- _build/log
- _build.tar.bz2
- theories/Corelib/dune
- theories/Ltac2/dune
expire_in: 1 day
.doc-template:
stage: build-1
interruptible: true
extends: .auto-use-tags
needs:
- build:base:dev
script:
- ulimit -S -s 16384
- tar xfj _build.tar.bz2
- make "$DUNE_TARGET"
artifacts:
when: always
name: "$CI_JOB_NAME"
expire_in: 2 months
# The used Rocq must be set explicitly for each job with "needs:".
# We add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail (to help debugging missing needs).
# set "needs" when using
.test-suite-template:
stage: build-1
interruptible: true
extends: .auto-use-tags
needs:
- not-a-real-job
script:
- cd test-suite
- make clean
- export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
- COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" TIMED=1 all ROCQ_EXE=$(pwd)/../_install_ci/bin/rocq
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
paths:
- test-suite/logs
expire_in: 1 week
# set "needs" when using
.validate-template:
stage: build-2
interruptible: true
extends: .auto-use-tags
needs:
- not-a-real-job
script:
- for target in $CI_TARGETS; do dev/ci/ci-wrapper.sh "$target"; done
- cd _install_ci
- find lib/coq/ -name '*.vo' -fprint0 vofiles
- xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
- tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
- "[ ! -f coqchk.failed ]" # needs quoting for yml syntax reasons
artifacts:
name: "$CI_JOB_NAME.logs"
when: always
paths:
- coqchk.log
expire_in: 1 week
# This template defaults to "needs: build:base"
# Remember to include it as a transitive dependency if you want additional "needs:"
.ci-template:
stage: build-1
interruptible: true
extends: .auto-use-tags
script:
- ulimit -S -s 16384 # For flambda + native
# set CI_TARGETS from job name if not already provided, then print
- echo CI_TARGETS = ${CI_TARGETS:=${CI_JOB_NAME#*:ci-}}
- for target in $CI_TARGETS; do dev/ci/ci-wrapper.sh "$target"; done
- touch ci-success
after_script:
- if { [ "$SAVE_BUILD_CI" ] || ! [ -e ci-success ]; } && [ -d _build_ci ]; then mv _build_ci saved_build_ci; fi
- dev/tools/list-potential-artifacts.sh > available_artifacts.txt
- dev/tools/cleanup-artifacts.sh downloaded_artifacts.txt available_artifacts.txt
artifacts:
name: "$CI_JOB_NAME"
paths:
- _install_ci
- saved_build_ci
exclude: # reduce artifact size
- saved_build_ci/**/.git # exclude .git directory itself as well
- saved_build_ci/**/.git/**/*
when: always
expire_in: 1 week
needs:
- build:base
only: &full-ci
variables:
- $FULL_CI == "true"
.ci-template-flambda:
extends: .ci-template
image: $EDGE_IMAGE
needs:
- build:edge+flambda
variables:
OPAM_VARIANT: "+flambda"
.deploy-template:
stage: deploy
extends: .auto-use-tags
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 "coqbot@users.noreply.github.com"
.pkg:opam-template:
stage: build-0
image: $EDGE_IMAGE
interruptible: true
extends: .auto-use-tags
# OPAM will build out-of-tree so no point in importing artifacts
script:
- if [ "$ROCQ_CI_NATIVE" = true ]; then opam install -y rocq-native; fi
- opam pin add --kind=path rocq-runtime.dev .
- opam pin add --kind=path rocq-core.dev .
- if [ "$ROCQ_CI_NATIVE" = true ]; then echo "Definition f x := x + x." > test_native.v; fi
- if [ "$ROCQ_CI_NATIVE" = true ]; then rocq c test_native.v; fi
- if [ "$ROCQ_CI_NATIVE" = true ]; then test -f .coq-native/Ntest_native.cmxs; fi
- opam pin add --kind=path coqide-server.dev .
- opam pin add --kind=path rocqide.dev .
- opam pin add --kind=path rocq-devtools .
- opam pin add --kind=path rocq-test-suite.dev . -v
- if command -v coqc; then exit 1; fi # coq-core didn't get autoinstalled
- opam pin add --kind=path coq-core.dev .
after_script:
- eval $(opam env)
- du -ha "$(coqc -where)" > files.listing
artifacts:
name: "$CI_JOB_NAME"
paths:
- files.listing
when: always
expire_in: 1 week
variables:
OPAM_VARIANT: "+flambda"
only: *full-ci
.nix-template:
stage: build-0
needs: []
interruptible: true
image: nixos/nix:latest
extends: .auto-use-tags
variables:
GIT_STRATEGY: none # Required because we don't have git
USER: root # Variable required by Cachix
before_script:
- cat /proc/{cpu,mem}info || true
# Use current worktree as tmpdir to allow exporting artifacts in case of failure
- export TMPDIR=$PWD
# Install Cachix
- nix-env -iA nixpkgs.cachix
- cachix use coq
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
paths:
- nix-build-coq.drv-0/*/test-suite/logs
expire_in: 1 week
##############################################################################
########################## End of templates ##################################
##############################################################################
docker-boot:
stage: docker
image: docker:stable
services:
- docker:dind
before_script: []
script:
- dev/tools/check-cachekey.sh
- docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- cd dev/ci/docker/old_ubuntu_lts
- if docker pull "$BASE_IMAGE"; then echo "Base image prebuilt!"; else docker build -t "$BASE_IMAGE" .; docker push "$BASE_IMAGE"; fi
- cd ../edge_ubuntu
- if docker pull "$EDGE_IMAGE"; then echo "Edge image prebuilt!"; else docker build -t "$EDGE_IMAGE" .; docker push "$EDGE_IMAGE"; fi
except:
variables:
- $SKIP_DOCKER == "true"
extends: .auto-use-docker-tags
timeout: 2h
build:base:
extends: .build-template
variables:
COQ_EXTRA_CONF: "-native-compiler yes"
only: *full-ci
# no rocqide for 32bit: libgtk installation problems
build:base+32bit:
extends: .build-template
variables:
OPAM_VARIANT: "+32bit"
COQ_EXTRA_CONF: "-native-compiler yes"
ROCQIDE: "no"
only: *full-ci
build:edge+flambda:
extends: .build-template
image: $EDGE_IMAGE
variables:
OPAM_VARIANT: "+flambda"
COQ_EXTRA_CONF: "-native-compiler yes"
only: *full-ci
build:base:dev:
extends: .build-template:base:dev
# Build using native dune rules
build:base:dev:dune:
stage: build-0
image: $EDGE_IMAGE
variables:
OPAM_VARIANT: "+flambda"
interruptible: true
extends: .auto-use-tags
script:
- cp theories/Corelib/dune.disabled theories/Corelib/dune
- cp theories/Ltac2/dune.disabled theories/Ltac2/dune
- dune build -p rocq-runtime,coq-core,rocq-core,coqide-server
- ls _build/install/default/lib/coq/theories/Init/Prelude.vo
- ls _build/install/default/lib/coq/user-contrib/Ltac2/Ltac2.vo
only: *full-ci
build:base+async:
extends: .build-template
variables:
COQ_EXTRA_CONF: "-native-compiler yes"
COQ_DUNE_EXTRA_OPT: "-async"
after_script:
- dmesg > dmesg.txt
allow_failure: true # See https://github.com/coq/coq/issues/9658
only:
variables:
- $UNRELIABLE =~ /enabled/ && $FULL_CI == "true"
artifacts:
when: always
paths:
- _install_ci
# All those are for the test-suite jobs, to be discarded once we have dune for the test-suite
- config/Makefile
- config/coq_config.py
- config/coq_config.ml
- config/coq_byte_config.ml
- config/dune.c_flags
- dmesg.txt
timeout: 1h 30min
lint:
stage: build-0
image: $EDGE_IMAGE
script: dev/lint-repository.sh
extends: .auto-use-tags
variables:
GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
OPAM_VARIANT: "+flambda"
# pkg:opam:
# extends: .pkg:opam-template
pkg:opam:native:
extends: .pkg:opam-template
variables:
ROCQ_CI_NATIVE: "true"
# broken, see eg https://gitlab.com/coq/coq/-/jobs/1754045983
# pkg:nix:deploy:
# extends: .nix-template
# environment:
# name: cachix
# url: https://coq.cachix.org
# script:
# - nix-build https://coq.inria.fr/nix/toolbox --argstr job coq --arg override "{coq = coq:$CI_COMMIT_SHA;}" -K | cachix push coq
# only:
# refs:
# - master
# - /^v.*\..*$/
# variables:
# - $CACHIX_AUTH_TOKEN
# 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_AUTH_TOKEN && $CACHIX_DEPLOYMENT_KEY
# # if the $CACHIX_AUTH_TOKEN variable isn't set, the job it depends on doesn't exist
# needs:
# - pkg:nix:deploy
# script:
# - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
# # Remove all pr branches because they could be missing when we run git fetch --unshallow
# - git branch --list 'pr-*' | xargs -r git branch -D
# - git fetch --unshallow
# - git branch -v
# - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"refs/heads/${CI_COMMIT_REF_NAME}"
pkg:nix:
extends: .nix-template
script:
- nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K
only: *full-ci
doc:refman:
extends: .doc-template
variables:
DUNE_TARGET: refman-html
artifacts:
paths:
- _build/log
- _build/default/doc/refman-html
doc:refman-pdf:
extends: .doc-template
variables:
DUNE_TARGET: refman-pdf
artifacts:
paths:
- _build/log
- _build/default/doc/refman-pdf
doc:init:
extends: .doc-template
variables:
DUNE_TARGET: corelib-html
artifacts:
paths:
- _build/log
- _build/default/doc/corelib/html
doc:refman:deploy:
extends: .deploy-template
environment:
name: deployment
url: https://coq.github.io/
only:
variables:
- $DOCUMENTATION_DEPLOY_KEY
needs:
- doc:ml-api:odoc
- doc:ci-refman
- doc:init
- library:ci-stdlib_doc
script:
- echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
- git clone git@github.com: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/corelib
- rm -rf _deploy/$CI_COMMIT_REF_NAME/refman-stdlib
- 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/refman-html _deploy/$CI_COMMIT_REF_NAME/refman
- cp -rv _build/default/doc/corelib/html _deploy/$CI_COMMIT_REF_NAME/corelib
- cp -rv saved_build_ci/stdlib/_build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman-stdlib
- cp -rv saved_build_ci/stdlib/_build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib
- cd _deploy/$CI_COMMIT_REF_NAME/
- git add api refman corelib refman-stdlib 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: .doc-template
variables:
DUNE_TARGET: apidoc
artifacts:
paths:
- _build/log
- _build/default/_doc/
test-suite:base:
extends: .test-suite-template
needs:
- build:base
only: *full-ci
test-suite:base+32bit:
extends: .test-suite-template
needs:
- build:base+32bit
variables:
OPAM_VARIANT: "+32bit"
only: *full-ci
test-suite:edge+flambda:
extends: .test-suite-template
image: $EDGE_IMAGE
needs:
- build:edge+flambda
variables:
OPAM_VARIANT: "+flambda"
only: *full-ci
test-suite:base:dev:
stage: build-1
interruptible: true
extends: .auto-use-tags
needs:
- build:base:dev
script:
- tar xfj _build.tar.bz2
- make test-suite
artifacts:
name: "$CI_JOB_NAME.logs"
when: on_failure
paths:
- _build/default/test-suite/logs
expire_in: 1 week
.test-suite:ocaml+beta+dune-template:
stage: build-1 # even though it has no deps we put it with the other test suite jobs
needs:
- docker-boot
interruptible: true
script:
- opam switch create $OCAMLVER --empty
- eval $(opam env)
- opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
- opam update
- opam install ocaml-variants=$OCAMLVER
- opam install dune zarith
- eval $(opam env)
- export COQ_UNIT_TEST=noop
- make test-suite
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
needs:
- build:base
variables:
COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force"
allow_failure: true
only:
variables:
- $UNRELIABLE =~ /enabled/ && $FULL_CI == "true"
validate:base:
extends: .validate-template
variables:
CI_TARGETS: "stdlib"
needs:
- build:base
- library:ci-stdlib
only: *full-ci
# we currently don't have a stdlib+32bit job
validate:base+32bit:
extends: .validate-template
needs:
- build:base+32bit
variables:
OPAM_VARIANT: "+32bit"
only: *full-ci
validate:edge+flambda:
extends: .validate-template
image: $EDGE_IMAGE
variables:
CI_TARGETS: "stdlib"
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
variables:
OPAM_VARIANT: "+flambda"
only: *full-ci
# Libraries are by convention the projects that depend on Rocq
# but not on its ML API
library:ci-argosy:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-autosubst:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-bbv:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-bedrock2:
extends: .ci-template-flambda
variables:
NJOBS: "1"
SAVE_BUILD_CI: "1" # for bedrock2_examples
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-coqutil
- library:ci-kami
- library:ci-riscv_coq
stage: build-3+
library:ci-bedrock2_examples:
extends: .ci-template-flambda
variables:
NJOBS: "1"
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-coqutil
- library:ci-kami
- library:ci-riscv_coq
- library:ci-bedrock2
stage: build-3+
timeout: 2h
library:ci-category_theory:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-equations
stage: build-2
library:ci-color:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-bignums
stage: build-2
library:ci-compcert:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-flocq
- library:ci-menhir
stage: build-2
library:ci-coq_performance_tests:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-coq_tools:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-coqprime:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-bignums
stage: build-2
library:ci-coqtail:
extends: .ci-template
library:ci-coquelicot:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-coqutil:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-cross_crypto:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-engine_bench:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-ext_lib:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-fcsl_pcm:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-2
library:ci-fiat_crypto:
extends: .ci-template-flambda
variables:
COQEXTRAFLAGS: "-async-proofs-tac-j 0"
SAVE_BUILD_CI: "1" # for fiat_crypto_ocaml
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-coqutil
- library:ci-kami
- library:ci-riscv_coq
- library:ci-bedrock2
- library:ci-coqprime
- library:ci-rupicola
- plugin:ci-rewriter
stage: build-3+
timeout: 3h
library:ci-fiat_crypto_legacy:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
timeout: 1h 30min
# We cannot use flambda due to
# https://github.com/ocaml/ocaml/issues/7842, see
# https://github.com/coq/coq/pull/11916#issuecomment-609977375
library:ci-fiat_crypto_ocaml:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-coqutil
- library:ci-kami
- library:ci-riscv_coq
- library:ci-bedrock2
- library:ci-coqprime
- library:ci-rupicola
- plugin:ci-rewriter
- library:ci-fiat_crypto
stage: build-3+
artifacts:
paths: [] # These artifacts would go over the size limit
library:ci-flocq:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-kami:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-menhir:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-oddorder:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-fourcolor:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-corn:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-bignums
- plugin:ci-elpi_hb # CoRN uses elpi only (not HB) - depending on ci-elpi_hb reduces CI package count
- library:ci-math_classes
stage: build-3+
library:ci-hott:
extends: .ci-template-flambda
library:ci-iris:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-autosubst
stage: build-2
library:ci-math_classes:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-bignums
stage: build-2
library:ci-mathcomp:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-elpi_hb # for Hierarchy Builder
stage: build-2
variables:
SAVE_BUILD_CI: "1" # for mathcomp_test
library:ci-mathcomp_test:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-mczify:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-algebra_tactics:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
- library:ci-mczify
stage: build-3+
library:ci-finmap:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-bigenough:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-analysis:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-mathcomp
- library:ci-finmap
- library:ci-bigenough
- plugin:ci-elpi_hb # for Hierarchy Builder
stage: build-3+
variables:
SAVE_BUILD_CI: "1" # for analysis_stdlib
library:ci-analysis_stdlib:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-mathcomp
- library:ci-finmap
- library:ci-bigenough
- library:ci-analysis
- plugin:ci-elpi_hb # for Hierarchy Builder
- library:ci-stdlib+flambda
stage: build-3+
library:ci-neural_net_interp:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-paco:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-itree:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-ext_lib
- library:ci-paco
stage: build-2
library:ci-itree_io:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-ext_lib
- library:ci-paco
- library:ci-simple_io
- library:ci-itree
stage: build-3+
library:ci-simple_io:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-ext_lib
stage: build-2
library:ci-sf:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-stdlib:
extends: .ci-template
variables:
SAVE_BUILD_CI: "1" # for test suite
library:ci-stdlib+flambda:
extends: .ci-template-flambda
variables:
CI_TARGETS: "stdlib"
SAVE_BUILD_CI: "1" # for test suite
library:ci-stdlib_test:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
stage: build-2
library:ci-stdlib_doc:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
stage: build-2
variables:
SAVE_BUILD_CI: "1" # for doc:refman:deploy
library:ci-tlc:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
library:ci-unimath:
extends: .ci-template-flambda
library:ci-verdi_raft:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-vst:
extends: .ci-template-flambda
variables:
NJOBS: "1"
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-flocq
- library:ci-menhir
- library:ci-compcert
stage: build-3+
timeout: 2h
library:ci-deriving:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
library:ci-mathcomp_word:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-2
.library:ci-jasmin: # disabled until repaired
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
- library:ci-mathcomp_word
- library:ci-mczify
- library:ci-algebra_tactics
- library:ci-ext_lib
- library:ci-paco
- library:ci-itree
stage: build-3+
library:ci-http:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
- library:ci-menhir
- library:ci-ext_lib
- library:ci-simple_io
- library:ci-paco
- library:ci-itree
- library:ci-itree_io
- plugin:ci-quickchick
stage: build-3+
variables:
CI_TARGETS: "ceres parsec json async_test http"
library:ci-trakt:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
stage: build-2
# Plugins are by definition the projects that depend on Rocq's ML API
plugin:ci-aac_tactics:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-atbr:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-autosubst_ocaml:
extends: .ci-template-flambda
plugin:ci-itauto:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-bignums:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-coinduction:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-coq_dpdgraph:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-coqhammer:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-elpi_hb:
extends: .ci-template-flambda
needs:
- build:edge+flambda
variables:
CI_TARGETS: "elpi hb"
SAVE_BUILD_CI: "1" # for elpi_test and hb_test
plugin:ci-elpi_test:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
stage: build-2
plugin:ci-hb_test:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
stage: build-2
plugin:ci-equations:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
variables:
SAVE_BUILD_CI: "1" # for equations_test
plugin:ci-equations_test:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-equations
stage: build-2
plugin:ci-fiat_parsers:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
plugin:ci-lean_importer:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
plugin:ci-ltac2_compiler:
extends: .ci-template
plugin:ci-metarocq:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-equations
stage: build-2
timeout: 1h 30min
plugin:ci-mtac2:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
variables:
CI_TARGETS: "unicoq mtac2"
plugin:ci-paramcoq:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-perennial:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:plugin-tutorial:
stage: build-0
interruptible: true
extends: .auto-use-tags
script:
- ./configure -prefix "$(pwd)/_install_ci"
- make -j "$NJOBS" plugin-tutorial
plugin:ci-quickchick:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-ext_lib
- library:ci-simple_io
- plugin:ci-elpi_hb
- library:ci-mathcomp
stage: build-3+
variables:
SAVE_BUILD_CI: "1" # for quickchick_test
plugin:ci-quickchick_test:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-ext_lib
- library:ci-simple_io
- plugin:ci-elpi_hb
- library:ci-mathcomp
- plugin:ci-quickchick
stage: build-3+
plugin:ci-reduction_effects:
extends: .ci-template-flambda
plugin:ci-relation_algebra:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
- plugin:ci-aac_tactics
stage: build-3+
plugin:ci-rewriter:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
library:ci-riscv_coq:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-coqutil
stage: build-2
library:ci-rupicola:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- library:ci-coqutil
- library:ci-kami
- library:ci-riscv_coq
- library:ci-bedrock2
stage: build-3+
plugin:ci-coq_lsp:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
plugin:ci-vsrocq:
extends: .ci-template-flambda
plugin:ci-smtcoq:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
plugin:ci-smtcoq_trakt:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-trakt
stage: build-3+
plugin:ci-stalmarck:
extends: .ci-template
needs:
- build:base
- library:ci-stdlib
plugin:ci-tactician:
extends: .ci-template-flambda
plugin:ci-waterproof:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
doc:ci-refman:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-elpi_hb
- library:ci-mathcomp
- library:ci-mczify
stage: build-3+
artifacts:
paths:
- _build/log
- _build/default/doc/refman-html
- _build/default/doc/refman-pdf
pipeline-stats:
image: $EDGE_IMAGE
extends: .auto-use-tags
stage: stats
dependencies: []
before_script: []
script:
- dev/tools/pipeline-stats.py
when: always
[ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
]
|
2026-03-28
|
|
|
|
|
