diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 05c2b4cc3..0bc67dfcc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -56,6 +56,7 @@ before_script: paths: - _install_ci - config/Makefile + - config/coq_config.py - test-suite/misc/universes/all_stdlib.v expire_in: 1 week script: @@ -71,7 +72,7 @@ before_script: - echo 'start:coq.build' - make -j "$NJOBS" byte - - make -j "$NJOBS" + - make -j "$NJOBS" world $EXTRA_TARGET - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' @@ -110,6 +111,19 @@ before_script: # purpose, we add a spurious dependency `not-a-real-job` that must be # overridden otherwise the CI will fail. +.doc-templare: &doc-template + stage: test + dependencies: + - not-a-real-job + script: + - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' + - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx + - make install-doc-sphinx + artifacts: + name: "$CI_JOB_NAME" + paths: + - _install_ci/share/doc/coq/ + # set dependencies when using .test-suite-template: &test-suite-template stage: test @@ -182,7 +196,9 @@ before_script: build:base: <<: *build-template variables: - COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" + # coqdoc for stdlib, until we know how to build it from installed Coq + EXTRA_TARGET: "stdlib" # no coqide for 32bit: libgtk installation problems build:base+32bit: @@ -229,6 +245,11 @@ warnings:edge: <<: *warnings-variables OPAM_SWITCH: edge +documentation: + <<: *doc-template + dependencies: + - build:base + test-suite:base: <<: *test-suite-template dependencies: |