Skip to content

Commit 15af645

Browse files
author
Thomas Kiley
authored
Merge pull request #1426 from reuk/reuk/download-project
More robust inclusion of sat libraries
2 parents de493ae + 88c2f9c commit 15af645

6 files changed

+233
-101
lines changed
+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# Distributed under the OSI-approved MIT License. See accompanying
2+
# file LICENSE or https://github.com/Crascit/DownloadProject for details.
3+
4+
cmake_minimum_required(VERSION 2.8.2)
5+
6+
project(${DL_ARGS_PROJ}-download NONE)
7+
8+
include(ExternalProject)
9+
ExternalProject_Add(${DL_ARGS_PROJ}-download
10+
${DL_ARGS_UNPARSED_ARGUMENTS}
11+
SOURCE_DIR "${DL_ARGS_SOURCE_DIR}"
12+
BINARY_DIR "${DL_ARGS_BINARY_DIR}"
13+
CONFIGURE_COMMAND ""
14+
BUILD_COMMAND ""
15+
INSTALL_COMMAND ""
16+
TEST_COMMAND ""
17+
)

cmake/DownloadProject.cmake

+183
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
# Distributed under the OSI-approved MIT License. See accompanying
2+
# file LICENSE or https://github.com/Crascit/DownloadProject for details.
3+
#
4+
# MODULE: DownloadProject
5+
#
6+
# PROVIDES:
7+
# download_project( PROJ projectName
8+
# [PREFIX prefixDir]
9+
# [DOWNLOAD_DIR downloadDir]
10+
# [SOURCE_DIR srcDir]
11+
# [BINARY_DIR binDir]
12+
# [QUIET]
13+
# ...
14+
# )
15+
#
16+
# Provides the ability to download and unpack a tarball, zip file, git repository,
17+
# etc. at configure time (i.e. when the cmake command is run). How the downloaded
18+
# and unpacked contents are used is up to the caller, but the motivating case is
19+
# to download source code which can then be included directly in the build with
20+
# add_subdirectory() after the call to download_project(). Source and build
21+
# directories are set up with this in mind.
22+
#
23+
# The PROJ argument is required. The projectName value will be used to construct
24+
# the following variables upon exit (obviously replace projectName with its actual
25+
# value):
26+
#
27+
# projectName_SOURCE_DIR
28+
# projectName_BINARY_DIR
29+
#
30+
# The SOURCE_DIR and BINARY_DIR arguments are optional and would not typically
31+
# need to be provided. They can be specified if you want the downloaded source
32+
# and build directories to be located in a specific place. The contents of
33+
# projectName_SOURCE_DIR and projectName_BINARY_DIR will be populated with the
34+
# locations used whether you provide SOURCE_DIR/BINARY_DIR or not.
35+
#
36+
# The DOWNLOAD_DIR argument does not normally need to be set. It controls the
37+
# location of the temporary CMake build used to perform the download.
38+
#
39+
# The PREFIX argument can be provided to change the base location of the default
40+
# values of DOWNLOAD_DIR, SOURCE_DIR and BINARY_DIR. If all of those three arguments
41+
# are provided, then PREFIX will have no effect. The default value for PREFIX is
42+
# CMAKE_BINARY_DIR.
43+
#
44+
# The QUIET option can be given if you do not want to show the output associated
45+
# with downloading the specified project.
46+
#
47+
# In addition to the above, any other options are passed through unmodified to
48+
# ExternalProject_Add() to perform the actual download, patch and update steps.
49+
# The following ExternalProject_Add() options are explicitly prohibited (they
50+
# are reserved for use by the download_project() command):
51+
#
52+
# CONFIGURE_COMMAND
53+
# BUILD_COMMAND
54+
# INSTALL_COMMAND
55+
# TEST_COMMAND
56+
#
57+
# Only those ExternalProject_Add() arguments which relate to downloading, patching
58+
# and updating of the project sources are intended to be used. Also note that at
59+
# least one set of download-related arguments are required.
60+
#
61+
# If using CMake 3.2 or later, the UPDATE_DISCONNECTED option can be used to
62+
# prevent a check at the remote end for changes every time CMake is run
63+
# after the first successful download. See the documentation of the ExternalProject
64+
# module for more information. It is likely you will want to use this option if it
65+
# is available to you. Note, however, that the ExternalProject implementation contains
66+
# bugs which result in incorrect handling of the UPDATE_DISCONNECTED option when
67+
# using the URL download method or when specifying a SOURCE_DIR with no download
68+
# method. Fixes for these have been created, the last of which is scheduled for
69+
# inclusion in CMake 3.8.0. Details can be found here:
70+
#
71+
# https://gitlab.kitware.com/cmake/cmake/commit/bdca68388bd57f8302d3c1d83d691034b7ffa70c
72+
# https://gitlab.kitware.com/cmake/cmake/issues/16428
73+
#
74+
# If you experience build errors related to the update step, consider avoiding
75+
# the use of UPDATE_DISCONNECTED.
76+
#
77+
# EXAMPLE USAGE:
78+
#
79+
# include(DownloadProject)
80+
# download_project(PROJ googletest
81+
# GIT_REPOSITORY https://github.com/google/googletest.git
82+
# GIT_TAG master
83+
# UPDATE_DISCONNECTED 1
84+
# QUIET
85+
# )
86+
#
87+
# add_subdirectory(${googletest_SOURCE_DIR} ${googletest_BINARY_DIR})
88+
#
89+
#========================================================================================
90+
91+
92+
set(_DownloadProjectDir "${CMAKE_CURRENT_LIST_DIR}")
93+
94+
include(CMakeParseArguments)
95+
96+
function(download_project)
97+
98+
set(options QUIET)
99+
set(oneValueArgs
100+
PROJ
101+
PREFIX
102+
DOWNLOAD_DIR
103+
SOURCE_DIR
104+
BINARY_DIR
105+
# Prevent the following from being passed through
106+
CONFIGURE_COMMAND
107+
BUILD_COMMAND
108+
INSTALL_COMMAND
109+
TEST_COMMAND
110+
)
111+
set(multiValueArgs "")
112+
113+
cmake_parse_arguments(DL_ARGS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
114+
115+
# Hide output if requested
116+
if (DL_ARGS_QUIET)
117+
set(OUTPUT_QUIET "OUTPUT_QUIET")
118+
else()
119+
unset(OUTPUT_QUIET)
120+
message(STATUS "Downloading/updating ${DL_ARGS_PROJ}")
121+
endif()
122+
123+
# Set up where we will put our temporary CMakeLists.txt file and also
124+
# the base point below which the default source and binary dirs will be.
125+
# The prefix must always be an absolute path.
126+
if (NOT DL_ARGS_PREFIX)
127+
set(DL_ARGS_PREFIX "${CMAKE_BINARY_DIR}")
128+
else()
129+
get_filename_component(DL_ARGS_PREFIX "${DL_ARGS_PREFIX}" ABSOLUTE
130+
BASE_DIR "${CMAKE_CURRENT_BINARY_DIR}")
131+
endif()
132+
if (NOT DL_ARGS_DOWNLOAD_DIR)
133+
set(DL_ARGS_DOWNLOAD_DIR "${DL_ARGS_PREFIX}/${DL_ARGS_PROJ}-download")
134+
endif()
135+
136+
# Ensure the caller can know where to find the source and build directories
137+
if (NOT DL_ARGS_SOURCE_DIR)
138+
set(DL_ARGS_SOURCE_DIR "${DL_ARGS_PREFIX}/${DL_ARGS_PROJ}-src")
139+
endif()
140+
if (NOT DL_ARGS_BINARY_DIR)
141+
set(DL_ARGS_BINARY_DIR "${DL_ARGS_PREFIX}/${DL_ARGS_PROJ}-build")
142+
endif()
143+
set(${DL_ARGS_PROJ}_SOURCE_DIR "${DL_ARGS_SOURCE_DIR}" PARENT_SCOPE)
144+
set(${DL_ARGS_PROJ}_BINARY_DIR "${DL_ARGS_BINARY_DIR}" PARENT_SCOPE)
145+
146+
# The way that CLion manages multiple configurations, it causes a copy of
147+
# the CMakeCache.txt to be copied across due to it not expecting there to
148+
# be a project within a project. This causes the hard-coded paths in the
149+
# cache to be copied and builds to fail. To mitigate this, we simply
150+
# remove the cache if it exists before we configure the new project. It
151+
# is safe to do so because it will be re-generated. Since this is only
152+
# executed at the configure step, it should not cause additional builds or
153+
# downloads.
154+
file(REMOVE "${DL_ARGS_DOWNLOAD_DIR}/CMakeCache.txt")
155+
156+
# Create and build a separate CMake project to carry out the download.
157+
# If we've already previously done these steps, they will not cause
158+
# anything to be updated, so extra rebuilds of the project won't occur.
159+
# Make sure to pass through CMAKE_MAKE_PROGRAM in case the main project
160+
# has this set to something not findable on the PATH.
161+
configure_file("${_DownloadProjectDir}/DownloadProject.CMakeLists.cmake.in"
162+
"${DL_ARGS_DOWNLOAD_DIR}/CMakeLists.txt")
163+
execute_process(COMMAND ${CMAKE_COMMAND} -G "${CMAKE_GENERATOR}"
164+
-D "CMAKE_MAKE_PROGRAM:FILE=${CMAKE_MAKE_PROGRAM}"
165+
.
166+
RESULT_VARIABLE result
167+
${OUTPUT_QUIET}
168+
WORKING_DIRECTORY "${DL_ARGS_DOWNLOAD_DIR}"
169+
)
170+
if(result)
171+
message(FATAL_ERROR "CMake step for ${DL_ARGS_PROJ} failed: ${result}")
172+
endif()
173+
execute_process(COMMAND ${CMAKE_COMMAND} --build .
174+
RESULT_VARIABLE result
175+
${OUTPUT_QUIET}
176+
WORKING_DIRECTORY "${DL_ARGS_DOWNLOAD_DIR}"
177+
)
178+
if(result)
179+
message(FATAL_ERROR "Build step for ${DL_ARGS_PROJ} failed: ${result}")
180+
endif()
181+
182+
endfunction()
183+

scripts/glucose_CMakeLists.txt

+1-19
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,12 @@
1-
cmake_minimum_required(VERSION 3.2)
2-
31
# CBMC only uses part of glucose.
42
# This CMakeLists is designed to build just the parts that are needed.
53

6-
set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
7-
set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
8-
set(CMAKE_BUILD_TYPE RelWithDebInfo)
9-
104
add_library(glucose-condensed
115
simp/SimpSolver.cc
126
core/Solver.cc
137
)
148

159
target_include_directories(glucose-condensed
1610
PUBLIC
17-
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
18-
$<INSTALL_INTERFACE:include>
19-
)
20-
21-
install(TARGETS glucose-condensed EXPORT glucose-condensed-targets
22-
LIBRARY DESTINATION lib
23-
ARCHIVE DESTINATION lib
24-
RUNTIME DESTINATION bin
25-
INCLUDES DESTINATION include
11+
${CMAKE_CURRENT_SOURCE_DIR}
2612
)
27-
28-
install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
29-
30-
install(EXPORT glucose-condensed-targets DESTINATION lib/cmake/glucose-condensed)

scripts/minisat2_CMakeLists.txt

+2-21
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,14 @@
1-
cmake_minimum_required(VERSION 3.2)
2-
31
# CBMC only uses part of minisat2.
42
# This CMakeLists is designed to build just the parts that are needed.
53

6-
set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
7-
set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
8-
set(CMAKE_BUILD_TYPE RelWithDebInfo)
9-
104
add_library(minisat2-condensed
115
minisat/simp/SimpSolver.cc
126
minisat/core/Solver.cc
137
)
148

15-
set(CBMC_INCLUDE_DIR "" CACHE PATH "The path to CBMC util headers")
16-
179
target_include_directories(minisat2-condensed
1810
PUBLIC
19-
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
20-
$<BUILD_INTERFACE:${CBMC_INCLUDE_DIR}>
21-
$<INSTALL_INTERFACE:include>
11+
${CMAKE_CURRENT_SOURCE_DIR}
2212
)
2313

24-
install(TARGETS minisat2-condensed EXPORT minisat-condensed-targets
25-
LIBRARY DESTINATION lib
26-
ARCHIVE DESTINATION lib
27-
RUNTIME DESTINATION bin
28-
INCLUDES DESTINATION include
29-
)
30-
31-
install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
32-
33-
install(EXPORT minisat-condensed-targets DESTINATION lib/cmake/minisat-condensed)
14+
target_link_libraries(minisat2-condensed util)

src/CMakeLists.txt

-57
Original file line numberDiff line numberDiff line change
@@ -82,63 +82,6 @@ macro(add_if_library target name)
8282
endif()
8383
endmacro(add_if_library)
8484

85-
# EXTERNAL PROJECTS
86-
include(ExternalProject)
87-
set(extern_location ${CMAKE_CURRENT_BINARY_DIR}/extern)
88-
89-
set(extern_include_directory ${extern_location}/include)
90-
file(MAKE_DIRECTORY ${extern_include_directory})
91-
92-
################################################################################
93-
94-
set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
95-
96-
# minisat download: This downloads minisat2, then patches it. Then, it
97-
# injects a minimal CMakeLists.txt so that we can build just the bits we
98-
# actually want, without having to update the provided makefile.
99-
100-
ExternalProject_Add(minisat2-extern
101-
PREFIX ${extern_location}
102-
URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
103-
PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
104-
COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
105-
CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR> -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR}
106-
BUILD_BYPRODUCTS ${minisat_lib}
107-
)
108-
109-
add_library(minisat2-condensed STATIC IMPORTED)
110-
set_target_properties(minisat2-condensed PROPERTIES
111-
IMPORTED_LOCATION ${minisat_lib}
112-
INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
113-
)
114-
add_dependencies(minisat2-condensed minisat2-extern)
115-
116-
################################################################################
117-
118-
set(glucose_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}glucose-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
119-
120-
# glucose download: This downloads glucose, then patches it. Then, it
121-
# injects a minimal CMakeLists.txt so that we can build just the bits we
122-
# actually want, without having to update the provided makefile.
123-
124-
ExternalProject_Add(glucose-extern
125-
PREFIX ${extern_location}
126-
URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
127-
PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose-syrup-patch
128-
COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
129-
CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
130-
BUILD_BYPRODUCTS ${glucose_lib}
131-
)
132-
133-
add_library(glucose-condensed STATIC IMPORTED)
134-
set_target_properties(glucose-condensed PROPERTIES
135-
IMPORTED_LOCATION ${glucose_lib}
136-
INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
137-
)
138-
add_dependencies(glucose-condensed glucose-extern)
139-
140-
################################################################################
141-
14285
# Override add_executable to automatically sign the target on OSX.
14386
function(add_executable name)
14487
_add_executable(${name} ${ARGN})

