aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-color.sh2
-rw-r--r--dev/ci/ci-common.sh2
-rwxr-xr-xdev/ci/ci-compcert.sh2
-rwxr-xr-xdev/ci/ci-cpdt.sh2
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh3
-rwxr-xr-xdev/ci/ci-fiat-parsers.sh2
-rwxr-xr-xdev/ci/ci-formal-topology.sh6
-rwxr-xr-xdev/ci/ci-geocoq.sh2
-rwxr-xr-xdev/ci/ci-hott.sh2
-rwxr-xr-xdev/ci/ci-iris-coq.sh4
-rwxr-xr-xdev/ci/ci-math-classes.sh4
-rwxr-xr-xdev/ci/ci-math-comp.sh2
-rwxr-xr-xdev/ci/ci-metacoq.sh4
-rwxr-xr-xdev/ci/ci-sf.sh2
-rwxr-xr-xdev/ci/ci-template.sh2
-rwxr-xr-xdev/ci/ci-tlc.sh2
-rwxr-xr-xdev/ci/ci-unimath.sh2
-rwxr-xr-xdev/ci/ci-vst.sh2
18 files changed, 24 insertions, 23 deletions
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index a0a4e0749d..309050057c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -32,4 +32,4 @@ sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUt
sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
-( cd ${Color_CI_DIR} && make -j ${NJOBS} )
+( cd ${Color_CI_DIR} && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 5435e95885..238960948d 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -68,7 +68,7 @@ install_ssreflect()
sed -i.bak '/field/d' Make && \
sed -i.bak '/fingroup/d' Make && \
sed -i.bak '/algebra/d' Make && \
- make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+ make Makefile.coq && make -f Makefile.coq all && make install )
echo -en 'travis_fold:end:ssr.install\\r'
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index c78ffdc2c0..0dd904648c 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -9,4 +9,4 @@ opam install -j ${NJOBS} -y menhir
git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
# Patch to avoid the upper version limit
-( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 0e791ebbfd..8b725f6fec 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -6,5 +6,5 @@ source ${ci_dir}/ci-common.sh
wget http://adam.chlipala.net/cpdt/cpdt.tgz
tar xvfz cpdt.tgz
-( cd cpdt && make clean && make -j ${NJOBS} )
+( cd cpdt && make clean && make )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c6df45a1d4..5ca3ac47fc 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,5 +6,6 @@ source ${ci_dir}/ci-common.sh
fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
+( cd ${fiat_crypto_CI_DIR} && git submodule update --init --recursive )
-( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} lite )
+( cd ${fiat_crypto_CI_DIR} && make lite )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 2095245eb8..292331b813 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
-( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples && make -j ${NJOBS} fiat-core )
+( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 64b78c0396..2556f84a55 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -17,16 +17,16 @@ source ${ci_dir}/ci-bignums.sh
git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
-( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${math_classes_CI_DIR} && make && make install )
# Setup Corn
git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
-( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${Corn_CI_DIR} && make && make install )
# Setup formal-topology
git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
-( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} )
+( cd ${formal_topology_CI_DIR} && make )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 4e5aa2687b..eadeb7c38c 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -13,4 +13,4 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
sed -i.bak '/Elements\/Book_1\.v/d' Make && \
sed -i.bak '/Elements\/Book_3\.v/d' Make && \
coq_makefile -f Make -o Makefile && \
- make -j ${NJOBS} )
+ make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 1bf6e9a872..693135a4c9 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 262dd6fa01..2d127ddc1b 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -20,7 +20,7 @@ stdpp_CI_COMMIT=${IRIS_DEP[2]}
git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
-( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${stdpp_CI_DIR} && make && make install )
# Build iris now
-( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
+( cd ${Iris_CI_DIR} && make )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 46581c6381..2837dee963 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -15,10 +15,10 @@ source ${ci_dir}/ci-bignums.sh
git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
-( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${math_classes_CI_DIR} && make && make install )
# Setup Corn
git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
-( cd ${Corn_CI_DIR} && make -j ${NJOBS} )
+( cd ${Corn_CI_DIR} && make )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index bb8188da4e..701403f2cf 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -12,4 +12,4 @@ checkout_mathcomp ${mathcomp_CI_DIR}
( cd ${mathcomp_CI_DIR}/mathcomp && \
sed -i.bak '/PFsection/d' Make && \
sed -i.bak '/stripped_odd_order_theorem/d' Make && \
- make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
+ make Makefile.coq && make -f Makefile.coq all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index e31691179e..c813b1fe99 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -10,10 +10,10 @@ metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
-( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && make install )
# Setup MetaCoq
git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
-( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 23ef41d2dd..6e6c7012b7 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -9,6 +9,6 @@ tar xvfz sf.tgz
sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
-( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
+( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
index 700105aed4..25da01a822 100755
--- a/dev/ci/ci-template.sh
+++ b/dev/ci/ci-template.sh
@@ -9,4 +9,4 @@ Template_CI_DIR=${CI_BUILD_DIR}/Template
git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
-( cd ${Template_CI_DIR} && make -j ${NJOBS} )
+( cd ${Template_CI_DIR} && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index ce26399378..8ecd8c441d 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -7,4 +7,4 @@ tlc_CI_DIR=${CI_BUILD_DIR}/tlc
git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
-( cd ${tlc_CI_DIR} && make -j ${NJOBS} )
+( cd ${tlc_CI_DIR} && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 175b82b5f9..66b56add77 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -10,5 +10,5 @@ git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
( cd ${UniMath_CI_DIR} && \
sed -i.bak '/Folds/d' Makefile && \
sed -i.bak '/HomologicalAlgebra/d' Makefile && \
- make -j ${NJOBS} BUILD_COQ=no )
+ make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index c111951852..27a336d80c 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -10,4 +10,4 @@ git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
# Targets are: msl veric floyd
# Patch to avoid the upper version limit
-( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} )
+( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make )
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:07:18 +0000