include subversion information used for each build in the --show-config output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from

5 files changed, 78 insertions, 2 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index d65ddc570..bf20c9f77 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -29,7 +29,7 @@ libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION)
 nodist_EXTRA_libcvc4_noinst_la_SOURCES = dummy.cpp
 nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp
 libcvc4_noinst_la_SOURCES =
-libcvc4_la_SOURCES =
+libcvc4_la_SOURCES = subversion_versioninfo.cpp
 libcvc4_la_LIBADD = \
 	@builddir@/util/libutil.la \
 	@builddir@/expr/libexpr.la \
@@ -61,6 +61,32 @@ publicheaders = \
 	include/cvc4_public.h \
 	include/cvc4parser_public.h
 
+subversion_versioninfo.cpp: svninfo
+	$(AM_V_GEN)( \
+	  if test -s svninfo; then \
+	    issvn=true; \
+	    branch=`grep '^URL: ' svninfo | sed 's,.*/cvc4/,,'`; \
+	    rev=`grep '^Revision: ' svninfo | awk '{print$$2}'`; \
+	    mods=`grep '^Modifications: ' svninfo | awk '{print$$2}'`; \
+	  else \
+	    issvn=false; \
+	    branch=unknown; \
+	    rev=0; \
+	    mods=false; \
+	  fi; \
+	  echo "#include \"util/configuration.h\""; \
+	  echo "const bool ::CVC4::Configuration::IS_SUBVERSION_BUILD = $$issvn;"; \
+	  echo "const char* const ::CVC4::Configuration::SUBVERSION_BRANCH_NAME = \"$$branch\";"; \
+	  echo "const unsigned ::CVC4::Configuration::SUBVERSION_REVISION = $$rev;"; \
+	  echo "const bool ::CVC4::Configuration::SUBVERSION_HAS_MODIFICATIONS = $$mods;"; \
+	) >"$@"
+svninfo: svninfo.tmp
+	$(AM_V_GEN)diff -q svninfo.tmp svninfo &>/dev/null || mv svninfo.tmp svninfo || true
+# .PHONY ensures it's always rebuilt
+.PHONY: 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
+
 install-data-local: $(publicheaders)
 	$(mkinstalldirs) $(DESTDIR)$(prefix)$(includedir)/cvc4
 	@for f in $(publicheaders); do \
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 9cb963d5c..9c2464b8d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -278,6 +278,19 @@ int runCvc4(int argc, char* argv[]) {
   Command* cmd;
   if( options.interactive ) {
     InteractiveShell shell(exprMgr, options);
+    Message() << Configuration::getPackageName()
+              << " " << Configuration::getVersionString();
+    if(Configuration::isSubversionBuild()) {
+      Message() << " [subversion " << Configuration::getSubversionBranchName()
+                << " r" << Configuration::getSubversionRevision()
+                << (Configuration::hasSubversionModifications() ?
+                    " (with modifications)" : "")
+                << "]";
+    }
+    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+              << " assertions:"
+              << (Configuration::isAssertionBuild() ? "on" : "off")
+              << endl;
     if(replayParser != NULL) {
       // have the replay parser use the declarations input interactively
       replayParser->useDeclarationsFrom(shell.getParser());
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index afd30bba9..db3c5520e 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -108,4 +108,20 @@ bool Configuration::isBuiltWithTlsSupport() {
   return USING_TLS;
 }
 
+bool Configuration::isSubversionBuild() {
+  return IS_SUBVERSION_BUILD;
+}
+
+const char* Configuration::getSubversionBranchName() {
+  return SUBVERSION_BRANCH_NAME;
+}
+
+unsigned Configuration::getSubversionRevision() {
+  return SUBVERSION_REVISION;
+}
+
+bool Configuration::hasSubversionModifications() {
+  return SUBVERSION_HAS_MODIFICATIONS;
+}
+
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 3aae370d9..258431114 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -35,6 +35,12 @@ class CVC4_PUBLIC Configuration {
   /** Private default ctor: Disallow construction of this class */
   Configuration();
 
+  // these constants are filled in by the build system
+  static const bool IS_SUBVERSION_BUILD;
+  static const char* const SUBVERSION_BRANCH_NAME;
+  static const unsigned SUBVERSION_REVISION;
+  static const bool SUBVERSION_HAS_MODIFICATIONS;
+
 public:
 
   static std::string getName();
@@ -76,7 +82,13 @@ public:
   static bool isBuiltWithCudd();
 
   static bool isBuiltWithTlsSupport();
-};
+
+  static bool isSubversionBuild();
+  static const char* getSubversionBranchName();
+  static unsigned getSubversionRevision();
+  static bool hasSubversionModifications();
+
+};/* class Configuration */
 
 }/* CVC4 namespace */
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index dbe0f6804..f68b64ab6 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -578,6 +578,15 @@ throw(OptionException) {
       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",
+               Configuration::getSubversionBranchName(),
+               Configuration::getSubversionRevision(),
+               Configuration::hasSubversionModifications() ?
+                 " (with modifications)" : "");
+      } else {
+        printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
+      }
       printf("\n");
       printf("library    : %u.%u.%u\n",
              Configuration::getVersionMajor(),