From 871a9e65009990963c12359531ea2beeacb7386d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 14 May 2018 18:29:02 +0200
Subject: gitlab: build sphinx doc in separate job

---
 .gitlab-ci.yml                  | 25 +++++++++++++++++++++++--
 Makefile.doc                    |  3 ++-
 doc/tools/coqrst/repl/coqtop.py |  5 ++++-
 3 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a6eed661e..b9e780061 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -55,6 +55,7 @@ before_script:
     paths:
       - _install_ci
       - config/Makefile
+      - config/coq_config.py
       - test-suite/misc/universes/all_stdlib.v
     expire_in: 1 week
   script:
@@ -70,7 +71,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'
 
@@ -109,6 +110,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
@@ -181,7 +195,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:
@@ -228,6 +244,11 @@ warnings:edge:
     <<: *warnings-variables
     OPAM_SWITCH: edge
 
+documentation:
+  <<: *doc-template
+  dependencies:
+    - build:base
+
 test-suite:base:
   <<: *test-suite-template
   dependencies:
diff --git a/Makefile.doc b/Makefile.doc
index 4670c79ec..dde3a37b7 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -31,6 +31,7 @@ DVIPS:=dvips
 HTMLSTYLE:=coqremote
 
 # Sphinx-related variables
+SPHINXENV:=COQBIN="$(CURDIR)/bin/"
 SPHINXOPTS= -j4
 SPHINXBUILD= sphinx-build
 SPHINXBUILDDIR= doc/sphinx/_build
@@ -55,7 +56,7 @@ endif
 
 sphinx: $(SPHINX_DEPS)
 	$(SHOW)'SPHINXBUILD doc/sphinx'
-	$(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
+	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
 	@echo
 	@echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html."
 
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index aeadce4c4..3ff00eaaf 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -41,10 +41,13 @@ class CoqTop:
                            the ansicolors module)
         :param args:       Additional arugments to coqtop.
         """
+        BOOT = True
+        if os.getenv('COQBOOT') == "no":
+            BOOT = False
         self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
         if not pexpect.utils.which(self.coqtop_bin):
             raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin))
-        self.args = (args or []) + ["-boot", "-color", "on"] * color
+        self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color
         self.coqtop = None
 
     def __enter__(self):
-- 
cgit v1.2.3