Creating library archive with all components #7567
Conversation
esteffin
requested review from
a team,
NlightNFotis,
thomasspriggs,
TGWDB and
peterschrammel
as code owners
src/libcprover-cpp/CMakeLists.txt
Outdated
| COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/aggregate_dependencies.sh" "${CMAKE_AR}" "$<TARGET_FILE:cprover-api-cpp>" "${DEPENDENCY_TARGETS}" | ||
| WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}") | ||
|
|
||
| set(lib_version 153) |
There was a problem hiding this comment.
Enrico says remove this.
| println!("cargo:rustc-link-lib=static=goto-symex"); | ||
| println!("cargo:rustc-link-lib=static=pointer-analysis"); | ||
| for solver_lib in solver_libs { | ||
| println!("cargo:rustc-link-lib=static={}", solver_lib); |
There was a problem hiding this comment.
I'm not sure if this bit is correct - do we package in libminisat and cadical in the libcprover we're building?
(Probably, it might be a dependency of solvers/ in any case, but can we check before we merge this?
There was a problem hiding this comment.
(Okay, answering my own question here - it seems that we're building without issues, at least on the minisat front https://github.com/diffblue/cbmc/actions/runs/4293367669/jobs/7480953774)
Still, I would be a bit apprehensive to remove this for loop. Can we at least comment it out so that we may re-introduce it if we find we need it for radical?
There was a problem hiding this comment.
The SAT solvers (dependency of the solver target) are added to the final API library.
Specifically they are gathered at line 25 of src/libcprover-cpp/CMakeLists.txt when doing get_target_property(LIBRARY_DEPENDENCIES solvers LINK_LIBRARIES), and added afterwards.
For this reason they can be removed from the RUST side.
CBMC is compiled as a collection of static libraries, one per sub-module. This commits add a merging of most submodules into a final libcprover.<version>.a, so that it can be installed and used alone (without requiring its sub-module dependencies).
esteffin
force-pushed
the
esteffin/creating-public-archive-with-all-components
branch
from
5cc5b62 to
cf4817f
Compare
esteffin
deleted the
esteffin/creating-public-archive-with-all-components
branch
CBMC is compiled as a collection of static libraries, one per sub-module.
This PR adds a merging step of most submodules into a final
libcprover.<version>.a, so that it can be installed and used alone (without requiring its sub-module dependencies).