aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-09 01:14:24 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-09 01:14:24 +0200
commitded7ac52847670a6f4f51671e2101a4fdd13a29e (patch)
treee609b0401e17fd61dff56060a43c42b0e70fe6ff
parent8fd1904d8bed254f04b39ba5d6067915b85e36b6 (diff)
parent871a9e65009990963c12359531ea2beeacb7386d (diff)
Merge PR #7515: gitlab: build sphinx doc in separate job
-rw-r--r--.gitlab-ci.yml25
-rw-r--r--Makefile.doc3
-rw-r--r--doc/tools/coqrst/repl/coqtop.py5
3 files changed, 29 insertions, 4 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:
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):