michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
4102 commits 3 branches 0 tags 28 MiB
Commit graph

92 commits

Author SHA1 Message Date
Leonardo de Moura
f49a610995 fix(.travis.yml): (try to fix) random build failures at travis 
At https://bitcointalk.org/index.php?topic=304389.0, people suggest
that the failure

    g++-4.8: internal compiler error: Killed (program cc1plus)

usually happens when the system does not have enough free memory.
A possible workaround is to disable parallel build, and compile file by
file. I added the option `-j1` to Ninja.
 2014-09-26 09:05:30 -07:00
Leonardo de Moura
480bc639ea feat(build): add IGNORE_SORRY cmake option 
It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
 2014-09-26 08:55:54 -07:00
Soonho Kong
bf02c54591 chore(.travis): install valgrind before we install c++ compiler 2014-09-10 09:47:43 -07:00
Soonho Kong
2e3306dc85 chore(.travis.yml): avoid g++-4.8.1 + DEBUG + TCMALLOC 
The combination sometimes triggers the following compiler error:

The log says:
               g++-4.8: internal compiler error: Killed (program cc1plus)

See: https://travis-ci.org/leanprover/lean/jobs/34351197

We can try this one again when travis-ci.org switches to Ubuntu 14.04 where we can use either gcc-4.8.3 or gcc-4.9.0.

See: https://github.com/travis-ci/travis-ci/issues/2046
 2014-09-04 15:41:07 -07:00
Soonho Kong
ba13144094 chore(.travis.yml): add 'travis_wait' to doxygen build 
"If you have a command that doesn't produce output for
more than 10 minutes, you can prefix it with travis_wait,
 a function that's exported by our build environment."

http://docs.travis-ci.com/user/build-timeouts/
 2014-06-02 22:37:27 -04:00
Leonardo de Moura
0f894f4618 chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 17:47:53 -07:00
Soonho Kong
cf25c626e5 chore(travis): fix bitbucket push 
Problem
=======

For efficiency, travis-ci uses shallow clone by doing

    git clone --depth=50 ...

which checks out recent 50 commits from the repo.

However, recent changes on bitbucket side rejects a shallow clone of a
repository.

Solution
========

We do

    git fetch --unshallow;

before we push to other repositories.
 2014-05-04 17:49:32 -04:00
