diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 11:00:20 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 11:00:20 +0200 |
commit | 296941dc97d53817cc58b4687ed99168e1dd33a9 (patch) | |
tree | 0fe64507c184d3fc31c2c9219cf2068363c8e2c6 | |
parent | 53fe81925820895e5657ec8c1d0389e96a0abc70 (diff) | |
parent | 741943da6e42937f6d50db9c920a40073160eebc (diff) |
Merge PR #979: Fix install-doc target and other gitlab failures
-rw-r--r-- | .gitlab-ci.yml | 43 | ||||
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | Makefile.doc | 15 | ||||
-rw-r--r-- | dev/ci/ci-common.sh | 2 |
4 files changed, 32 insertions, 29 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8beeffcca..ae55302d1 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -21,7 +21,7 @@ variables: COMPILER_BLEEDING_EDGE: "4.05.0" CAMLP5_VER_BLEEDING_EDGE: "7.01" - TEST_PACKAGES: "time python" + TIMING_PACKAGES: "time python" COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" @@ -58,14 +58,14 @@ before_script: artifacts: name: "$CI_JOB_NAME" paths: - - install + - _install_ci - config/Makefile expire_in: 1 week script: - set -e - echo 'start:coq.config' - - ./configure -prefix "$(pwd)/install" ${EXTRA_CONF} + - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF} - echo 'end:coq.config' - echo 'start:coq.build' @@ -74,7 +74,7 @@ before_script: - echo 'start:coq.install' - make install - - cp bin/fake_ide install/bin/ + - cp bin/fake_ide _install_ci/bin/ - echo 'end:coq.install' - set +e @@ -110,7 +110,9 @@ before_script: - cd test-suite - make clean # careful with the ending / - - make -j ${NJOBS} BIN=$(readlink -f ../install/bin)/ LIB=$(readlink -f ../install/lib/coq)/ all + - BIN=$(readlink -f ../_install_ci/bin)/ + - LIB=$(readlink -f ../_install_ci/lib/coq)/ + - make -j ${NJOBS} BIN="$BIN" LIB="$LIB" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -120,7 +122,7 @@ before_script: .validate-template: &validate-template stage: test script: - - cd install + - cd _install_ci - find lib/coq/ -name '*.vo' -print0 > vofiles - 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/ @@ -128,10 +130,10 @@ before_script: .documentation-template: &documentation-template stage: test script: - - ./configure -prefix "$(pwd)/install" ${EXTRA_CONF} - - cp install/lib/coq/tools/coqdoc/coqdoc.sty . + - INSTALLDIR=$(readlink -f _install_ci) + - ./configure -prefix "$INSTALLDIR" ${EXTRA_CONF} + - cp "$INSTALLDIR/lib/coq/tools/coqdoc/coqdoc.sty" . - - INSTALLDIR=$(readlink -f install) - LIB="$INSTALLDIR/lib/coq" # WTF using a newline makes make sigsev # see https://gitlab.com/SkySkimmer/coq/builds/17313312 @@ -145,7 +147,7 @@ before_script: artifacts: name: "$CI_JOB_NAME" paths: - - install/share/doc + - _install_ci/share/doc expire_in: 1 week .ci-template: &ci-template @@ -160,6 +162,7 @@ before_script: - build variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" + EXTRA_PACKAGES: "$TIMING_PACKAGES" build: <<: *build-template @@ -201,7 +204,7 @@ test-suite: dependencies: - build variables: - EXTRA_PACKAGES: "$TEST_PACKAGES" + EXTRA_PACKAGES: "$TIMING_PACKAGES" test-suite:32bit: <<: *test-suite-template @@ -209,7 +212,7 @@ test-suite:32bit: - build:32bit variables: COMPILER: "$COMPILER_32BIT" - EXTRA_PACKAGES: "gcc-multilib $TEST_PACKAGES" + EXTRA_PACKAGES: "gcc-multilib $TIMING_PACKAGES" test-suite:bleeding-edge: <<: *test-suite-template @@ -218,7 +221,7 @@ test-suite:bleeding-edge: variables: COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" - EXTRA_PACKAGES: "$TEST_PACKAGES" + EXTRA_PACKAGES: "$TIMING_PACKAGES" documentation: <<: *documentation-template @@ -258,7 +261,7 @@ ci-color: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "subversion" + EXTRA_PACKAGES: "$TIMING_PACKAGES subversion" ci-compcert: <<: *ci-template @@ -268,13 +271,13 @@ ci-coq-dpdgraph: variables: <<: *ci-template-vars EXTRA_OPAM: "ocamlgraph" - EXTRA_PACKAGES: "autoconf" + EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-coquelicot: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "autoconf" + EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-geocoq: <<: *ci-template @@ -289,13 +292,13 @@ ci-fiat-parsers: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "python" + EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-flocq: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "autoconf" + EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-formal-topology: <<: *ci-template @@ -304,7 +307,7 @@ ci-hott: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "autoconf" + EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-iris-coq: <<: *ci-template @@ -319,7 +322,7 @@ ci-sf: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "wget" + EXTRA_PACKAGES: "$TIMING_PACKAGES wget" ci-unimath: <<: *ci-template @@ -54,6 +54,7 @@ FIND_SKIP_DIRS:='(' \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ -name '_build_ci' -o \ + -name '_install_ci' -o \ -name 'user-contrib' -o \ -name 'coq-makefile' -o \ -name '.opamcache' -o \ diff --git a/Makefile.doc b/Makefile.doc index 3f8ae3680..0c3b70149 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -218,13 +218,9 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ @touch $(INDEXES) (cd doc/common/styles/html/$(HTMLSTYLE);\ for f in `find . -name \*.css`; do \ - install -m 644 -D $$f ../../../../refman/html/$$f;\ + $(MKDIR) $$(dirname ../../../../refman/html/$$f);\ + $(INSTALLLIB) $$f ../../../../refman/html/$$f;\ done) - (cd doc/common/styles/html/$(HTMLSTYLE);\ - for f in `find . -name coqdoc.css -o -name style.css`; do \ - install -m 644 -D $$f ../../../../refman/html/;\ - done) - install -m 644 doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ @@ -391,8 +387,11 @@ install-doc-meta: install-doc-html: $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq) - $(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman - $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib + (for f in `cd doc/refman/html; find . -type f`; do \ + $(MKDIR) $$(dirname $(FULLDOCDIR)/html/refman/$$f);\ + $(INSTALLLIB) doc/refman/html/$$f $(FULLDOCDIR)/html/refman/$$f;\ + done) + $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html $(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 238960948..358f527f9 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -4,7 +4,7 @@ set -xe if [ -n "${GITLAB_CI}" ]; then - export COQBIN=`pwd`/install/bin + export COQBIN=`pwd`/_install_ci/bin else export COQBIN=`pwd`/bin fi |