diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 16f8e1c4de8df0758b4dc1569746ad7700678ff3..4e2129ba02b9b4606d45c3abf2663ec67fc518b2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,7 +1,22 @@ +###################### Global Config ###################### + +workflow: + rules: + - if: '$CI_PIPELINE_SOURCE == "merge_request_event"' + - if: '$CI_COMMIT_BRANCH && $CI_OPEN_MERGE_REQUESTS' + when: never + - if: '$CI_COMMIT_BRANCH' + stages: - build - process +###################### Rules and Scripts ################## + +.not_in_wip_branches: + rules: + - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event") + .build-common: stage: build script: @@ -21,14 +36,14 @@ stages: image: mathcomp/mathcomp-dev:${CI_JOB_NAME} extends: .build-common -.build-for-process: +.compile: stage: build image: mathcomp/mathcomp:1.12.0-coq-8.13 script: - ./create_makefile.sh --without-classic - make -j ${NJOBS} -.build-for-process-classic: +.compile-classic: stage: build image: mathcomp/mathcomp:1.12.0-coq-8.13 script: @@ -63,26 +78,50 @@ stages: - "*/*/*/*/*/*/*/*/*/*.glob" expire_in: 1 week +.doc: + extends: + - .preferred-stable-version + stage: process + script: + - make html -j ${NJOBS} + - mv html with-proofs + - make gallinahtml -j ${NJOBS} + - mv html without-proofs + - make htmlpretty -j ${NJOBS} + - mv html pretty + + +###################### The Jobs ###################### + 1.10.0-coq-8.11: - extends: .build + extends: + - .build + - .not_in_wip_branches 1.11.0-coq-8.11: - extends: .build + extends: + - .build + - .not_in_wip_branches 1.11.0-coq-8.12: - extends: .build + extends: + - .build + - .not_in_wip_branches 1.12.0-coq-8.13: - extends: .build + extends: + - .build + - .not_in_wip_branches -build-for-process: +compile: extends: - - .build-for-process + - .compile - .collect-vo-files -build-for-process-classic: +compile-classic: extends: - - .build-for-process-classic + - .not_in_wip_branches + - .compile-classic - .collect-vo-files proof-length: @@ -92,59 +131,55 @@ proof-length: - scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v` spell-check: + extends: + - .not_in_wip_branches stage: build image: bbbrandenburg/aspell-ci script: - scripts/flag-typos-in-comments.sh `find . -iname '*.v' ! -path './classic/*'` +# mathcomp-dev with stable Coq 8.13 coq-8.13: extends: - .build-dev + - .not_in_wip_branches # it's ok to fail with an unreleased version of ssreflect allow_failure: true +# mathcomp-dev with coq-dev coq-dev: extends: - .build-dev + - .not_in_wip_branches # it's ok to fail with an unreleased version of ssreflect and Coq allow_failure: true validate: extends: + - .not_in_wip_branches - .preferred-stable-version stage: process - needs: ["build-for-process"] + needs: ["compile"] dependencies: - - build-for-process + - compile script: make validate validate-classic: extends: + - .not_in_wip_branches - .preferred-stable-version stage: process - needs: ["build-for-process-classic"] + needs: ["compile-classic"] dependencies: - - build-for-process-classic + - compile-classic script: make validate -.doc: - extends: - - .preferred-stable-version - stage: process - script: - - make html -j ${NJOBS} - - mv html with-proofs - - make gallinahtml -j ${NJOBS} - - mv html without-proofs - - make htmlpretty -j ${NJOBS} - - mv html pretty - doc: extends: - .doc - needs: ["build-for-process"] + needs: ["compile"] dependencies: - - build-for-process + - compile artifacts: name: "prosa-spec-$CI_COMMIT_REF_NAME" paths: @@ -155,10 +190,11 @@ doc: doc-classic: extends: + - .not_in_wip_branches - .doc - needs: ["build-for-process-classic"] + needs: ["compile-classic"] dependencies: - - build-for-process-classic + - compile-classic artifacts: name: "prosa-classic-spec-$CI_COMMIT_REF_NAME" paths: @@ -169,11 +205,12 @@ doc-classic: proof-state: extends: + - .not_in_wip_branches - .preferred-stable-version stage: process - needs: ["build-for-process"] + needs: ["compile"] dependencies: - - build-for-process + - compile script: - make alectryon - mv html ../with-proofs-and-proof-state