From: Tim King <taking@google.com>
Date: Sat, 24 Oct 2015 00:47:11 +0000 (-0700)
Subject: This commit moves the scripts for building the Debug_tags, Traces_tags, Debug_tags... 
X-Git-Tag: cvc5-1.0.0~6185
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=596581cefe8bc36f30f685d884d6152ff0b80b03;p=cvc5.git

This commit moves the scripts for building the Debug_tags, Traces_tags, Debug_tags.h and Trace_tags.h out of options/Makefile.am and into seperate scripts. This also enables these files always being created.
---

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 24b78836a..19aa43c98 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -131,35 +131,24 @@ EXTRA_DIST = \
 	../smt/smt_options.cpp \
 	options.cpp \
 	options_holder.h \
-	$(OPTIONS_FILES_SRCS)
+	$(OPTIONS_FILES_SRCS) \
+	mktagheaders \
+	mktags
+
 
-if CVC4_DEBUG
-# listing Debug_tags too ensures that make doesn't auto-remove it
+# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it
 # after building (if it does, we don't get the "cached" effect with
 # the .tmp files below, and we have to re-compile and re-link each
 # time, even when there are no changes).
 BUILT_SOURCES += \
 	Debug_tags.h \
-	Debug_tags
-endif
-if CVC4_TRACING
-# listing Trace_tags too ensures that make doesn't auto-remove it
-# after building (if it does, we don't get the "cached" effect with
-# the .tmp files below, and we have to re-compile and re-link each
-# time, even when there are no changes).
-BUILT_SOURCES += \
+	Debug_tags \
 	Trace_tags.h \
 	Trace_tags
-endif
-%_tags.h: %_tags
-	$(AM_V_GEN)( \
-	  echo 'static char const* const $^[] = {'; \
-	  for tag in `cat $^`; do \
-	    echo "\"$$tag\","; \
-	  done; \
-	  echo 'NULL'; \
-	  echo '};' \
-	) >"$@"
+
+%_tags.h: %_tags mktagheaders
+	$(AM_V_at)chmod +x @srcdir@/mktagheaders
+	$(AM_V_GEN)( @srcdir@/mktagheaders "$<" ) >"$@"
 
 # This .tmp business is to keep from having to re-compile options.cpp
 # (and then re-link the libraries) if nothing has changed.
@@ -171,11 +160,9 @@ endif
 # The "sed" invocation below is particularly obnoxious, but it works around
 # inconsistencies in REs on different platforms, using only a basic regular
 # expression (no |, no \<, ...).
-Debug_tags.tmp Trace_tags.tmp:
-	$(AM_V_GEN)\
-	grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
-		`find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
-	sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@"
+Debug_tags.tmp Trace_tags.tmp: mktags
+	$(AM_V_at)chmod +x @srcdir@/mktags
+	$(AM_V_GEN)(@srcdir@/mktags '$(@:_tags.tmp=)' '@srcdir@/../') >"$@"
 
 MOSTLYCLEANFILES = \
 	Debug_tags \
diff --git a/src/options/mktagheaders b/src/options/mktagheaders
new file mode 100755
index 000000000..63a19bc23
--- /dev/null
+++ b/src/options/mktagheaders
@@ -0,0 +1,20 @@
+#!/bin/bash
+#
+# mktagheaders
+#
+# The purpose of this script is to generate the *_tag.h header file from the
+# *_tags file.
+#
+# Invocation:
+#
+#    mktagheaders <tag-file>
+#
+
+TAG_FILE=$1
+
+echo 'static char const* const '$TAG_FILE'[] = {';
+for tag in `cat $TAG_FILE`; do
+  echo "\"$$tag\",";
+done;
+echo 'NULL';
+echo '};'
diff --git a/src/options/mktags b/src/options/mktags
new file mode 100755
index 000000000..169b373b8
--- /dev/null
+++ b/src/options/mktags
@@ -0,0 +1,32 @@
+#!/bin/bash
+#
+# mktags
+#
+# The purpose of this script is to create Debug_tags and Trace_tags files.
+# Note that in the Makefile workflow these are first stored in a *_tags.tmp
+# file. This file contains a list of all of the strings that occur in things
+# like Debug("foo") or Debug.isOn("bar") in a given directory. The list is
+# seperated by newlines.  The expected Debug_tags file for the previous two
+# tags would be:
+# bar
+# foo
+#
+# Invocation:
+#
+#    mktags {Debug,Trace} <directory>
+#
+
+DebugOrTrace=$1
+FindDirectory=$2
+
+grep -h '\<'$DebugOrTrace'\(\.isOn\)* *( *\".*\" *)' \
+  `find $FindDirectory -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
+  sed 's/\/\/.*//;s/^'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | \
+  LC_ALL=C sort | \
+  uniq
+
+
+# Reference copy of what this is replacing.
+# 	grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
+#		`find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
+#	sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq