From 72832c1a749e4bde8d16930b0f59e5db9810cafc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 25 Jan 2013 17:11:44 -0500 Subject: Fix version identification for new git repository. --- src/Makefile.am | 41 +++++++++++++++++++++++++++++++++++----- src/main/driver_unified.cpp | 4 +++- src/main/options_handlers.h | 12 +++++++++--- src/util/configuration.cpp | 29 +++++++++++++++++++++++++++- src/util/configuration.h | 10 ++++++++++ src/util/configuration_private.h | 5 ++++- 6 files changed, 90 insertions(+), 11 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index 1d54bc2a8..3087d934c 100644 --- 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 741975b11..9fa40d3ab 100644 --- 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 c2eb489ed..f14a67d5f 100644 --- 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 59fe28eca..c6e951049 100644 --- 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 3f6547872..c85f62f7f 100644 --- 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 c480b4318..e0c750749 100644 --- 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\ -- cgit v1.2.3