Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
121 lines (110 sloc) 4.51 KB
language: c
sudo: false
os:
- linux
branches:
except:
- /^lean-.*$/
env:
global:
- secure: "HxnRtl6pMc+nbszQgDgvMuroMG5AuviULPb0MxPfEIZqYSwKALgc0ILXc89kJyf9rFfpsUdKGmtrGOytzXIp8Yuxvp+fnk/rtuuRyMLeWA0sJ75/Jn+l0BKVid6LNwl7bA4aMOSkjL85kaxU2e5HtlROUkiAgmdAcV10BoK7Vh7yC/S4Zl3kzyCQd8AGSxk0AbeQrb9vK7T1+gWVkEjUFtUsFJ3q5SGrO/j3825qLoRnYj/bKUgtYExQNKjTnTYMbeok+mKJEO1VbLeTk1ri8bLyO2x25lhGImaJSgdPOzuH905ALrf+EHkKm/FYvy5w+zERiuidwwFK5OqVOVWsD5W0G5rYKmDKpzSd39FNnrvb2Tzl2kCin70j6SDOXyZ+4k/iGJpBnOtx3+Ez4gsBDWLIba1c5EXvzhvPoycddgSLBY2LNz4EJI+YqbBTBxG7dVr4NmKKjPowFerVMLM10SgkH9ZZjbAVMxejUJTzp/4gxTanlWm/xds5uC0E0mraLY1H1yzGtwij/lVJN8RGbuhvW9jluLYQzfN7Hb/MReBXTKwdVo5SnsZzv9GEM56IsQXgIhzRoHAuDHd8rS1rfXGaOVfsbYK7pBjtx9j+Pq3BNSPlIL5u4j2JXH6QVJSNaK1npCq81S21dIBfYTP49ft28bhgVE0czkD7kl3fCCk="
cache:
directories:
- $TRAVIS_BUILD_DIR/test/
- $TRAVIS_BUILD_DIR/src/
- $HOME/.elan
install:
- |
if [ ! -d "$HOME/.elan/toolchains/" ]; then
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
fi
- source ~/.elan/env
- mkdir $HOME/scripts || echo ""
- export PATH="$HOME/scripts:$PATH"
- cp travis_long.sh $HOME/scripts/travis_long
- chmod +x $HOME/scripts/travis_long
- (git status | grep -e "Changes not staged for commit:"); RESULT=$?
- if [ $RESULT -eq 0 ]; then git checkout -f HEAD ; fi
- git clean -d -f -q
- ./purge_olean.sh
- rm mathlib.txt || true
- export LEAN_VERSION=lean-`lean --run scripts/lean_version.lean`
jobs:
include:
- env: TASK="check Lean proofs"
stage: Pre-build-1
script:
- travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
- env: TASK="check Lean proofs"
stage: Pre-build-2
script:
- travis_long "timeout 2400 leanpkg test" | python scripts/detect_errors.py
- env: TASK="check Lean proofs"
stage: Test
script:
- travis_long "leanpkg test"
- lean --recursive --export=mathlib.txt src/
- travis_long "leanchecker mathlib.txt"
- sh scripts/deploy_nightly.sh
- env: TASK="check install scripts"
if: type != pull_request OR head_repo = leanprover-community/mathlib
language: python
python:
- "3.6"
install:
- if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi
os:
- linux
script:
- cp scripts/leanpkg-example.toml leanpkg.toml
- sh scripts/remote-install-update-mathlib.sh --global
- source $HOME/.profile
- update-mathlib
- env: TASK="check install scripts"
if: type != pull_request OR head_repo = leanprover-community/mathlib
language: sh
install:
- if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi
os:
- osx
script:
- cp scripts/leanpkg-example.toml leanpkg.toml
- sh scripts/remote-install-update-mathlib.sh
- source $HOME/.profile
- update-mathlib
- env: TASK="check dev scripts"
if: type != pull_request OR head_repo = leanprover-community/mathlib
sudo: true
language: python
python:
- "3.4"
install:
- if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi
os:
- linux
script:
- cp scripts/leanpkg-example.toml leanpkg.toml
- cd scripts
- echo y | bash setup-dev-scripts.sh --global
- source $HOME/.profile
- update-mathlib
- cache-olean
- cache-olean --fetch
- env: TASK="check dev scripts"
if: type != pull_request OR head_repo = leanprover-community/mathlib
language: sh
install:
- if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi
os:
- osx
script:
- cp scripts/leanpkg-example.toml leanpkg.toml
- cd scripts
- echo y | bash setup-dev-scripts.sh
- source $HOME/.profile
- update-mathlib
- cache-olean
- cache-olean --fetch
notifications:
webhooks:
- https://leanprover.zulipchat.com/api/v1/external/travis?stream=travis&topic=build-status&api_key=SwF1QzwUWol76dCxsYgwHbI6giN3cxGn
You can’t perform that action at this time.