Fix version identification for new git repository.

diff --git a/src/Makefile.am b/src/Makefile.am
index 1d54bc2a8be053d5f0f2fd977c6b1e9eeee0db8e..3087d934caf8d12be20a889c67a0c027cddd7f89 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -30,8 +30,8 @@ libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION)
 # as a C library, which messes up exception handling support)
 nodist_EXTRA_libcvc4_noinst_la_SOURCES = dummy.cpp
 nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp
-libcvc4_noinst_la_SOURCES = subversion_versioninfo.cpp
-libcvc4_la_SOURCES = subversion_versioninfo.cpp
+libcvc4_noinst_la_SOURCES = git_versioninfo.cpp svn_versioninfo.cpp
+libcvc4_la_SOURCES = git_versioninfo.cpp svn_versioninfo.cpp
 libcvc4_la_LIBADD = \
        @builddir@/options/liboptions.la \
        @builddir@/util/libutil.la \
@@ -67,9 +67,12 @@ libcvc4_noinst_la_LIBADD += \
 endif
 
 CLEANFILES = \
-       subversion_versioninfo.cpp \
+       svn_versioninfo.cpp \
        svninfo.tmp \
-       svninfo
+       svninfo \
+       git_versioninfo.cpp \
+       gitinfo.tmp \
+       gitinfo
 
 EXTRA_DIST = \
        include/cvc4_private_library.h \
@@ -80,7 +83,7 @@ EXTRA_DIST = \
        include/cvc4.h \
        cvc4.i
 
