diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-24 16:07:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 10:07:15 -0500 |
| commit | 31bba4ba83354f41c756e9800489672ff1c9711c (patch) | |
| tree | a9a7d07d93b6e80d4b6c9e273b3f3c1ebdb2d4c6 /cmake | |
| parent | 34798fb86eabe7b9aaff86be23a7a3428ebfc957 (diff) | |
Refactor our integration of LFSC (#6201)
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.
Diffstat (limited to 'cmake')
| -rw-r--r-- | cmake/FindLFSC.cmake | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index 00a7a7d18..03b96d186 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -13,17 +13,25 @@ # LFSC_INCLUDE_DIR - the LFSC include directory # LFSC_LIBRARIES - Libraries needed to use LFSC -find_program(LFSC_BINARY NAMES lfscc) -find_path(LFSC_INCLUDE_DIR NAMES lfscc.h) -find_library(LFSC_LIBRARIES NAMES lfscc) +find_program(LFSC_BINARY + NAMES lfscc + PATHS ${CMAKE_SOURCE_DIR}/deps/bin +) +find_path(LFSC_INCLUDE_DIR + NAMES lfscc.h + PATHS ${CMAKE_SOURCE_DIR}/deps/include +) +find_library(LFSC_LIBRARIES + NAMES lfscc + PATHS ${CMAKE_SOURCE_DIR}/deps/lib +) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(LFSC - DEFAULT_MSG - LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES) + QUIET + LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES) mark_as_advanced(LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES) if(LFSC_FOUND) - message(STATUS "Found LFSC include dir: ${LFSC_INCLUDE_DIR}") - message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}") + message(STATUS "Found LFSC: ${LFSC_BINARY}") endif() |