| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-06-21 | Make CaDiCaL a required dependency. (#6761) | Mathias Preiner | |
| Since the new BV solver is enabled by default and uses CaDiCaL (and optionally CryptoMiniSat) we make CaDiCaL a required dependency. | |||
| 2021-06-16 | Make symfpu a required dependency. (#6749) | Aina Niemetz | |
| 2021-06-15 | Add cocoalib (#6731) | Gereon Kremer | |
| This PR adds CoCoALib as an optional dependency. It will be used in the CAD-based nonlinear solver for computer algebra routines beyond the capabilities of libpoly like quotient rings and polynomial factorization. | |||
| 2021-04-16 | Refactor cmake: auto-download and default-on dependencies (#6355) | Gereon Kremer | |
| This PR changes a few things in how dependencies are handled during configuration: - --x-dir are removed for most dependencies, use the generic --dep-path instead - the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves - external projects check this option and send an error if it is OFF - some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU) This will essentially fail every call to ./configure.sh until the user specifies --auto-download. | |||
| 2021-04-07 | New C++ Api: Initial setup of Api documentation. (#6295) | Aina Niemetz | |
| This configures the initial setup for generating Api documentation with Sphinx via Breathe and Doxygen. All fixes in the documentation of the cvc5.h header are for the purpose of eliminating warnings. This PR does not check for completeness of the documentation, and does not yet tweak the documentation to be nice, beautiful and consistent, which is postponed to future PRs. Configure with `--docs`, and then make. This will generate a `docs` directory in the build directory. The Sphinx documentation can be found at `build/docs/sphinx/index.html`. Doxygen documentation is only generated as xml under `build/docs/doxygen`. This PR further proposes a new style for copyright headers. If this style is approved, I will submit a PR to update the update_copyright.pl script. | |||
| 2021-04-01 | Refactor CLN dependency & Cleanup (#6251) | Gereon Kremer | |
| This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system. Also, it does a bit of cleanup. | |||
| 2021-03-27 | Refactor ANTLR3 dependency (#6202) | Gereon Kremer | |
| This PR refactors our first, and arguably most fragile, dependency. Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake). This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project. Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains. | |||
| 2021-03-23 | Removing unused build options and deprecated proof compile flag (#6195) | Haniel Barbosa | |
| 2021-03-20 | Generate cvc/Kind.java for the java API (#6143) | mudathirmahgoub | |
| PR changes: Refactor python/genkinds.py by separating parsing from file generation. Add java/genkinds.py to generate file Kind.java. Enable java API in ./configure.sh with "under development" warning. | |||
| 2021-03-10 | cmake: Fix optimization level for debug builds. (#6097) | Mathias Preiner | |
| Further cleans up some unused variables and moves the configuration of best to configure.sh. | |||
| 2021-03-08 | contrib: Do not use HOST env variable for cross-compilation host target. (#6078) | Mathias Preiner | |
| On some systems HOST is set by default to the host name. This commit adds a --host option for the get-antlr-3.4 and get-gmp-dev scripts. It further simplifies the machine type check in get-antlr-3.4 and updates the GMP version to 6.2.1. | |||
| 2021-03-02 | Remove obsolete dependency on CxxTest. (#6038) | Aina Niemetz | |
| 2021-03-02 | Add aarch64 (ARM64) cross-compile support. (#6033) | Mathias Preiner | |
| This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64. Fixes #1479 #5769. | |||
| 2021-03-01 | Make -Werror optional but enable it for CI. (#6032) | Mathias Preiner | |
| 2021-02-09 | cmake: Make Python3 default and improve toml error messages. (#5884) | Mathias Preiner | |
| ./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag. | |||
| 2021-02-04 | Clarifying documentation of `--static-binary` (#5844) | yoni206 | |
| The documentation regarding --static-binary is improved. | |||
| 2020-08-12 | Add option to only build library (#4801) | makaimann | |
| This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API. It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange. | |||
| 2020-07-17 | Support for using 'libedit' over 'readline' #4571 (#4579) | Andrew V. Jones | |
| Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> | |||
| 2020-07-17 | Integration of libpoly (#4679) | Gereon Kremer | |
| This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration. Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities. | |||
| 2020-07-02 | Remove SWIG bindings (#4683) | Andres Noetzli | |
| This commit removes support for SWIG bindings for the legacy API. The bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da and we are not planning on using SWIG for the Java API for the new API. | |||
| 2020-05-22 | Add support for SAT solver Kissat. (#4514) | Aina Niemetz | |
| 2020-03-31 | Switch to GitHub actions for CI (#4190) | Mathias Preiner | |
| Enable CI with GitHub actions, add macOS builds and disable Travis CI. | |||
| 2020-03-31 | Remove replay and use-theory options and idl (#4186) | Andrew Reynolds | |
| Towards disentangling Options / NodeManager / SmtEngine. This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work. The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it. The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging. It also removes the solver in src/theory/idl, which cannot be enabled after this commit. | |||
| 2020-02-26 | Remove portfolio leftovers (#3821) | Andres Noetzli | |
| Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio build but there were some leftovers. This commit removes them. | |||
| 2020-02-19 | Add Python bindings using Cython -- see below for more details (#2879) | makaimann | |
| 2019-11-16 | Add support for ThreadSanitizer instrumentation (#3467) | Andres Noetzli | |
| This commit adds support for compiling CVC4 with ThreadSanitizer instrumentation. This is useful for debugging issues when CVC4 is used in a multi-threaded context (e.g. #3292). | |||
| 2019-10-11 | Add support for UBSan instrumentation (#3382) | Andres Noetzli | |
| This commit adds support for compiling CVC4 with UBSan instrumentation. The commit also adds a dummy version of `AigBitblaster`. Previously, when CVC4 was built without ABC, `AigBitblaster` was not fully defined (the class was declared but the implementation was not being compiled). This lead to missing RTTI information when compiling with UBSan instrumentation. | |||
| 2019-10-07 | Build system: Add build type for incremental competition builds. (#3365) | Aina Niemetz | |
| Previously, competition builds for incremental tracks required to manually pass in -DCVC4_SMTCOMP_APPLICATION_TRACK as compiler flag. This introduces an additional build type for incremental competition builds to simplify configuration for such builds. | |||
| 2019-09-06 | Remove portfolio (#3236) | Andrew Reynolds | |
| 2019-08-08 | Fix issues with Ninja build system and add configure option. (#3166) | Mathias Preiner | |
| Adds option --ninja to configure.sh. | |||
| 2019-04-09 | Removing references to cvc4-bugs@... (#2945) | Haniel Barbosa | |
| 2018-12-17 | Configured for linking against drat2er (#2754) | Alex Ozdemir | |
| drat2er is a C/C++ project which includes support for * Checking DRAT proofs * Converting DRAT proofs to LRAT proofs * Converting DRAT proofs to ER proofs It does the first 2 by using drat-trim under the hood. I've modified our CMake configuration to allow drat2er to be linked into CVC4, and I added a contrib script. | |||
| 2018-11-08 | cmake: Add option to explicitely enable/disable static binaries. (#2698) | Mathias Preiner | |
| 2018-11-05 | configure.sh: Fix option parsing to match --help (#2611) | Andres Noetzli | |
| 2018-09-27 | cmake: Add CxxTest finder module to allow custom paths. (#2542) | Mathias Preiner | |
| 2018-09-25 | cmake: configure.sh wrapper: Removed unused option --gmp. | Aina Niemetz | |
| 2018-09-24 | cmake: Add program prefix option. (#2515) | Mathias Preiner | |
| 2018-09-22 | cmake: Add python3 option. | Mathias Preiner | |
| 2018-09-22 | cmake: Add more documentation, some fixes and cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: configure.sh wrapper: Use explicit build directory structure. | Aina Niemetz | |
| We don't create build directories for every build type (and configuration) anymore. The default build directory is now 'build' (created where you call the wrapper script from). Option --name allows to configure an individual name (and path) for the build directory. | |||
| 2018-09-22 | cmake: configure wrapper: Modify next steps message after configuration. | Mathias Preiner | |
| Since configure.sh is only a wrapper for cmake it prints all the messages from cmake. At the end we print the next steps after configuration. If configure.sh is used we add the info to also change into the build directory before calling make. | |||
| 2018-09-22 | cmake: Add support for cross-compiling for Windows. | Mathias Preiner | |
| 2018-09-22 | cmake: configure.sh wrapper: Fixes for sh. | Mathias Preiner | |
| 2018-09-22 | cmake: configure.sh wrapper: Add --name option. | Mathias Preiner | |
| 2018-09-22 | cmake: configure.sh wrapper: Add --prefix for install directory. | Mathias Preiner | |
| 2018-09-22 | cmake: Add make install rule. | Mathias Preiner | |
| 2018-09-22 | cmake: configure.sh wrapper: Fix handling of options with arguments. | Aina Niemetz | |
| 2018-09-22 | cmake: configure.sh wrapper: Removed env vars help text. | Aina Niemetz | |
| 2018-09-22 | cmake: configure.sh wrapper: Configurable build directory | Aina Niemetz | |
| 2018-09-22 | cmake: configure.sh wrapper: Create build dirs for configurations | Aina Niemetz | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
path: root/configure.sh
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback