.travis.yml

os:
  - linux
language: c++
sudo: true
dist: trusty
cache: apt
addons:
  apt:
    sources:
    - ubuntu-toolchain-r-test
    packages:
    - cmake
    - cmake-data
    - mercurial
    - python2.7
    - texlive-latex-recommended
    - texlive-humanities
    - texlive-xetex
    - texlive-science
    - texlive-latex-extra
    - texlive-luatex
    - texlive-fonts-recommended
    - latexmk
    - latex-xcolor
    - lmodern
    - pgf
    - moreutils
    - nodejs
    - npm
    - g++-5
    - libstdc++-5-dev
    - libgmp-dev
    - libmpfr-dev
    - liblua5.2-dev
    - emacs24
env:
  global:
   # GH_TOKEN=[secure]              (to push to leanprover org)
   - secure: "LAgBomK36BzF2mN/lOwua+gDzLgF6RyuMYBjMlP5KY3knUZT8m/9wff2GlWGm87anb6aIJH69ERjVyFU4sWi9qcD+26vs1m9agMFxuqTfpibeDoz/rd9D/9LA3mNeO6v5kR2FTQ/OTTC6nMC4olRxdzz22Jg9ly7cNzfFPuSGFA="
   # REPOn=BLESSED                  (to perform extra stuff only for pushes to the blessed repo)
   - secure: "Du/ZXFXdhRZL6AU6t6G8A3BNr3oPpHK4h2UCK00b+bgonHy7kDgTE0YxRVOf8VpXqfJwekzT4hWJhnKXasTp5avNEVEbdWC4nyM4tZbl6a8g8iI3Oo+JB6seSO6fIhrv6sZ7BCa6iuKDwzWJ0sQnXL+kx/zUqcle5eVUu5ic/24="
  matrix:
   - TEST=FALSE

before_install:
  - mkdir ~/bin
  - export PATH="/home/travis/.cask/bin:~/bin:$PATH"
  - curl -fsSL https://raw.github.com/cask/cask/master/go | python
  - cask
  - tar xvfz header/l3kernel.tar.gz -C ~/

install:
  # Install Lean dependencies
  - git clone https://github.com/leanprover/lean
  # Build Lean
  - if [[ $TEST == TRUE ]] ; then
      cd lean &&
      mkdir build &&
      cd build &&
      cmake -DIGNORE_SORRY=ON -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-5 ../src &&
      make &&
      cd ../../;
    fi
  # bibtex2html
  - wget --no-check-certificate http://www.lri.fr/\~filliatr/ftp/bibtex2html/bibtex2html-1.98-linux.tar.gz
  - tar xvfz bibtex2html-1.98-linux.tar.gz
  - cp -v bibtex2html-1.98-linux/* ~/bin
  - rm -rf bibtex2html-1.98-linux bibtex2html-1.98-linux.tar.gz
  - sudo npm -g i cssmin minify

script:
  - EMACS_BIN=emacs make
  # Build completion.js
  - echo "var completions = [" > js/completion.js
  - ./lean/bin/lean --server < js/completion_input.in | grep "|" | grep -v "^private\." | sort | uniq | sed -e "s/\([^|]\+\)|\(.\+\)/{name:\"\1\", value:\"\1\", meta:\"\2\"},/" >> js/completion.js
  - echo "]" >> js/completion.js
  # Build input-method.js
  - cask exec emacs --no-site-file --no-site-lisp -q --batch -l ./elisp/org-html-export.el -l ./lean/src/emacs/lean-input.el -f lean-input-export-translations-to-stdout > js/input-method.js
  # Push to gh-pages
  - if [[ "${REPO}" == "BLESSED" ]] && [[ "${TRAVIS_PULL_REQUEST}" == "false" ]] ; then
      git config --global user.email "notifications@travis-ci.org" &&
      git config --global user.name "Travis CI" &&
      git checkout --orphan gh-pages &&
      rm -f .git/index &&
      git add -f *.html tutorial.pdf quickref.pdf &&
      for CSS in css/*.css; do cssmin ${CSS} | sponge ${CSS} ; done &&
      git add css &&
      git add images &&
      git add fonts &&
      for JS in js/*.js; do minify ${JS} | sponge ${JS} ; done &&
      git add -f js/* &&
      rm -rf pygments-main &&
      git clean -fxd &&
      git commit -m "Update `date -R`" &&
      git push -q https://soonhokong:${GH_TOKEN}@github.com/leanprover/tutorial.git +HEAD:gh-pages &&
      git checkout -f master;
    fi
  # Test
  - if [[ $TEST == TRUE ]] ; then
        LEAN_BIN=lean/bin/lean make -j2 test;
    fi
  - if [[ $TEST_JS == TRUE ]] ; then
        make -j2 test_js;
    fi

notifications:
  email:
    recipients:
     - lean-build@googlegroups.com