src/solvers/CMakeLists.txt

+30-4
Original file line numberDiff line numberDiff line change
@@ -65,17 +65,43 @@ list(REMOVE_ITEM sources
6565

6666
add_library(solvers ${sources} ${headers})
6767

68+
include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
69+
6870
if("${sat_impl}" STREQUAL "minisat2")
6971
message(STATUS "Building solvers with minisat2")
72+
73+
download_project(PROJ minisat2
74+
URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
75+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
76+
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
77+
)
78+
79+
add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
80+
81+
target_compile_definitions(solvers PUBLIC
82+
SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
83+
)
84+
7085
target_sources(solvers PRIVATE ${minisat2_source})
71-
add_dependencies(solvers minisat2-extern)
72-
target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
86+
7387
target_link_libraries(solvers minisat2-condensed)
7488
elseif("${sat_impl}" STREQUAL "glucose")
7589
message(STATUS "Building solvers with glucose")
90+
91+
download_project(PROJ glucose
92+
URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
93+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
94+
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
95+
)
96+
97+
add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
98+
99+
target_compile_definitions(solvers PUBLIC
100+
SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
101+
)
102+
76103
target_sources(solvers PRIVATE ${glucose_source})
77-
add_dependencies(solvers glucose-extern)
78-
target_compile_definitions(solvers PUBLIC SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
104+
79105
target_link_libraries(solvers glucose-condensed)
80106
endif()
81107

0 commit comments

Comments
 (0)