-subversion_versioninfo.cpp: svninfo
+svn_versioninfo.cpp: svninfo
        $(AM_V_GEN)( \
          if test -s svninfo; then \
            issvn=true; \
@@ -108,6 +111,34 @@ svninfo: svninfo.tmp
 svninfo.tmp:
        $(AM_V_GEN)(cd "$(top_srcdir)" && svn info && echo "Modifications: `test -z \"\`svn status -q\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
 
+git_versioninfo.cpp: gitinfo
+       $(AM_V_GEN)( \
+         if test -s gitinfo; then \
+           isgit=true; \
+           branch=`head -1 gitinfo`; \
+           rev=`head -2 gitinfo | tail -1 | awk '{print$$1}'`; \
+           mods=`grep '^Modifications: ' gitinfo | awk '{print$$2}'`; \
+         else \
+           isgit=false; \
+           branch=unknown; \
+           rev=0; \
+           mods=false; \
+         fi; \
+         echo "#include \"util/configuration.h\""; \
+         echo "const bool ::CVC4::Configuration::IS_GIT_BUILD = $$isgit;"; \
+         echo "const char* const ::CVC4::Configuration::GIT_BRANCH_NAME = \"$$branch\";"; \
+         echo "const char* const ::CVC4::Configuration::GIT_COMMIT = \"$$rev\";"; \
+         echo "const bool ::CVC4::Configuration::GIT_HAS_MODIFICATIONS = $$mods;"; \
+       ) >"$@"
+# This .tmp business is to keep from having to re-compile options.cpp
+# (and then re-link the libraries) if nothing has changed.
+gitinfo: gitinfo.tmp
+       $(AM_V_GEN)diff -q gitinfo.tmp gitinfo &>/dev/null || mv gitinfo.tmp gitinfo || true
+# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
+.PHONY: gitinfo.tmp
+gitinfo.tmp:
+       $(AM_V_GEN)(cd "$(top_srcdir)" && sed 's,^ref: refs/heads/,,' .git/HEAD && git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD` && echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
+
 install-data-local:
        (echo include/cvc4.h; \
         echo include/cvc4_public.h; \

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 741975b112c621a478f5409ad5b4e396aa786cc2..9fa40d3abd748a17ac861030e4b8cce69316f6fe 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -239,7 +239,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       InteractiveShell shell(*exprMgr, opts);
       Message() << Configuration::getPackageName()
                 << " " << Configuration::getVersionString();
-      if(Configuration::isSubversionBuild()) {
+      if(Configuration::isGitBuild()) {
+        Message() << " [" << Configuration::getGitId() << "]";
+      } else if(Configuration::isSubversionBuild()) {
         Message() << " [" << Configuration::getSubversionId() << "]";
       }
       Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")

diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index c2eb489ed98d4a6bb886f58ce7595d5cd8806321..f14a67d5f9582ffc70d303296977aa3e4ede4e01 100644 (file)
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -26,14 +26,20 @@ inline void showConfiguration(std::string option, SmtEngine* smt) {
   fputs(Configuration::about().c_str(), stdout);
   printf("\n");
   printf("version    : %s\n", Configuration::getVersionString().c_str());
-  if(Configuration::isSubversionBuild()) {
-    printf("subversion : yes [%s r%u%s]\n",
+  if(Configuration::isGitBuild()) {
+    printf("scm        : git [%s %s%s]\n",
+           Configuration::getGitBranchName(),
+           std::string(Configuration::getGitCommit()).substr(0, 8).c_str(),
+           Configuration::hasGitModifications() ?
+             " (with modifications)" : "");
+  } else if(Configuration::isSubversionBuild()) {
+    printf("scm        : svn [%s r%u%s]\n",
            Configuration::getSubversionBranchName(),
            Configuration::getSubversionRevision(),
            Configuration::hasSubversionModifications() ?
              " (with modifications)" : "");
   } else {
-    printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
+    printf("scm        : no\n");
   }
   printf("\n");
   printf("library    : %u.%u.%u\n",

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 59fe28ecae7515515f61adaf56d47a51aca01e57..c6e9510499a98de00f23e99058bdeef787fa164c 100644 (file)
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -195,6 +195,33 @@ bool Configuration::isTraceTag(char const * tag){
   return false;
 }
 
+bool Configuration::isGitBuild() {
+  return IS_GIT_BUILD;
+}
+
+const char* Configuration::getGitBranchName() {
+  return GIT_BRANCH_NAME;
+}
+
+const char* Configuration::getGitCommit() {
+  return GIT_COMMIT;
+}
+
+bool Configuration::hasGitModifications() {
+  return GIT_HAS_MODIFICATIONS;
+}
+
+std::string Configuration::getGitId() {
+  if(! isGitBuild()) {
+    return "";
+  }
+
+  stringstream ss;
+  ss << "git " << getGitBranchName() << " " << string(getGitCommit()).substr(0, 8)
+     << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" );
+  return ss.str();
+}
+
 bool Configuration::isSubversionBuild() {
   return IS_SUBVERSION_BUILD;
 }
@@ -211,7 +238,7 @@ bool Configuration::hasSubversionModifications() {
   return SUBVERSION_HAS_MODIFICATIONS;
 }
 
-string Configuration::getSubversionId() {
+std::string Configuration::getSubversionId() {
   if(! isSubversionBuild()) {
     return "";
   }

diff --git a/src/util/configuration.h b/src/util/configuration.h
index 3f654787262cfb7b86c4f24c04d0da58d32dcf34..c85f62f7fe4c78d2239f30c901cf419bc88d44a9 100644 (file)
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -38,6 +38,10 @@ class CVC4_PUBLIC Configuration {
   static const char* const SUBVERSION_BRANCH_NAME;
   static const unsigned SUBVERSION_REVISION;
   static const bool SUBVERSION_HAS_MODIFICATIONS;
+  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;
 
 public:
 
@@ -101,6 +105,12 @@ public:
   /* Test if the given argument is a known trace tag name */
   static bool isTraceTag(char const *);
 
+  static bool isGitBuild();
+  static const char* getGitBranchName();
+  static const char* getGitCommit();
+  static bool hasGitModifications();
+  static std::string getGitId();
+
   static bool isSubversionBuild();
   static const char* getSubversionBranchName();
   static unsigned getSubversionRevision();

diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index c480b4318d501e66b10f3c876dbe0975d5d3f313..e0c7507494decb682293d596d38fdc3f25b50f80 100644 (file)
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -115,10 +115,13 @@ namespace CVC4 {
 
 #define CVC4_ABOUT_STRING ( ::std::string("\
 This is CVC4 version " CVC4_RELEASE_STRING ) + \
+    ( ::CVC4::Configuration::isGitBuild() \
+        ? ( ::std::string(" [") + ::CVC4::Configuration::getGitId() + "]" ) \
+        : \
     ( ::CVC4::Configuration::isSubversionBuild() \
         ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \
         : ::std::string("") \
-    ) + "\n\
+    )) + "\n\
 compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
 on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
 Copyright (C) 2009, 2010, 2011, 2012\n\