| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-03-12 | Fix public headers for make install. (#2856) | Mathias Preiner | |
| This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4. Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API). | |||
| 2018-10-20 | Travis: run examples and avoid building them twice (#2663) | Andres Noetzli | |
| `make check` builds the examples but does not run them. This commit changes our Travis script to run the examples after building them and removes `makeExamples()` to avoid building them twice. | |||
| 2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
| 2018-09-22 | travis: Switch to cmake. | Mathias Preiner | |
| 2018-08-27 | Remove Coverity build from Travis (#2373) | Andres Noetzli | |
| The Coverity build is now done as part of our nightlies and the Travis Coverity build was timing out most of the time anyway, so this commit removes it. | |||
| 2018-08-07 | Delete functions instead of using CVC4_UNDEFINED (#1794) | Andres Noetzli | |
| C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable. | |||
| 2018-03-26 | Regression level 0 for distcheck on Travis (#1714) | Andres Noetzli | |
| We are running all our Travis tests with regression level 0 except for distcheck, which is running with the default level 1. This commit lowers the level to 0 to make all jobs consistent. | |||
| 2018-03-08 | Fix Travis for unit test compilation errors. (#1651) | Mathias Preiner | |
| make units does not fail if we have compile error for a unit test, however, make check does. -Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings. Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds. | |||
| 2018-02-16 | Make regress1 default, only test regress0 on Travis. (#1611) | Aina Niemetz | |
| 2018-02-07 | Reduce number of Travis builds. (#1578) | Aina Niemetz | |
| 2018-01-08 | Remove portfolio option from builds. (#1496) | Aina Niemetz | |
| 2017-12-18 | Fix travis write errors. (#1445) | Aina Niemetz | |
| For reasons unknown, after the latest update of the Trusty environment on Travis, we encountered write errors for the three Clang builds. As suggested here https://github.com/travis-ci/travis-ci/issues/4704#issuecomment-321777557, adding filter_secrets: false to the .travis.yml fixes the problem. Note: switching back to the deprecated builds did not fix the problem. | |||
| 2017-10-11 | Reduce number of travis builds. | Mathias Preiner | |
| This also removes the Java API test code, which will be tested in the nightly builds. Same goes for the removed portfolio builds. | |||
| 2017-09-14 | Enable ccache compression, increase cache size (#1099) | Andres Noetzli | |
| This commit enables compression for ccache, increases the cache size to 1GB and resets the ccache statistics before each run. | |||
| 2017-09-13 | Make ccache work with Clang on Travis (#1097) | Andres Noetzli | |
| This commit uses a workaround [0] to get ccache to work with Clang on Travis. [0] https://github.com/travis-ci/travis-ci/issues/5383#issuecomment-224630584 | |||
| 2017-09-12 | Enable ccache on Travis, disable debug symbols (#1094) | Andres Noetzli | |
| Enable ccache on Travis for faster compile times. Also disable debug symbols for the debug builds on Travis to use the available cache more efficiently. Note: this change only works on GCC, support for Clang will require additional changes but the time savings should already be pretty significant. | |||
| 2017-09-01 | Add travis debug build with cln. (#1066) | Aina Niemetz | |
| Until now, all travis builds where built with gmp. This commit adds an additional debug build built with cln. | |||
| 2017-08-31 | Add GCC7 jobs to Travis (#1054) | Andres Noetzli | |
| This commit adds two jobs (debug, with portfolio, test groups 0 and 1) to Travis. Both jobs are added using matrix.include, based on the example in the documentation: https://docs.travis-ci.com/user/languages/cpp/#GCC-on-Linux . This unfortunately requires some code duplication but there does not seem to be a way to do it in a much better fashion. | |||
| 2017-08-31 | Replace CVC4_THREADLOCAL in interactive_shell (#1065) | Andres Noetzli | |
| Commit 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4 caused our nightly builds to fail because it did not replace CVC4_THREADLOCAL with CVC4_THREAD_LOCAL in interactive_shell. This commit fixes the issue and adds readline to Travis, s.t. readline related code gets compiled as part of our CI tests. | |||
| 2017-08-30 | Remove Coverity SSL certificate workaround from Travis configuration. (#1058) | Mathias Preiner | |
| Coverity works without the SSL certificate workaround and is not needed anymore. Note that we don't require sudo anymore and we could switch to container-based Travis builds (instead of VM-based). However, container-based environments only provide 4G of memory (instead of 7.5G for VMs) , which is not enough for the current CVC4 build environment. | |||
| 2017-08-29 | Fix indentation for disabled Java tests. | Mathias Preiner | |
| 2017-08-29 | Disable Java tests for now until they get fixed. | Mathias Preiner | |
| 2017-08-28 | Run Ant on Travis | Pat Hawks | |
| 2017-08-28 | Travis: Package instead of download for cxxtest (#1055) | Andres Noetzli | |
| Before this commit, we were downloading cxxtest from Sourceforge. This commit instead installs the Ubuntu package, which is easier and more reliable. Instead of adding the package to the list of packages for Coverity and the common list of packages, this commit changes the Coverity package list to just refer to the common list of packages. | |||
| 2017-08-25 | Move LFSC checker out of the CVC repository. (#222) | Aina Niemetz | |
| LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution anymore. As a consequence, we + Add --with-lfsc and --with-lfsc-directory as configure options. In the case where CVC4 has not been built with integrated LFSC, all code that interacts with LFSC is disabled. + Disable proof checking if CVC4_USE_LFSC is not defined. Configuring the build with --check-proofs but without --with-lfsc results in an error. + Do not call LFSC's cleanup function (but we should in the future). LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt. Disabled call to lfscc_cleanup until the problem in lfscc is fixed. + Disable building with LFSC for the distcheck travis build since it is not part of the distribution anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker before calling make check on the temp build (the build of the unpacked distribution tar ball). | |||
| 2017-08-24 | Test Java API on CI | Pat Hawks | |
| 2017-08-07 | Optionally split regression tests into test groups (#207) | Andres Noetzli | |
| To prevent timing out on Travis, this commit adds the option to split the regression tests into groups and run each group in a separate job. The group of a test is determined by computing a checksum of its name. | |||
| 2017-07-26 | -Og for non-opt build, parallel pcvc4 check (#206) | Andres Noetzli | |
| -Og enables optimizations that do not interfere with debugging. This is the new default for debug builds if the compiler supports the flag. This commit also enables parallel checking for the portfolio build on Travis. | |||
| 2017-07-23 | Disabling compiling unit tests with coverity scan for now. | Tim King | |
| 2017-07-14 | Disable separate gnu++11 tests on Travis (#193) | Andres Noetzli | |
| Given that we are now always compiling with gnu++11, we don't need separate tests anymore. | |||
| 2017-01-05 | Disabling a regression test that assumes CVC4 is configured with proofs on. ↵ | Tim King | |
| Modifying the travis rules so there are instances with proofs disabled. | |||
| 2016-09-25 | Integrating a working coverity_scan travis rule back into master. | Tim King | |
| 2016-09-21 | Fixing an error in the previous travis commit. | Tim King | |
| 2016-09-20 | Updating the travis file for coverity scan. | Tim King | |
| 2016-09-18 | Adding a gnu++11 rule to travis. | Tim King | |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King | |
| What to Know As a User: A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems. The Problem: The build order of CVC4 used to be [roughly] specified as: options < expr < util < libcvc4 < parsers < main Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable. The Solution: To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen: 1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file. 2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options. 3. All of the old options_handlers.h files have been refactored. 4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary. 5. I am removing the libstatistics library. The constraints that the CVC4 build system will eventually satisfy are: - The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files. - The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases. - The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.) - One library per Makefile.am. - No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.) The build order of CVC4 can now be [roughly] specified as base < options < util < expr < smt_util < libcvc4 < parsers < main The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean. More details about the directories: base/ The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere. options/ The options/ directory is self contained. - It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h . - There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options. - Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done. - The */options_handlers.h files have been removed. - The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp. - All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h . util/ The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean. expr/ The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/. - An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h. - Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h. - The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/. - Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes. - Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources. - This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC. smt_util/ The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel. What is up next: - A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed. - The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up. | |||
| 2015-11-23 | Switching travis over to using the containers infrastructure. | Tim King | |
| 2015-11-12 | Updating the contrib/new-theory script and travis to use the new ↵ | Tim King | |
| Makefile.theories script. | |||
| 2015-11-12 | Updating the contrib/new-theory script and travis to use the new ↵ | Tim King | |
| Makefile.theories script. | |||
| 2014-06-19 | Some reversions of recent commits re: portfolio failure. | Morgan Deters | |
| * Partial reversion of b8e28a7, do it a different way. * Revert "Test portfolio with --no-wait-to-join." This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c. | |||
| 2014-06-19 | Test portfolio with --no-wait-to-join. | Morgan Deters | |
| 2014-06-15 | fix travis config | Morgan Deters | |
| 2014-04-10 | refactor .travis.yml | Kshitij Bansal | |
| 2014-03-31 | Travis-CI test for new-theory script, also related bugfixes. | Morgan Deters | |
| 2014-01-08 | Merge branch '1.3.x' | Morgan Deters | |
| Conflicts: COPYING NEWS config/cvc4.m4 | |||
| 2014-01-08 | Cache apt packages on Travis. | Morgan Deters | |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
| generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
| 2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
| 2013-12-16 | Send Travis-CI emails to everyone | Morgan Deters | |
| 2013-12-13 | Fix to Travis-CI config. | Morgan Deters | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
path: root/.travis.yml
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback