mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
Merge pull request #937 from delcypher/cmake_git_version
[CMake] Support including Git hash and description into the build.
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
e2933350b2
|
|
@ -35,8 +35,8 @@ set(Z3_VERSION_MAJOR 4)
|
|||
set(Z3_VERSION_MINOR 5)
|
||||
set(Z3_VERSION_PATCH 1)
|
||||
set(Z3_VERSION_TWEAK 0)
|
||||
set(Z3_FULL_VERSION 0)
|
||||
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
|
||||
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
|
||||
message(STATUS "Z3 version ${Z3_VERSION}")
|
||||
|
||||
################################################################################
|
||||
|
|
@ -75,6 +75,64 @@ endif()
|
|||
################################################################################
|
||||
list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules")
|
||||
|
||||
################################################################################
|
||||
# Handle git hash and description
|
||||
################################################################################
|
||||
include(${CMAKE_SOURCE_DIR}/cmake/git_utils.cmake)
|
||||
macro(disable_git_describe)
|
||||
message(WARNING "Disabling INCLUDE_GIT_DESCRIBE")
|
||||
set(INCLUDE_GIT_DESCRIBE OFF CACHE BOOL "Include git describe output in version output" FORCE)
|
||||
endmacro()
|
||||
macro(disable_git_hash)
|
||||
message(WARNING "Disabling INCLUDE_GIT_HASH")
|
||||
set(INCLUDE_GIT_HASH OFF CACHE BOOL "Include git hash in version output" FORCE)
|
||||
unset(Z3GITHASH) # Used in configure_file()
|
||||
endmacro()
|
||||
option(INCLUDE_GIT_HASH "Include git hash in version output" ON)
|
||||
option(INCLUDE_GIT_DESCRIBE "Include git describe output in version output" ON)
|
||||
|
||||
set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git")
|
||||
if (EXISTS "${GIT_DIR}")
|
||||
# Try to make CMake configure depend on the current git HEAD so that
|
||||
# a re-configure is triggered when the HEAD changes.
|
||||
add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
|
||||
if (ADD_GIT_DEP_SUCCESS)
|
||||
if (INCLUDE_GIT_HASH)
|
||||
get_git_head_hash("${GIT_DIR}" Z3GITHASH)
|
||||
if (NOT Z3GITHASH)
|
||||
message(WARNING "Failed to get Git hash")
|
||||
disable_git_hash()
|
||||
endif()
|
||||
message(STATUS "Using Git hash in version output: ${Z3GITHASH}")
|
||||
# This mimics the behaviour of the old build system.
|
||||
string(APPEND Z3_FULL_VERSION_STR " ${Z3GITHASH}")
|
||||
else()
|
||||
message(STATUS "Not using Git hash in version output")
|
||||
unset(Z3GITHASH) # Used in configure_file()
|
||||
endif()
|
||||
if (INCLUDE_GIT_DESCRIBE)
|
||||
get_git_head_describe("${GIT_DIR}" Z3_GIT_DESCRIPTION)
|
||||
if (NOT Z3_GIT_DESCRIPTION)
|
||||
message(WARNING "Failed to get Git description")
|
||||
disable_git_describe()
|
||||
endif()
|
||||
message(STATUS "Using Git description in version output: ${Z3_GIT_DESCRIPTION}")
|
||||
# This mimics the behaviour of the old build system.
|
||||
string(APPEND Z3_FULL_VERSION_STR " ${Z3_GIT_DESCRIPTION}")
|
||||
else()
|
||||
message(STATUS "Not including git descrption in version")
|
||||
endif()
|
||||
else()
|
||||
message(WARNING "Failed to add git dependency.")
|
||||
disable_git_describe()
|
||||
disable_git_hash()
|
||||
endif()
|
||||
else()
|
||||
message(STATUS "Failed to find git directory.")
|
||||
disable_git_describe()
|
||||
disable_git_hash()
|
||||
endif()
|
||||
|
||||
################################################################################
|
||||
# Useful CMake functions/Macros
|
||||
################################################################################
|
||||
|
|
|
|||
|
|
@ -283,6 +283,8 @@ The following useful options can be passed to CMake whilst configuring.
|
|||
* ``INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings.
|
||||
* ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
|
||||
* ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
|
||||
* ``INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build.
|
||||
* ``INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build.
|
||||
|
||||
On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
|
||||
|
||||
|
|
|
|||
173
contrib/cmake/cmake/git_utils.cmake
Normal file
173
contrib/cmake/cmake/git_utils.cmake
Normal file
|
|
@ -0,0 +1,173 @@
|
|||
# add_git_dir_dependency(GIT_DIR SUCCESS_VAR)
|
||||
#
|
||||
# Adds a configure time dependency on the git directory such that if the HEAD
|
||||
# of the git directory changes CMake will be forced to re-run. This useful
|
||||
# for fetching the current git hash and including it in the build.
|
||||
#
|
||||
# `GIT_DIR` is the path to the git directory (i.e. the `.git` directory)
|
||||
# `SUCCESS_VAR` is the name of the variable to set. It will be set to TRUE
|
||||
# if the dependency was successfully added and FALSE otherwise.
|
||||
function(add_git_dir_dependency GIT_DIR SUCCESS_VAR)
|
||||
if (NOT "${ARGC}" EQUAL 2)
|
||||
message(FATAL_ERROR "Invalid number (${ARGC}) of arguments")
|
||||
endif()
|
||||
|
||||
if (NOT IS_ABSOLUTE "${GIT_DIR}")
|
||||
message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not an absolute path")
|
||||
endif()
|
||||
|
||||
if (NOT IS_DIRECTORY "${GIT_DIR}")
|
||||
message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not a directory")
|
||||
endif()
|
||||
|
||||
set(GIT_HEAD_FILE "${GIT_DIR}/HEAD")
|
||||
if (NOT EXISTS "${GIT_HEAD_FILE}")
|
||||
message(AUTHOR_WARNING "Git head file \"${GIT_HEAD_FILE}\" cannot be found")
|
||||
set(${SUCCESS_VAR} FALSE PARENT_SCOPE)
|
||||
return()
|
||||
endif()
|
||||
|
||||
# List of files in the git tree that CMake configuration should depend on
|
||||
set(GIT_FILE_DEPS "${GIT_HEAD_FILE}")
|
||||
|
||||
# Examine the HEAD and workout what additional dependencies there are.
|
||||
file(READ "${GIT_HEAD_FILE}" GIT_HEAD_DATA LIMIT 128)
|
||||
string(STRIP "${GIT_HEAD_DATA}" GIT_HEAD_DATA_STRIPPED)
|
||||
|
||||
if ("${GIT_HEAD_DATA_STRIPPED}" MATCHES "^ref:[ ]*(.+)$")
|
||||
# HEAD points at a reference.
|
||||
set(GIT_REF "${CMAKE_MATCH_1}")
|
||||
if (EXISTS "${GIT_DIR}/${GIT_REF}")
|
||||
# Unpacked reference. The file contains the commit hash
|
||||
# so add a dependency on this file so that if we stay on this
|
||||
# reference (i.e. branch) but change commit CMake will be forced
|
||||
# to reconfigure.
|
||||
list(APPEND GIT_FILE_DEPS "${GIT_DIR}/${GIT_REF}")
|
||||
elseif(EXISTS "${GIT_DIR}/packed-refs")
|
||||
# The ref must be packed (see `man git-pack-refs`).
|
||||
list(APPEND GIT_FILE_DEPS "${GIT_DIR}/packed-refs")
|
||||
else()
|
||||
# Fail
|
||||
message(AUTHOR_WARNING "Unhandled git reference")
|
||||
set(${SUCCESS_VAR} FALSE PARENT_SCOPE)
|
||||
return()
|
||||
endif()
|
||||
else()
|
||||
# Detached HEAD.
|
||||
# No other dependencies needed
|
||||
endif()
|
||||
|
||||
# FIXME:
|
||||
# This is the directory we will copy (via `configure_file()`) git files
|
||||
# into. This is a hack. It would be better to use the
|
||||
# `CMAKE_CONFIGURE_DEPENDS` directory property but that feature is not
|
||||
# available in CMake 2.8.12. So we use `configure_file()` to effectively
|
||||
# do the same thing. When the source file to `configure_file()` changes
|
||||
# it will trigger a re-run of CMake.
|
||||
set(GIT_CMAKE_FILES_DIR "${CMAKE_CURRENT_BINARY_DIR}/git_cmake_files")
|
||||
file(MAKE_DIRECTORY "${GIT_CMAKE_FILES_DIR}")
|
||||
|
||||
foreach (git_dependency ${GIT_FILE_DEPS})
|
||||
message(STATUS "Adding git dependency \"${git_dependency}\"")
|
||||
configure_file(
|
||||
"${git_dependency}"
|
||||
"${GIT_CMAKE_FILES_DIR}"
|
||||
COPYONLY
|
||||
)
|
||||
endforeach()
|
||||
|
||||
set(${SUCCESS_VAR} TRUE PARENT_SCOPE)
|
||||
endfunction()
|
||||
|
||||
# get_git_head_hash(GIT_DIR OUTPUT_VAR)
|
||||
#
|
||||
# Retrieve the current commit hash for a git working directory where `GIT_DIR`
|
||||
# is the `.git` directory in the root of the git working directory.
|
||||
#
|
||||
# `OUTPUT_VAR` should be the name of the variable to put the result in. If this
|
||||
# function fails then either a fatal error will be raised or `OUTPUT_VAR` will
|
||||
# contain a string with the suffix `NOTFOUND` which can be used in CMake `if()`
|
||||
# commands.
|
||||
function(get_git_head_hash GIT_DIR OUTPUT_VAR)
|
||||
if (NOT "${ARGC}" EQUAL 2)
|
||||
message(FATAL_ERROR "Invalid number of arguments")
|
||||
endif()
|
||||
if (NOT IS_DIRECTORY "${GIT_DIR}")
|
||||
message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory")
|
||||
endif()
|
||||
if (NOT IS_ABSOLUTE "${GIT_DIR}")
|
||||
message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path")
|
||||
endif()
|
||||
find_package(Git)
|
||||
if (NOT Git_FOUND)
|
||||
set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE)
|
||||
return()
|
||||
endif()
|
||||
get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY)
|
||||
execute_process(
|
||||
COMMAND
|
||||
"${GIT_EXECUTABLE}"
|
||||
"rev-parse"
|
||||
"-q" # Quiet
|
||||
"HEAD"
|
||||
WORKING_DIRECTORY
|
||||
"${GIT_WORKING_DIR}"
|
||||
RESULT_VARIABLE
|
||||
GIT_EXIT_CODE
|
||||
OUTPUT_VARIABLE
|
||||
Z3_GIT_HASH
|
||||
OUTPUT_STRIP_TRAILING_WHITESPACE
|
||||
)
|
||||
if (NOT "${GIT_EXIT_CODE}" EQUAL 0)
|
||||
message(WARNING "Failed to execute git")
|
||||
set(${OUTPUT_VAR} NOTFOUND PARENT_SCOPE)
|
||||
return()
|
||||
endif()
|
||||
set(${OUTPUT_VAR} "${Z3_GIT_HASH}" PARENT_SCOPE)
|
||||
endfunction()
|
||||
|
||||
# get_git_head_describe(GIT_DIR OUTPUT_VAR)
|
||||
#
|
||||
# Retrieve the output of `git describe` for a git working directory where
|
||||
# `GIT_DIR` is the `.git` directory in the root of the git working directory.
|
||||
#
|
||||
# `OUTPUT_VAR` should be the name of the variable to put the result in. If this
|
||||
# function fails then either a fatal error will be raised or `OUTPUT_VAR` will
|
||||
# contain a string with the suffix `NOTFOUND` which can be used in CMake `if()`
|
||||
# commands.
|
||||
function(get_git_head_describe GIT_DIR OUTPUT_VAR)
|
||||
if (NOT "${ARGC}" EQUAL 2)
|
||||
message(FATAL_ERROR "Invalid number of arguments")
|
||||
endif()
|
||||
if (NOT IS_DIRECTORY "${GIT_DIR}")
|
||||
message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory")
|
||||
endif()
|
||||
if (NOT IS_ABSOLUTE "${GIT_DIR}")
|
||||
message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path")
|
||||
endif()
|
||||
find_package(Git)
|
||||
if (NOT Git_FOUND)
|
||||
set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE)
|
||||
return()
|
||||
endif()
|
||||
get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY)
|
||||
execute_process(
|
||||
COMMAND
|
||||
"${GIT_EXECUTABLE}"
|
||||
"describe"
|
||||
"--long"
|
||||
WORKING_DIRECTORY
|
||||
"${GIT_WORKING_DIR}"
|
||||
RESULT_VARIABLE
|
||||
GIT_EXIT_CODE
|
||||
OUTPUT_VARIABLE
|
||||
Z3_GIT_DESCRIPTION
|
||||
OUTPUT_STRIP_TRAILING_WHITESPACE
|
||||
)
|
||||
if (NOT "${GIT_EXIT_CODE}" EQUAL 0)
|
||||
message(WARNING "Failed to execute git")
|
||||
set(${OUTPUT_VAR} NOTFOUND PARENT_SCOPE)
|
||||
return()
|
||||
endif()
|
||||
set(${OUTPUT_VAR} "${Z3_GIT_DESCRIPTION}" PARENT_SCOPE)
|
||||
endfunction()
|
||||
|
|
@ -3,7 +3,9 @@ if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
|
|||
${z3_polluted_tree_msg}
|
||||
)
|
||||
endif()
|
||||
configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY)
|
||||
|
||||
set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"")
|
||||
configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h)
|
||||
|
||||
z3_add_component(util
|
||||
SOURCES
|
||||
|
|
|
|||
8
src/util/version.h.cmake.in
Normal file
8
src/util/version.h.cmake.in
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
// automatically generated file.
|
||||
#define Z3_MAJOR_VERSION @Z3_VERSION_MAJOR@
|
||||
#define Z3_MINOR_VERSION @Z3_VERSION_MINOR@
|
||||
#define Z3_BUILD_NUMBER @Z3_VERSION_PATCH@
|
||||
#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@
|
||||
|
||||
#define Z3_FULL_VERSION @Z3_FULL_VERSION@
|
||||
#cmakedefine Z3GITHASH @Z3GITHASH@
|
||||
Loading…
Reference in a new issue