Soonho Kong
4fddc5b8bc chore(travis): use lean-build@googlegroups 2014-05-02 17:21:54 -04:00
Soonho Kong
219e9d6c0c chore(travis): re-encrypt secure keys for leanprover/lean 
Travis-ci[1] supports encryption key feature[2]. The caveat is that
plain-texts are encrypted and decrypted using repository's public and
private keys. That is, if we migrate our blessed repo to another one, we
need to re-encrypt and update our secure keys in .travis.yml file:

 - GH_TOKEN : to push to OSX/Windows repositories
              (Github token for account "soonhokong")

 - DROPBOX_KEY : to push compiled binaries to DROPBOX
                 (DROPBOX_KEY=access token)

 - REPO : encrypt "BLESSED". If travis-ci is running on another
          repository, REPO variable is not decrypted to "BLESSED" because it
          will use a different private key. Many actions (i.e. upload to
          Dropbox, trigger OSX/Windows Builds) are protected by this
          condition.

 - COVERALLS_REPO_TOKEN: to push to https://coveralls.io
                         (https://coveralls.io/r/leanprover/lean)

[1]: http://travis-ci.com
[2]: http://docs.travis-ci.com/user/encryption-keys/
 2014-05-02 00:10:56 -04:00
Leonardo de Moura
ba34c5d588 chore(.travis.yml): remove automatic copy to bitbucket 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 15:10:47 -07:00
Leonardo de Moura
d1e1ce4f5c fix(.travis.yml): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 09:47:50 -07:00
Soonho Kong
fa1f64e2d5 chore(travis): fix another typo 2013-12-26 02:57:13 -05:00
Soonho Kong
0efb7e8297 chore(travis): fix typo 2013-12-26 02:38:16 -05:00
Soonho Kong
558c07738c chore(travis): fix package name 2013-12-26 02:34:22 -05:00
Soonho Kong
06899d02c0 chore(travis): upload Lean package to Dropbox 2013-12-26 02:25:09 -05:00
Soonho Kong
e6df417440 chore(travis): use another repository to fix luajit problem on ubuntu 2013-12-23 16:43:22 -05:00
Soonho Kong
2cdd06b182 chore(travis): use ppa to install LuaJit-2.0.1 on Ubuntu 2013-12-23 15:35:51 -05:00
Soonho Kong
cbd7333550 chore(travis): fix Lua packages (Linux) 2013-12-13 17:55:54 -05:00
Soonho Kong
cb09b9ba14 chore(travis): add extra builds to test Lua-5.1 and LuaJit on OSX and Linux 2013-12-13 15:08:23 -05:00
Soonho Kong
7359f360db chore(travis): restore multiple builds 2013-11-17 03:04:37 -05:00
Soonho Kong
5d26ce6c32 chore(travis): test doxygen-upload #1 2013-11-17 02:24:07 -05:00
Soonho Kong
e5dbcc8ac5 chore(travis): fix typo in Linux build (dropbox upload) 2013-11-17 01:31:14 -05:00
Soonho Kong
0e9ca085ad chore(travis): fix typo in Linux build 2013-11-17 01:00:56 -05:00
Soonho Kong
4cc16e06a0 chore(travis): fix typo in Linux build 2013-11-17 00:28:21 -05:00
Soonho Kong
e61a5271ab chore(travis): fix doxygen-upload in Linux build 2013-11-16 23:54:33 -05:00
Soonho Kong
b1916721f2 chore(travis): update coveralls.io repo token 2013-11-10 02:04:27 -05:00
Soonho Kong
27710a778a chore(travis): use gcov-4.8 on ubuntu 2013-11-10 01:52:47 -05:00
Soonho Kong
7831b534ba chore(travis): fix lcov permission problem 2013-11-10 01:44:50 -05:00
Soonho Kong
6a2dfe7765 chore(travis): add coveralls.io support 2013-11-10 00:52:32 -05:00
Soonho Kong
6cb282d70b chore(travis): split a memcheck build into two builds using range option (-I) 2013-11-06 13:49:14 -05:00
Leonardo de Moura
36fe8e5c5f feat(lua): install Lua at travis VM 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 11:21:30 -07:00
Soonho Kong
a46b313c1c chore(travis): use demangle_cpptype.py to print out test/valgrind output 
[skip ci]
 2013-09-29 16:30:02 -07:00
Soonho Kong
80c282d0a3 chore(travis): do not use c++filt on Linux builds 
There is a bug in c++filt on Linux. For instance,

    c++filt -t 355687428096000

causes a segmentation fault.
 2013-09-29 13:27:32 -07:00
Soonho Kong
58e2ec331c chore(travis): use c++filt to handle demangled c++ names 2013-09-28 23:38:22 -07:00
Soonho Kong
d48ec2ddfa chore(travis): fix git-commit-msg extraction 
[skip-ci]
 2013-09-28 13:33:13 -07:00
Soonho Kong
db6e0ce319 chore(travis): set stack size as unlimited before run valgrind 2013-09-27 19:05:23 -07:00
Soonho Kong
f1407d501a chore(travis): fix testcov problem 2013-09-27 17:56:33 -07:00
Soonho Kong
0ce089b942 chore(travis): push all linux builds to cdash 2013-09-27 17:56:33 -07:00
Soonho Kong
3527babfee chore(travis): use consistent build name 
- have build name is in the form of
       "<BRANCH>_<CXX_COMPILER>_<BUILD_TYPE>(_TC)?"
   to have consistency over time.
 - have "Generator" field in cdash XMLs which is in the form of
        "<GIT_COMMIT>###<GIT_SUBJECT>"
   it will be displayed as a small mouseover-text.
 2013-09-27 12:22:44 -07:00
Soonho Kong
a05b6b476e fix(testcov): install lcov and include testcov only when it's on 2013-09-26 22:24:24 -07:00
Soonho Kong
5e5087b0a3 chore(testcov): add compile target "cov" to run code-coverage locally 
- need to run cmake with "-DTESTCOV=ON" and "-DCMAKE_BUILD_TYPE=Debug"
 - type "make/ninja cov"
 - open "coverage/index.html" to check the code coverage
 2013-09-26 20:28:52 -07:00
Soonho Kong
875fda80de Update .travis.yml 
- make TCMALLOC explicit
 2013-09-20 13:45:10 -07:00
Soonho Kong
49efbad8df Update .travis.yml 
[skip ci]
 2013-09-20 11:34:36 -07:00
Soonho Kong
85a92e8888 Fix typo in .travis.yml 2013-09-16 18:51:59 -07:00
Soonho Kong
a2182b59e3 Fix memcheck.supp problem 2013-09-16 18:14:55 -07:00
Soonho Kong
9b792d938d Update .travis.yml 
fix typo [skip ci]
 2013-09-15 22:07:55 -07:00
Soonho Kong
e6d9aa7527 Use GNU parallel to upload doxygen files to dropbox 
[skip ci]
 2013-09-15 20:31:15 -07:00
Soonho Kong
b1310bd679 Update .travis.yml 
- force to use precompiled cmake
- do not delete old doxygen files (will fix later)
[skip ci]
 2013-09-15 13:51:02 -07:00
Soonho Kong
5edf78559d Fix typo in .travis.yml 2013-09-15 12:27:42 -07:00
Soonho Kong
2d8febb7f1 Fix .travis.yml 
- Use precompiled cmake
- clang + ninja + release build still has a bug. Use make instead.
 2013-09-15 12:23:10 -07:00