Add new versioning scheme (#7253)

This introduces a new versioning mechanism that allows for better automation.

11 files changed, 28 insertions, 154 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1dd005dd7..67347bbf4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1308,7 +1308,7 @@ target_link_libraries(cvc5-obj PUBLIC $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECT
 # add_dependencies() is necessary for cmake versions before 3.21
 add_dependencies(cvc5-obj cvc5base cvc5context)
 # Add libcvc5 dependencies for generated sources.
-add_dependencies(cvc5-obj gen-expr gen-gitinfo gen-options gen-tags gen-theory)
+add_dependencies(cvc5-obj gen-expr gen-versioninfo gen-options gen-tags gen-theory)
 
 # Link the shared library
 add_library(cvc5-shared SHARED)
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 95831f33d..d6759ba6e 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -130,13 +130,13 @@ target_include_directories(cvc5jni PUBLIC ${JNI_DIR})
 target_link_libraries(cvc5jni PRIVATE ${JNI_LIBRARIES})
 target_link_libraries(cvc5jni PRIVATE cvc5-shared)
 
-set(CVC5_JAR "cvc5-${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}.jar")
+set(CVC5_JAR "cvc5-${CVC5_VERSION}.jar")
 
 # create cvc5.jar file
 add_jar(cvc5jar
   SOURCES
   ${JAVA_FILES}
-  VERSION ${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}
+  VERSION ${CVC5_VERSION}
   OUTPUT_NAME cvc5
 )
 set_target_properties(cvc5jar PROPERTIES SOURCES "${JAVA_FILES}")
diff --git a/src/api/python/setup.py.in b/src/api/python/setup.py.in
index 7f8783a28..05efa152b 100644
--- a/src/api/python/setup.py.in
+++ b/src/api/python/setup.py.in
@@ -22,7 +22,7 @@
 
 from setuptools import setup
 
-CVC5_VERSION='${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}'
+CVC5_VERSION='${CVC5_VERSION}'
 
 setup(name='pycvc5',
       version=CVC5_VERSION,
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index 78f6cd069..8c1c2a714 100644
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -13,15 +13,6 @@
 # The build system configuration.
 ##
 
-# Extract info from Git for git_versioninfo.cpp
-# Note: GitInfo.cmake generates git_versioninfo.cpp.
-find_package(Git)
-configure_file(GitInfo.cmake.in GitInfo.cmake @ONLY)
-add_custom_target(gen-gitinfo
-  BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
-  COMMAND ${CMAKE_COMMAND} -DGIT_FOUND=${GIT_FOUND} -P GitInfo.cmake)
-
-
 # Generate cvc5config.h header
 configure_file(cvc5config.h.in cvc5config.h)
 
@@ -40,10 +31,10 @@ set(LIBBASE_SOURCES
   modal_exception.h
   output.cpp
   output.h
-  ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
+  ${CMAKE_CURRENT_BINARY_DIR}/versioninfo.cpp
 )
 set_source_files_properties(
-  ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
+  ${CMAKE_CURRENT_BINARY_DIR}/versioninfo.cpp
   PROPERTIES GENERATED TRUE
 )
 
@@ -86,4 +77,4 @@ set_source_files_properties(
 add_library(cvc5base OBJECT ${LIBBASE_SOURCES})
 set_target_properties(cvc5base PROPERTIES POSITION_INDEPENDENT_CODE ON)
 target_compile_definitions(cvc5base PRIVATE -D__BUILDING_CVC5LIB)
-add_dependencies(cvc5base gen-gitinfo gen-tags)
+add_dependencies(cvc5base gen-versioninfo gen-tags)
diff --git a/src/base/GitInfo.cmake.in b/src/base/GitInfo.cmake.in
deleted file mode 100644
index 56a1c5fdb..000000000
--- a/src/base/GitInfo.cmake.in
+++ /dev/null
@@ -1,48 +0,0 @@
-###############################################################################
-# Top contributors (to current version):
-#   Aina Niemetz, Mathias Preiner
-#
-# This file is part of the cvc5 project.
-#
-# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
-# in the top-level source directory and their institutional affiliations.
-# All rights reserved.  See the file COPYING in the top-level source
-# directory for licensing information.
-# #############################################################################
-##
-
-set(GIT_BUILD "false")
-set(GIT_IS_DIRTY "false")
-set(GIT_SHA1 "")
-set(GIT_BRANCH "")
-
-if(GIT_FOUND)
-  # Get current git branch, result is != 0 if this is not a git repository
-  execute_process(
-    COMMAND @GIT_EXECUTABLE@ -C @PROJECT_SOURCE_DIR@ rev-parse --abbrev-ref HEAD
-    RESULT_VARIABLE GIT_RESULT
-    OUTPUT_VARIABLE GIT_BRANCH
-    OUTPUT_STRIP_TRAILING_WHITESPACE
-  )
-  if("${GIT_RESULT}" STREQUAL "0")
-    set(GIT_BUILD "true")
-    # Extract sha1 of HEAD
-    execute_process(
-      COMMAND @GIT_EXECUTABLE@ -C @PROJECT_SOURCE_DIR@ rev-parse HEAD
-      OUTPUT_VARIABLE GIT_SHA1
-      OUTPUT_STRIP_TRAILING_WHITESPACE
-    )
-    # Result is != 0 if worktree is dirty
-    # Note: git diff HEAD shows both staged and unstaged changes.
-    execute_process(
-      COMMAND @GIT_EXECUTABLE@ -C @PROJECT_SOURCE_DIR@ diff HEAD --quiet
-      RESULT_VARIABLE GIT_RESULT
-    )
-    if(NOT "${GIT_RESULT}" STREQUAL "0")
-      set(GIT_IS_DIRTY "true")
-    endif()
-  endif()
-endif()
-
-configure_file(
-  @CMAKE_CURRENT_SOURCE_DIR@/git_versioninfo.cpp.in git_versioninfo.cpp)
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index b4f6cae7f..35a899617 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -82,15 +82,7 @@ bool Configuration::isStaticBuild()
 
 string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }
 
-string Configuration::getVersionString() { return CVC5_RELEASE_STRING; }
-
-unsigned Configuration::getVersionMajor() { return CVC5_MAJOR; }
-
-unsigned Configuration::getVersionMinor() { return CVC5_MINOR; }
-
-unsigned Configuration::getVersionRelease() { return CVC5_RELEASE; }
-
-std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; }
+string Configuration::getVersionString() { return CVC5_FULL_VERSION; }
 
 std::string Configuration::copyright() {
   std::stringstream ss;
@@ -205,9 +197,9 @@ std::string Configuration::copyright() {
 
 std::string Configuration::about() {
   std::stringstream ss;
-  ss << "This is cvc5 version " << CVC5_RELEASE_STRING;
+  ss << "This is cvc5 version " << getVersionString();
   if (Configuration::isGitBuild()) {
-    ss << " [" << Configuration::getGitId() << "]";
+    ss << " [" << Configuration::getGitInfo() << "]";
   }
   ss << "\ncompiled with " << Configuration::getCompiler()
      << "\non " << Configuration::getCompiledDateTime() << "\n\n";
@@ -271,36 +263,11 @@ bool Configuration::isTraceTag(const std::string& tag)
 }
 
 bool Configuration::isGitBuild() {
-  return IS_GIT_BUILD;
-}
-
-const char* Configuration::getGitBranchName() {
-  return GIT_BRANCH_NAME;
-}
-
-const char* Configuration::getGitCommit() {
-  return GIT_COMMIT;
+  return GIT_BUILD;
 }
 
-bool Configuration::hasGitModifications() {
-  return GIT_HAS_MODIFICATIONS;
-}
-
-std::string Configuration::getGitId() {
-  if(! isGitBuild()) {
-    return "";
-  }
-
-  const char* branchName = getGitBranchName();
-  if(*branchName == '\0') {
-    branchName = "-";
-  }
-
-  stringstream ss;
-  ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
-     << (::cvc5::Configuration::hasGitModifications() ? " (with modifications)"
-                                                      : "");
-  return ss.str();
+std::string Configuration::getGitInfo() {
+  return CVC5_GIT_INFO;
 }
 
 std::string Configuration::getCompiler() {
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 01579526d..f9a21f77a 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -36,10 +36,11 @@ class CVC5_EXPORT Configuration
   Configuration();
 
   // these constants are filled in by the build system
-  static const bool IS_GIT_BUILD;
-  static const char* const GIT_BRANCH_NAME;
-  static const char* const GIT_COMMIT;
-  static const bool GIT_HAS_MODIFICATIONS;
+  static const bool GIT_BUILD;
+  static const bool CVC5_IS_RELEASE;
+  static const char* const CVC5_VERSION;
+  static const char* const CVC5_FULL_VERSION;
+  static const char* const CVC5_GIT_INFO;
 
 public:
 
@@ -82,14 +83,6 @@ public:
 
   static std::string getVersionString();
 
-  static unsigned getVersionMajor();
-
-  static unsigned getVersionMinor();
-
-  static unsigned getVersionRelease();
-
-  static std::string getVersionExtra();
-
   static std::string copyright();
 
   static std::string about();
@@ -123,10 +116,7 @@ public:
   static bool isTraceTag(const std::string& tag);
 
   static bool isGitBuild();
-  static const char* getGitBranchName();
-  static const char* getGitCommit();
-  static bool hasGitModifications();
-  static std::string getGitId();
+  static std::string getGitInfo();
 
   static std::string getCompiler();
   static std::string getCompiledDateTime();
diff --git a/src/base/cvc5config.h.in b/src/base/cvc5config.h.in
index a824a9c1f..39619f928 100644
--- a/src/base/cvc5config.h.in
+++ b/src/base/cvc5config.h.in
@@ -1,21 +1,6 @@
 #ifndef CVC5__BASE__CVC5CONFIG_H
 #define CVC5__BASE__CVC5CONFIG_H
 
-/* Major component of the version of cvc5. */
-#define CVC5_MAJOR @CVC5_MAJOR@
-
-/* Minor component of the version of cvc5. */
-#define CVC5_MINOR @CVC5_MINOR@
-
-/* Release component of the version of cvc5. */
-#define CVC5_RELEASE @CVC5_RELEASE@
-
-/* Extraversion component of the version of cvc5. */
-#define CVC5_EXTRAVERSION "@CVC5_EXTRAVERSION@"
-
-/* Full release string for cvc5. */
-#define CVC5_RELEASE_STRING "@CVC5_RELEASE_STRING@"
-
 /* Full name of this package. */
 #define CVC5_PACKAGE_NAME "@CVC5_PACKAGE_NAME@"
 
diff --git a/src/base/git_versioninfo.cpp.in b/src/base/versioninfo.cpp.in
index 3db99fe15..0e873d7b3 100644
--- a/src/base/git_versioninfo.cpp.in
+++ b/src/base/versioninfo.cpp.in
@@ -14,7 +14,9 @@
  */
 
 #include "base/configuration.h"
-const bool ::cvc5::Configuration::IS_GIT_BUILD = @GIT_BUILD@;
-const char* const ::cvc5::Configuration::GIT_BRANCH_NAME = "@GIT_BRANCH@";
-const char* const ::cvc5::Configuration::GIT_COMMIT = "@GIT_SHA1@";
-const bool ::cvc5::Configuration::GIT_HAS_MODIFICATIONS = @GIT_IS_DIRTY@;
+
+const bool ::cvc5::Configuration::GIT_BUILD = @GIT_BUILD@;
+const bool ::cvc5::Configuration::CVC5_IS_RELEASE = @CVC5_IS_RELEASE@;
+const char* const ::cvc5::Configuration::CVC5_VERSION = "@CVC5_VERSION@";
+const char* const ::cvc5::Configuration::CVC5_FULL_VERSION = "@CVC5_FULL_VERSION@";
+const char* const ::cvc5::Configuration::CVC5_GIT_INFO = "@CVC5_GIT_INFO@";
\ No newline at end of file
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d6a6f9331..4e92584a8 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -189,7 +189,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
                     << Configuration::getVersionString();
       if (Configuration::isGitBuild())
       {
-        CVC5Message() << " [" << Configuration::getGitId() << "]";
+        CVC5Message() << " [" << Configuration::getGitInfo() << "]";
       }
       CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
                     << " assertions:"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 0dfeb3b2c..93b08a858 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -451,20 +451,9 @@ void OptionsHandler::showConfiguration(const std::string& option,
   std::cout << Configuration::about() << std::endl;
 
   print_config("version", Configuration::getVersionString());
-
   if (Configuration::isGitBuild())
   {
-    const char* branchName = Configuration::getGitBranchName();
-    if (*branchName == '\0')
-    {
-      branchName = "-";
-    }
-    std::stringstream ss;
-    ss << "git [" << branchName << " "
-       << std::string(Configuration::getGitCommit()).substr(0, 8)
-       << (Configuration::hasGitModifications() ? " (with modifications)" : "")
-       << "]";
-    print_config("scm", ss.str());
+    print_config("scm", Configuration::getGitInfo());
   }
   else
   {
@@ -474,9 +463,7 @@ void OptionsHandler::showConfiguration(const std::string& option,
   std::cout << std::endl;
 
   std::stringstream ss;
-  ss << Configuration::getVersionMajor() << "."
-     << Configuration::getVersionMinor() << "."
-     << Configuration::getVersionRelease();
+  ss << Configuration::getVersionString();
   print_config("library", ss.str());
 
   std::cout << std::endl;