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