diff --git a/.travis.yml b/.travis.yml index 5eab889d1..c26e0535c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -137,12 +137,12 @@ install: until sudo apt-get -qq update; do echo retry; done; until sudo apt-get -qq install libluajit-5.1-dev luajit; do echo retry; done; fi - - wget http://dl.dropboxusercontent.com/u/203889738/gcc/ninja.tar.gz; - tar xfz ninja.tar.gz; - cd ninja; - ./bootstrap.py > /dev/null 2>&1; - sudo cp -v ninja /usr/bin/; - cd ..; + - wget http://dl.dropboxusercontent.com/u/203889738/gcc/ninja.tar.gz && + tar xfz ninja.tar.gz && + cd ninja && + ./bootstrap.py > /dev/null 2>&1 && + sudo cp -v ninja /usr/bin/ && + cd .. - until sudo apt-get -qq install libstdc++-4.9-dev; do echo retry; done - if [[ $REPO == BLESSED && $MEMCHECK == TRUE ]]; then sudo apt-get -qq install valgrind; @@ -150,15 +150,15 @@ install: - if [[ $CMAKE_CXX_COMPILER == g++-4.9 ]]; then until sudo apt-get -qq install g++-4.9; do echo retry; done fi - if [[ $CMAKE_CXX_COMPILER == clang++-3.4 ]]; then until sudo apt-get -qq install clang-3.4; do echo retry; done fi - if [[ $REPO == BLESSED && ($UPLOAD || $BUILD_DOXYGEN == TRUE) ]]; then - sudo apt-get -qq install python python-pip; - sudo pip install dropbox; + sudo apt-get -qq install python python-pip && + sudo pip install dropbox fi - if [[ $TESTCOV == ON ]]; then - wget http://downloads.sourceforge.net/ltp/lcov-1.11.tar.gz; - tar xvfz lcov-1.11.tar.gz; - sudo make -C lcov-1.11 install - rm -rf lcov-1.11.tar.gz lcov-1.11; - sudo cp -v `which gcov-4.9` `which gcov`; + wget http://downloads.sourceforge.net/ltp/lcov-1.11.tar.gz && + tar xvfz lcov-1.11.tar.gz && + sudo make -C lcov-1.11 install && + rm -rf lcov-1.11.tar.gz lcov-1.11 && + sudo cp -v `which gcov-4.9` `which gcov` fi before_script: @@ -167,124 +167,124 @@ before_script: git push -q https://soonhok:${BB_TOKEN}@bitbucket.org/leanprover/lean.git +HEAD:master; fi - if [[ $REPO == BLESSED && $TRIGGER_OSX == TRUE ]]; then - MSG=`git log --pretty=oneline --abbrev-commit -n 1 | cut -d ' ' -f 2-`; - cp .travis.yml /tmp/.travis.temp.yml; - cp .travis.osx.yml .travis.yml; - git config --global user.email "notifications@travis-ci.org"; - git config --global user.name "Travis CI"; - git add .travis.yml; - git commit -m "$MSG"; - git push -q https://soonhokong:${GH_TOKEN}@github.com/soonhokong/lean-osx.git +HEAD:master; - mv /tmp/.travis.temp.yml .travis.yml; - git reset --hard HEAD~; + MSG=`git log --pretty=oneline --abbrev-commit -n 1 | cut -d ' ' -f 2-` && + cp .travis.yml /tmp/.travis.temp.yml && + cp .travis.osx.yml .travis.yml && + git config --global user.email "notifications@travis-ci.org" && + git config --global user.name "Travis CI" && + git add .travis.yml && + git commit -m "$MSG" && + git push -q https://soonhokong:${GH_TOKEN}@github.com/soonhokong/lean-osx.git +HEAD:master && + mv /tmp/.travis.temp.yml .travis.yml && + git reset --hard HEAD~ fi - if [[ $REPO == BLESSED && $TRIGGER_WINDOWS == TRUE ]]; then - MSG=`git log --pretty=oneline --abbrev-commit -n 1 | cut -d ' ' -f 2-`; - cp .travis.yml /tmp/.travis.temp.yml; - cp .travis.windows.yml .travis.yml; - git config --global user.email "notifications@travis-ci.org"; - git config --global user.name "Travis CI"; - git add .travis.yml; - git commit -m "$MSG"; - git push -q https://soonhokong:${GH_TOKEN}@github.com/soonhokong/lean-windows.git +HEAD:master; - mv /tmp/.travis.temp.yml .travis.yml; - git reset --hard HEAD~; + MSG=`git log --pretty=oneline --abbrev-commit -n 1 | cut -d ' ' -f 2-` && + cp .travis.yml /tmp/.travis.temp.yml && + cp .travis.windows.yml .travis.yml && + git config --global user.email "notifications@travis-ci.org" && + git config --global user.name "Travis CI" && + git add .travis.yml && + git commit -m "$MSG" && + git push -q https://soonhokong:${GH_TOKEN}@github.com/soonhokong/lean-windows.git +HEAD:master && + mv /tmp/.travis.temp.yml .travis.yml && + git reset --hard HEAD~ fi script: - mkdir -p build - cd build - if [[ $CMAKE_BUILD_TYPE == Release && $CMAKE_CXX_COMPILER=clang++-3.4 ]]; then - GENERATOR=; + GENERATOR= else - GENERATOR=-GNinja; + GENERATOR=-GNinja fi - if [[ $TESTCOV != ON ]]; then - TESTCOV=OFF; + TESTCOV=OFF fi - - /usr/bin/cmake -DIGNORE_SORRY=ON -DCONSERVE_MEMORY=${CONSERVE_MEMORY} -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTESTCOV=${TESTCOV} -DTCMALLOC=${TCMALLOC} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} ${GENERATOR} -DCMAKE_PROGRAM_PATH=/usr/bin ../src; + - /usr/bin/cmake -DIGNORE_SORRY=ON -DCONSERVE_MEMORY=${CONSERVE_MEMORY} -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTESTCOV=${TESTCOV} -DTCMALLOC=${TCMALLOC} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} ${GENERATOR} -DCMAKE_PROGRAM_PATH=/usr/bin ../src - if [[ $CMAKE_BUILD_TYPE == Debug || $CMAKE_BUILD_TYPE == Release || $TESTCOV == ON ]]; then - SITE=Ubuntu12.04@Travis; + SITE=Ubuntu12.04@Travis && if [[ $CMAKE_BUILD_TYPE == Release ]]; then - BUILD_TYPE=Release; + BUILD_TYPE=Release else - BUILD_TYPE=Debug; - fi; - LUA_VERSION=LUA_${LUA}; - BUILD_NAME=${TRAVIS_BRANCH}_${CMAKE_CXX_COMPILER}_${BUILD_TYPE}_${LUA_VERSION}; + BUILD_TYPE=Debug + fi && + LUA_VERSION=LUA_${LUA} && + BUILD_NAME=${TRAVIS_BRANCH}_${CMAKE_CXX_COMPILER}_${BUILD_TYPE}_${LUA_VERSION} && if [[ $TCMALLOC == ON ]]; then - BUILD_NAME=${BUILD_NAME}_TC; - fi; - CONFIG_FILE=DartConfiguration.tcl; - sed -i "s/^Site:.*/Site:$SITE/" $CONFIG_FILE; - sed -i "s/BuildName:.*/BuildName:$BUILD_NAME/" $CONFIG_FILE; + BUILD_NAME=${BUILD_NAME}_TC + fi && + CONFIG_FILE=DartConfiguration.tcl && + sed -i "s/^Site:.*/Site:$SITE/" $CONFIG_FILE && + sed -i "s/BuildName:.*/BuildName:$BUILD_NAME/" $CONFIG_FILE && if [[ $MEMCHECK == TRUE ]]; then - ninja -j 1; + ninja -j 1 else - ctest -D ExperimentalConfigure; - sed -i "s/^Site:.*/Site:$SITE/" $CONFIG_FILE; - sed -i "s/BuildName:.*/BuildName:$BUILD_NAME/" $CONFIG_FILE; - ctest -D ExperimentalBuild -VV; - yes "C" | ctest -D ExperimentalTest -VV | ../script/demangle_cpptype.py; - fi; + ctest -D ExperimentalConfigure && + sed -i "s/^Site:.*/Site:$SITE/" $CONFIG_FILE && + sed -i "s/BuildName:.*/BuildName:$BUILD_NAME/" $CONFIG_FILE && + ctest -D ExperimentalBuild -VV && + yes "C" | ctest -D ExperimentalTest -VV | ../script/demangle_cpptype.py + fi fi - cd .. after_script: - cd build - if [[ $REPO == BLESSED && $TESTCOV == ON ]]; then - ctest -D ExperimentalCoverage; - ninja -j 1 cov; - npm install coveralls --save; - cat coverage.info.cleaned | ./node_modules/coveralls/bin/coveralls.js; + ctest -D ExperimentalCoverage && + ninja -j 1 cov && + npm install coveralls --save && + cat coverage.info.cleaned | ./node_modules/coveralls/bin/coveralls.js fi - if [[ $REPO == BLESSED && $MEMCHECK == TRUE ]]; then - MEMCHECK_SUPP=`readlink -f ../src/memcheck.supp`; - CONFIG_FILE=DartConfiguration.tcl; - sed -i "s,^MemoryCheckSuppressionFile:\W*$,MemoryCheckSuppressionFile:$MEMCHECK_SUPP," $CONFIG_FILE; - ulimit -s unlimited; - yes "C" | ctest -D ExperimentalMemCheck -LE expensive -VV -I $MEMCHECK_RANGE | ../script/demangle_cpptype.py; + MEMCHECK_SUPP=`readlink -f ../src/memcheck.supp` && + CONFIG_FILE=DartConfiguration.tcl && + sed -i "s,^MemoryCheckSuppressionFile:\W*$,MemoryCheckSuppressionFile:$MEMCHECK_SUPP," $CONFIG_FILE && + ulimit -s unlimited && + yes "C" | ctest -D ExperimentalMemCheck -LE expensive -VV -I $MEMCHECK_RANGE | ../script/demangle_cpptype.py fi - if [[ $REPO == BLESSED && $PUSH_TO_CDASH == TRUE ]]; then - GIT_COMMIT=`git log --oneline -n 1 | cut -d ' ' -f 1`; - GIT_SUBJECT=`git log --oneline -n 1 | cut -d ' ' -f 2-`; - GIT_SUBJECT=${GIT_SUBJECT//\"/\\\"}; - GIT_SUBJECT=${GIT_SUBJECT//,/\,}; - GIT_SUBJECT=$(echo -e $(printf '%q' "$GIT_SUBJECT")); - find Testing -name "*.xml" -exec sed -i "s,Generator=\".*\",Generator=\"${GIT_COMMIT}###${GIT_SUBJECT}\"," {} ";"; - find Testing \( -name "LastTest_*.log" -o -name "LastDynamicAnalysis_*.log" \) -exec sh -c 'TMP=`mktemp /tmp/ctesttmp_XXXX`; ../script/demangle_cpptype.py {} > $TMP; mv -v $TMP {}' ";"; - ctest -D ExperimentalSubmit; + GIT_COMMIT=`git log --oneline -n 1 | cut -d ' ' -f 1` && + GIT_SUBJECT=`git log --oneline -n 1 | cut -d ' ' -f 2-` && + GIT_SUBJECT=${GIT_SUBJECT//\"/\\\"} && + GIT_SUBJECT=${GIT_SUBJECT//,/\,} && + GIT_SUBJECT=$(echo -e $(printf '%q' "$GIT_SUBJECT")) && + find Testing -name "*.xml" -exec sed -i "s,Generator=\".*\",Generator=\"${GIT_COMMIT}###${GIT_SUBJECT}\"," {} ";" && + find Testing \( -name "LastTest_*.log" -o -name "LastDynamicAnalysis_*.log" \) -exec sh -c 'TMP=`mktemp /tmp/ctesttmp_XXXX`; ../script/demangle_cpptype.py {} > $TMP; mv -v $TMP {}' ";" && + ctest -D ExperimentalSubmit fi - if [[ $REPO == BLESSED && $PACKAGE == TRUE ]]; then - make package; + make package fi - cd .. - if [[ $REPO == BLESSED && $BUILD_DOXYGEN == TRUE ]]; then - sudo apt-get -qq install graphviz doxygen parallel; - script/doxygen.sh > /dev/null; - DOXYGEN_DIR=doc/html; - find $DOXYGEN_DIR -type f -name "*.md5" -exec rm {} ";"; - find $DOXYGEN_DIR -type f | split -l 100 - doxygen_files.txt.; - ls -1 doxygen_files.txt.* | travis_wait parallel -u -j 10 ./script/dropbox_upload.py --destpath /Public --dropbox-token ${DROPBOX_KEY} --copylist {}; + sudo apt-get -qq install graphviz doxygen parallel && + script/doxygen.sh > /dev/null && + DOXYGEN_DIR=doc/html && + find $DOXYGEN_DIR -type f -name "*.md5" -exec rm {} ";" && + find $DOXYGEN_DIR -type f | split -l 100 - doxygen_files.txt. && + ls -1 doxygen_files.txt.* | travis_wait parallel -u -j 10 ./script/dropbox_upload.py --destpath /Public --dropbox-token ${DROPBOX_KEY} --copylist {} fi - if [[ $REPO == BLESSED && $UPLOAD ]]; then - UPLOAD_DIR=bin; - BINARY=lean_${UPLOAD}; - NOW=`TZ='America/Los_Angeles' date +"%Y%m%d_%H%M"`; - GIT_COMMIT=`git log --oneline -n 1 | cut -d ' ' -f 1`; - OS=linux; - LUA_VERSION=LUA_${LUA}; - ARCHIVE_BINARY=${NOW}_${TRAVIS_BRANCH}_${GIT_COMMIT}_${OS}_${CMAKE_CXX_COMPILER}_${BUILD_TYPE}_${LUA_VERSION}; + UPLOAD_DIR=bin && + BINARY=lean_${UPLOAD} && + NOW=`TZ='America/Los_Angeles' date +"%Y%m%d_%H%M"` && + GIT_COMMIT=`git log --oneline -n 1 | cut -d ' ' -f 1` && + OS=linux && + LUA_VERSION=LUA_${LUA} && + ARCHIVE_BINARY=${NOW}_${TRAVIS_BRANCH}_${GIT_COMMIT}_${OS}_${CMAKE_CXX_COMPILER}_${BUILD_TYPE}_${LUA_VERSION} && if [[ $TCMALLOC == ON ]]; then - ARCHIVE_BINARY=${ARCHIVE_BINARY}_tcmalloc; - fi; - mkdir ${UPLOAD_DIR}; + ARCHIVE_BINARY=${ARCHIVE_BINARY}_tcmalloc + fi && + mkdir ${UPLOAD_DIR} && if [[ $REPO == BLESSED && $PACKAGE == TRUE ]]; then - cp -v build/lean*.tar.gz ${UPLOAD_DIR}/; - fi; - cp -v build/shell/lean ${UPLOAD_DIR}/${BINARY}; - tar cvfz ${UPLOAD_DIR}/${ARCHIVE_BINARY}.tar.gz ${UPLOAD_DIR}/${BINARY}; - script/dropbox_upload.py --srcpath ${UPLOAD_DIR} --destpath /Public/${UPLOAD_DIR} --dropbox-token ${DROPBOX_KEY}; + cp -v build/lean*.tar.gz ${UPLOAD_DIR}/ + fi && + cp -v build/shell/lean ${UPLOAD_DIR}/${BINARY} && + tar cvfz ${UPLOAD_DIR}/${ARCHIVE_BINARY}.tar.gz ${UPLOAD_DIR}/${BINARY} && + script/dropbox_upload.py --srcpath ${UPLOAD_DIR} --destpath /Public/${UPLOAD_DIR} --dropbox-token ${DROPBOX_KEY} fi notifications: