aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml43
-rw-r--r--Makefile1
-rw-r--r--Makefile.doc15
-rw-r--r--dev/ci/ci-common.sh2
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
diff --git a/Makefile b/Makefile
index 82595a6e6..4786e0f7c 100644
--- a/Makefile
+++ b/Makefile
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 23:44:09 +0000