| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 32 kB |
|
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)/../_ins 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 || touc - 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_buil - 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_ - cd ../edge_ubuntu - if docker pull "$EDGE_IMAGE"; then echo "Edge image prebuilt!"; else docker build -t "$EDGE_ 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: # 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_COM 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 - cp -rv saved_build_ci/stdlib/_build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF - 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 - 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.8 Sekunden (vorverarbeitet) ] |
2026-03-28