diff options
-rw-r--r-- | .gitlab-ci.yml | 43 | ||||
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | dev/ci/ci-common.sh | 2 |
3 files changed, 25 insertions, 21 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/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 |