From b207b8e6953d76af98e1d18983fb1467fc8fe8f5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 16 Jun 2017 17:50:41 -0400 Subject: Remove -j ${NJOBS} from make invocations in the ci According to https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make` invocation in `.travis.yml`. Additionally, explicitly passing `-j` in, e.g., fiat-crypto, results in error messages such as ``` make[2]: *** write jobserver: Bad file descriptor. Stop. make[2]: *** Waiting for unfinished jobs.... make[2]: *** write jobserver: Bad file descriptor. Stop. make[1]: *** [coqprime] Error 2 make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2! make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c ``` because the `-j` on the `make` in the `ci-fiat-crypto.sh` script disables jobserver mode, and the submake in fiat-crypto to make coqprime does not explicitly pass `-j`, and so reenables jobserver mode, and then `make` gets very confused. Commit made with ```bash cd dev/ci git grep --name-only -- 'make -j ${NJOBS}' | xargs sed s'/make -j \${NJOBS}/make/g' -i git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' | xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i ``` --- dev/ci/ci-bedrock-facade.sh | 2 +- dev/ci/ci-bedrock-src.sh | 2 +- dev/ci/ci-color.sh | 2 +- dev/ci/ci-common.sh | 2 +- dev/ci/ci-compcert.sh | 2 +- dev/ci/ci-cpdt.sh | 2 +- dev/ci/ci-fiat-crypto.sh | 2 +- dev/ci/ci-fiat-parsers.sh | 2 +- dev/ci/ci-formal-topology.sh | 6 +++--- dev/ci/ci-geocoq.sh | 2 +- dev/ci/ci-hott.sh | 2 +- dev/ci/ci-iris-coq.sh | 4 ++-- dev/ci/ci-math-classes.sh | 4 ++-- dev/ci/ci-math-comp.sh | 2 +- dev/ci/ci-metacoq.sh | 4 ++-- dev/ci/ci-sf.sh | 2 +- dev/ci/ci-template.sh | 2 +- dev/ci/ci-tlc.sh | 2 +- dev/ci/ci-unimath.sh | 2 +- dev/ci/ci-vst.sh | 2 +- 20 files changed, 25 insertions(+), 25 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh index 95cfa3073..9e6b6b108 100755 --- a/dev/ci/ci-bedrock-facade.sh +++ b/dev/ci/ci-bedrock-facade.sh @@ -7,4 +7,4 @@ bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR} -( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade ) +( cd ${bedrock_facade_CI_DIR} && make facade ) diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh index 532611d4b..a642354e6 100755 --- a/dev/ci/ci-bedrock-src.sh +++ b/dev/ci/ci-bedrock-src.sh @@ -7,4 +7,4 @@ bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR} -( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src ) +( cd ${bedrock_src_CI_DIR} && make src ) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 3f0716511..57b50fc8d 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -7,4 +7,4 @@ Color_CI_DIR=${CI_BUILD_DIR}/color svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} -( 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 2711b7eca..d373ed3b1 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -59,7 +59,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 c78ffdc2c..0dd904648 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 0e791ebbf..8b725f6fe 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 ad6cb8c0e..5ca3ac47f 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -8,4 +8,4 @@ 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 d8460bc70..e7f98c3de 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 ) +( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index ecb36349f..056655cf6 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -13,16 +13,16 @@ formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology 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 4e5aa2687..eadeb7c38 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 1bf6e9a87..693135a4c 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 262dd6fa0..2d127ddc1 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 beb75773b..f177d231b 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -11,10 +11,10 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn 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 bb8188da4..701403f2c 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 e31691179..c813b1fe9 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 7d23ccad9..ae7a13b53 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -7,6 +7,6 @@ source ${ci_dir}/ci-common.sh wget ${sf_CI_TARURL} tar xvfz sf.tgz -( 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 700105aed..25da01a82 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 ce2639937..8ecd8c441 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 175b82b5f..66b56add7 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 c11195185..27a336d80 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 ) -- cgit v1.2.3