Moving Gitlab CI documentation build to the main Coq build.

1 files changed, 8 insertions, 41 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 04b75bfdf..03e001f4a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,8 +27,9 @@ variables:
   #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
   COQIDE_OPAM: "lablgtk-extras"
   COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6"
-  COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa"
+  COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa python3-pip"
   COQDOC_OPAM: "hevea"
+  SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex"
 
 
 before_script:
@@ -36,6 +37,7 @@ before_script:
   - printenv
 #  - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
   - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -qq && sudo apt-get install -y -qq ${EXTRA_PACKAGES}; fi
+  - if [ -n "${PIP_PACKAGES}" ]; then sudo pip3 install ${PIP_PACKAGES}; fi
 
   # setup cache
   - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi
@@ -132,28 +134,6 @@ before_script:
     - 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 -boot -silent -o -m -coqlib lib/coq/
 
-.documentation-template: &documentation-template
-  stage: test
-  script:
-    - INSTALLDIR=$(readlink -f _install_ci)
-    - cp "$INSTALLDIR/lib/coq/tools/coqdoc/coqdoc.sty" .
-
-    - LIB="$INSTALLDIR/lib/coq"
-    # WTF using a newline makes make sigsev
-    # see https://gitlab.com/SkySkimmer/coq/builds/17313312
-    - DOCVFILES=$(find "$LIB/" -name '*.v' -printf "%p ")
-    - DOCLIGHTDIRS="$LIB/theories/Init/ $LIB/theories/Logic/ $LIB/theories/Unicode/ $LIB/theories/Arith/"
-    - DOCLIGHTVOFILES=$(find $DOCLIGHTDIRS -name '*.vo' -printf "%p ")
-
-    - make doc QUICK=true COQDOC_NOBOOT=true COQTEX="$INSTALLDIR/bin/coq-tex" COQDOC="$INSTALLDIR/bin/coqdoc" VFILES="$DOCVFILES" THEORIESLIGHTVO="$DOCLIGHTVOFILES"
-
-    - make install-doc
-  artifacts:
-    name: "$CI_JOB_NAME"
-    paths:
-      - _install_ci/share/doc
-    expire_in: 1 week
-
 .ci-template: &ci-template
   stage: test
   script:
@@ -170,6 +150,11 @@ before_script:
 
 build:
   <<: *build-template
+  variables:
+    EXTRA_CONF: "-with-doc yes"
+    EXTRA_PACKAGES: "$COQDOC_PACKAGES"
+    EXTRA_OPAM: "$COQDOC_OPAM"
+    PIP_PACKAGES: "$SPHINX_PACKAGES"
 
 # no coqide for 32bit: libgtk installation problems
 build:32bit:
@@ -229,24 +214,6 @@ test-suite:bleeding-edge:
     CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
     EXTRA_PACKAGES: "$TIMING_PACKAGES"
 
-documentation:
-  <<: *documentation-template
-  dependencies:
-    - build
-  variables:
-    EXTRA_PACKAGES: "$COQDOC_PACKAGES"
-    EXTRA_OPAM: "$COQDOC_OPAM"
-
-documentation:bleeding-edge:
-  <<: *documentation-template
-  dependencies:
-    - build:bleeding-edge
-  variables:
-    COMPILER: "$COMPILER_BLEEDING_EDGE"
-    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
-    EXTRA_PACKAGES: "$COQDOC_PACKAGES"
-    EXTRA_OPAM: "$COQDOC_OPAM"
-
 validate:
   <<: *validate-template
   dependencies: