| Age | Commit message (Collapse) | Author |
|---|
|
This commit adds a check for CryptoMiniSat's static dependencies when configuring CryptoMiniSat. It changes a build-time failure into a configure-time failure.
`find_library` in CMake > 3.18 supports `REQUIRED`; as `cvc5` targets 3.10, I've implemented a check for what `find_library` returns.
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
Currently, the CLN `CONFIGURE_COMMAND` chains multiple commands using
`&&` but this does not seem to work with CMake 3.20.4 and CMake 3.19.7
and is also not the recommended way of doing it. The commit fixes the
issue by using additional `COMMAND`s and also switches to using the
CMake's `chdir` instead of `cd`.
|
|
This commit changes the output of our configuration to show which
dependencies are being built as part of the cvc5 build. For example:
```
ABC : off
CryptoMiniSat : off
GLPK : off
Kissat : off
LibPoly : on (local)
CoCoALib : off
Build libcvc5 only : off
MP library : gmp (system)
Editline : off
```
Indicates that `LibPoly` was not found in the system and is thus built
as part of the cvc5 build and GMP was found in the system.
|
|
Newer compilers, such as GCC 11, default to C++17. CoCoA does not
compile with C++17 and its check for the C++ version used by the
compiler does not take into account newer C++ versions. As a result,
building CoCoA using `--auto-download` fails with GCC 11. This commit
adds a patch that makes the test in CoCoA take into account compilers
that default to C++17 or newer.
|
|
On some platforms, autotools installs ANTLR3's libraries into lib but
CMAKE_INSTALL_LIBDIR is set to lib64 (e.g., Fedora 33). This commit
sets --libdir to force autotools to install the library into the
directory specified by CMAKE_INSTALL_LIBDIR.
|
|
On 64-bit openSUSE (and maybe other distributions), the default install directory for static libraries is `lib64` *not* `lib`. This has an impact on cvc5 when it is automatically building CMS (e.g., with `./configure.sh --cryptominisat --auto-download`): CMS adheres to the default value of `CMAKE_INSTALL_LIBDIR` to work out where to install the library files (so `lib64` on openSUSE), which fails when cvc5 tries to find these in `lib`.
Without this change, the build fails as follows:
```
<snip>
src/CMakeFiles/cvc5.dir/theory/type_enumerator.cpp.o -Wl,-rpath,:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: deps/lib/libcadical.a deps/lib/libcryptominisat5.a ../deps/install/lib64/libglpk.a deps/lib/libpicpolyxx.a /usr/lib64/libgmp.so deps/lib/libpicpoly.a /usr/lib64/libgmp.so && :
/usr/lib64/gcc/x86_64-suse-linux/11/../../../../x86_64-suse-linux/bin/ld: cannot find deps/lib/libcryptominisat5.a: No such file or directory
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
```
and where:
```
avj@platypus ~/clones/cvc5/master/build$ find . -iname "libcryptominisat5.a"
./deps/src/CryptoMiniSat-EP-build/lib/libcryptominisat5.a
./deps/lib64/libcryptominisat5.a
```
(notice: `lib64` in the second path!)
This commit fixes this discrepancy to ensure that cvc5 checks for CMS on `CMAKE_INSTALL_LIBDIR` as well.
**Note**: `CMAKE_INSTALL_LIBDIR` comes from `GNUInstallDirs`, and this is `include`'d in cvc5's top-level `CMakeLists.txt`
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
On 64-bit openSUSE (and maybe other distributions), the default install directory for static libraries is `lib64` *not* `lib`. This has an impact on cvc5 when it is automatically building ANTLR3: ANTLR3 follows the system-wide default of `lib64`, which fails when cvc5 tries to find these in `lib`.
Without this change, the build fails as follows:
```
<snip>
src/parser/CMakeFiles/cvc5parser.dir/smt2/Smt2Parser.c.o -Wl,-rpath,/home/avj/clones/cvc5/lib64_cms/build/src:::::::::::::::::::::::: src/libcvc5.so.1 deps/lib/libantlr3c.a && :
/usr/lib64/gcc/x86_64-suse-linux/11/../../../../x86_64-suse-linux/bin/ld: cannot find deps/lib/libantlr3c.a: No such file or directory
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
```
and where:
```
avj@platypus ~/clones/cvc5/lib64_cms/build$ find . -iname "libantlr3c.a"
./deps/src/ANTLR3-EP-runtime/.libs/libantlr3c.a
./deps/lib64/libantlr3c.a
```
(notice: `lib64` in the second path!)
This commit fixes this discrepancy to ensure that cvc5 checks for ANTLR3 on `CMAKE_INSTALL_LIBDIR`, which matches that `autotools` will use.
**Note**: `CMAKE_INSTALL_LIBDIR` comes from `GNUInstallDirs`, and this is `include`'d in cvc5's top-level `CMakeLists.txt`
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
With CMake 3.11 and later, `<DOWNLOAD_DIR>` is substituted in
`ExternalProject_Add` but not in older versions [0]. To maintain
compatibility with older versions of CMake, this commit changes
`ExternalProject_Add` to use `<DOWNLOADED_FILE>` instead, which is both
nicer and substituted in older versions of CMake.
[0] https://cmake.org/cmake/help/latest/release/3.11.html#modules
|
|
When building cvc5 on macOS for M1 natively, ANTLR's version of
`config.sub` does not recognize `aarch64-apple-darwin20.5.0`. This
commit fixes that issue by downloading the latest version of
`config.sub` (similar to what we are already doing for `config.guess`).
The commit also updates the URLs for `config.guess` and `config.sub` to
the URLs recommended in the files themselves. The commit also does some
minor cleanup/simplifications of the commands for building ANTLR.
|
|
* Fix CaDiCaL auto-download on macOS
If we are auto-downloading CaDiCaL, we are manually instantiating its makefile.
To do that, we use `CMAKE_CXX_COMPILER` for the compiler and assemble some
flags. However, we are missing the platform dependent flags. Specifically, we
need to set `-isysroot` on macOS to make sure that the header files are found
because they are not at /usr/include on newer versions of Apple's XCode [0].
Unfortunately, I could not find a CMake variable with the platform specific
flags. They are assembled here [1]. To solve this problem, the commit checks if
`CMAKE_OSX_SYSROOT` is set and adds a corresponding compiler flag if it is.
[0] https://developer.apple.com/documentation/xcode-release-notes/xcode-10-release-notes
[1] https://github.com/Kitware/CMake/blob/d60d6c269ae7ad15adbb82028e9ab50290db2a2b/Source/cmLocalGenerator.cxx#L1900-L1923
|
|
As mentioned in #6822, we are currently printing an incorrect message if CaDiCaL or SymFPU are not found but auto-download is disabled. This PR fixes this issue.
|
|
This commit adds the following new code coverage targets:
- coverage-reset: Resets the code coverage counters
- coverage: Generates code coverage report for all cvc5 executions since the
last coverage-reset
- coverage-test: This was previously the coverage target that runs the
tests and generates the coverage report (as used for
nightlies).
By using `make coverage-reset` and `make coverage` it is now possible to
generate coverage reports for arbitrary executions of cvc5.
|
|
|
|
The following commit made our libpoly patch for our Windows builds
obsolete:
https://github.com/SRI-CSL/libpoly/commit/ce7e620c54bd907200ce8b11812d123bf5f4ec8e
This resulted in our build getting stuck because it detected that the
patch had already been applied and was prompting the user what to do.
This commit removes that patch file and the corresponding command.
|
|
The Windows version of CaDiCaL does not require the `sys/resource.h`
file, so this commit removes that check. It does, however, require
linking against the Process Status API (psapi), because of a call to
`GetProcessMemoryInfo()`, so this commit adds that dependency for
Windows builds.
|
|
This PR updates to the latest version of libpoly, which has a memory leak fixed.
|
|
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.
|
|
This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.
This PR is a piece of this old one (#5657) which I am closing and splitting up.
|
|
|
|
This PR updates to the most recent version of libpoly which fixes some memory leaks.
|
|
PR changes:
Add Solver.java and relation JNI c files
Update FindJUnit to download JUnit5
Add Java unit tests
|
|
|
|
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
|
|
This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)
|
|
This PR adds the dependency of the CaDiCaL cmake target on the external project CaDiCaL-EP if it is not found in the system.
|
|
(#6417)
This will look for already downloaded dependencies in the build
directory and therefore will not require --auto-download if the
dependencies were already downloaded in a previous build.
|
|
This PR makes sure that our build of libpoly works on systems without GMP: by passing the paths to GMP we use ourselves to libpoly, we make sure libpoly always has a suitable version of GMP.
Also, we make libpoly somewhat faster to build by disabling tests.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
Addtionally adds checks for required documentation modules.
|
|
ANTLR3_COMMAND was using a fixed path instead of relying on the
ANTLR3_JAR variable. If the ANTLR3 JAR was found on the system (for
example due to an existing deps folder at the root of the CVC4
folder), then the command would fail because the JAR was not at the
expected location. This commit changes the command to use the variable
and prints the location of the JAR file to make debugging easier.
|
|
This PR fixes a linker issue with libpoly and static builds where Poly and GMP would be linked against in the wrong order.
|
|
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.
|
|
This PR fixes the libpoly build: it naively removed the test/ folder from the source directory to save on cache size.
It also uses the recently published 0.1.9 release of libpoly.
Fixes #4706.
|
|
|
|
|
|
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.
|
|
|
|
This PR avoids output redirection by replacing sed + redirect with copy + in-place sed.
Using output redirects can cause problems if the cmake output itself is redirected as well.
This should fix the current nightly failure.
|
|
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.
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
This PR refactors how we obtain, build and use the external SAT solvers used by CVC4: CaDiCaL, CryptoMiniSat and Kissat.
All three contrib scripts are removed and instead an external project is integrated into the cmake find scripts.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
This PR enables us to build gtest ourselves if it is not already installed.
|
|
|
|
As title; attempts to correct #6224.
Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com
|
|
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.
|
|
|
|
This PR further decouples LFSC from the remaining build system, but makes it more convenient to use at the same time.
The contrib/get-lfsc-checker script is now completely standalone and installs LFSC and the necessary signatures to deps/, as well as wrapper scripts to conveniently run lfscc from there and directly check cvc4 proofs.
The goal would be to automatically use LFSC in our regressions as well.
|
|
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.
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
