diff options
| -rw-r--r-- | .gitlab-ci.yml | 25 | ||||
| -rw-r--r-- | Makefile.doc | 3 | ||||
| -rw-r--r-- | 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): |