7 files changed, 67 insertions, 160 deletions
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index e28bd78cc..e73c82d76 100644
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -40,9 +40,7 @@ libcvc4_add_sources(GENERATED git_versioninfo.cpp)
 #-----------------------------------------------------------------------------#
 # Generate code for debug/trace tags
 
-set(gentmptags_script ${CMAKE_CURRENT_LIST_DIR}/gentmptags.sh)
-set(gentags_script ${CMAKE_CURRENT_LIST_DIR}/gentags.sh)
-set(genheader_script ${CMAKE_CURRENT_LIST_DIR}/genheader.sh)
+set(collect_tags_script ${CMAKE_CURRENT_LIST_DIR}/collect_tags.py)
 
 file(GLOB_RECURSE source_files
      ${PROJECT_SOURCE_DIR}/src/*.cpp
@@ -52,41 +50,15 @@ file(GLOB_RECURSE source_files
 string(REPLACE ";" " " source_files_list "${source_files}")
 
 add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
-  COMMAND
-    ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Debug ${source_files_list}
-  DEPENDS mktags ${gentmptags_script} ${source_files}
-)
-
-add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
-  COMMAND
-    ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Trace ${source_files_list}
-  DEPENDS mktags ${gentmptags_script} ${source_files}
-)
-
-add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
-  COMMAND ${gentags_script} Debug
-  DEPENDS ${gentags_script} ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
-)
-
-add_custom_command(
-  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
-  COMMAND ${gentags_script} Trace
-  DEPENDS ${gentags_script} ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
-)
-
-add_custom_command(
   OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h
-  COMMAND ${genheader_script} ${CMAKE_CURRENT_LIST_DIR} Debug
-  DEPENDS mktagheaders ${genheader_script} ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
+  COMMAND ${PYTHON_EXECUTABLE} ${collect_tags_script} ${CMAKE_CURRENT_BINARY_DIR}/ Debug ${PROJECT_SOURCE_DIR}/src
+  DEPENDS ${collect_tags_script} ${source_files}
 )
 
 add_custom_command(
   OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h
-  COMMAND ${genheader_script} ${CMAKE_CURRENT_LIST_DIR} Trace
-  DEPENDS mktagheaders ${genheader_script} ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
+  COMMAND ${PYTHON_EXECUTABLE} ${collect_tags_script} ${CMAKE_CURRENT_BINARY_DIR}/ Trace ${PROJECT_SOURCE_DIR}/src
+  DEPENDS ${collect_tags_script} ${source_files}
 )
 
 add_custom_target(gen-tags
diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py
new file mode 100644
index 000000000..ea4938d6b
--- /dev/null
+++ b/src/base/collect_tags.py
@@ -0,0 +1,62 @@
+#!/usr/bin/env python3
+
+import argparse
+import glob
+import os
+import re
+import shutil
+import subprocess
+
+
+def parse_args():
+    """Parse command line arguments and return them."""
+    ap = argparse.ArgumentParser(description='collect debug and trace tags')
+    ap.add_argument('destdir', help='where to put the results')
+    ap.add_argument('type', choices=['Debug', 'Trace'], help='which tags to collect')
+    ap.add_argument('basedir', help='where to look for source file')
+    return ap.parse_args()
+
+
+def collect_tags(basedir):
+    """Collect all tags used in filed within the given base directory.
+    Return them sorted lexicographically."""
+    tags = set()
+    for ext in ['.cc', '.cpp', '.g', '.h']:
+        for filename in glob.iglob('{}/**/*{}'.format(basedir, ext), recursive=True):
+            content = open(filename).read()
+            for tag in RE_PAT.finditer(content):
+                tags.add(tag.group(1))
+    return sorted(tags)
+
+
+def write_file(filename, type, tags):
+    """Render the header file to the given filename."""
+    with open(filename, 'w') as out:
+        out.write('static char const* const {}_tags[] = {{\n'.format(type))
+        for t in tags:
+            out.write('"{}",\n'.format(t))
+        out.write('nullptr\n')
+        out.write('};\n')
+
+
+if __name__ == '__main__':
+    # setup
+    opts = parse_args()
+    RE_PAT = re.compile('{}(?:\\.isOn)?\\("([^"]+)"\\)'.format(opts.type))
+    FILENAME_TMP = '{}/{}_tags.tmp'.format(opts.destdir, opts.type)
+    FILENAME_DEST = '{}/{}_tags.h'.format(opts.destdir, opts.type)
+
+    # collect tags
+    tags = collect_tags(opts.basedir)
+    # write header file
+    write_file(FILENAME_TMP, opts.type, tags)
+
+    if not os.path.isfile(FILENAME_DEST):
+        # file does not exist yet
+        shutil.copy(FILENAME_TMP, FILENAME_DEST)
+    elif subprocess.run(
+        ['diff', FILENAME_TMP, FILENAME_DEST],
+        stdout=subprocess.PIPE
+    ).returncode == 1:
+        # file needs to change
+        shutil.copy(FILENAME_TMP, FILENAME_DEST)
diff --git a/src/base/genheader.sh b/src/base/genheader.sh
deleted file mode 100755
index 2091f7781..000000000
--- a/src/base/genheader.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/bin/sh
-#
-# Convenience wrapper for cmake in src/base/CMakeLists.txt
-#
-# Create Debug_tags.h/Trace_tags.h header files.
-#
-# Usage: genheader.sh <directory-mktags> Debug|Trace
-
-path="$1"
-shift
-tags_type="$1" # Debug/Trace
-tags_file="${tags_type}_tags"
-
-if [ "${tags_type}" != "Debug" ] && [ "${tags_type}" != "Trace" ]; then
-  echo "$0: Invalid tags type '${tags_type}' (must be 'Debug' or 'Trace')"
-  exit 1
-fi
-
-[ ! -e "${tags_file}" ] && echo "$0: ${tags_file} does not exist" && exit 1
-
-"${path}/mktagheaders" "${tags_file}" "${tags_file}" > "${tags_file}.h"
diff --git a/src/base/gentags.sh b/src/base/gentags.sh
deleted file mode 100755
index 67888b3f5..000000000
--- a/src/base/gentags.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/sh
-#
-# Convenience wrapper for cmake in src/base/CMakeLists.txt
-#
-# Update Debug_tags/Trace_tags in case that debug/trace tags have been
-# modified. Use diff to compare the contents of the *.tmp files with the
-# corresponding *_tags file.
-#
-# Usage: gentags.sh Debug|Trace
-
-tags_type="$1" # Debug/Trace
-tags_file="${tags_type}_tags"
-
-if [ "${tags_type}" != "Debug" ] && [ "${tags_type}" != "Trace" ]; then
-  echo "$0: Invalid tags type '${tags_type}' (must be 'Debug' or 'Trace')"
-  exit 1
-fi
-
-[ ! -e "${tags_file}.tmp" ] && \
-    echo "$0: ${tags_file}.tmp does not exist" && exit 1
-
-if [ -e "${tags_file}" ]; then
-  # Do not update file if tags didn't change.
-  diff -q "${tags_file}.tmp" "${tags_file}" > /dev/null 2>&1 && exit 0
-fi
-mv "${tags_file}.tmp" "${tags_file}"
diff --git a/src/base/gentmptags.sh b/src/base/gentmptags.sh
deleted file mode 100755
index 566fa1747..000000000
--- a/src/base/gentmptags.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/bin/sh
-#
-# Convenience wrapper for cmake in src/base/CMakeLists.txt
-#
-# Create Debug_tags.tmp/Trace_tags.tmp files from given source files.
-#
-# Usage: gentmptags.sh <directory-mktags> Debug|Trace <source files ...>
-
-path="$1"
-shift
-tags_type="$1"
-tags_file="${tags_type}_tags"
-shift
-source_files_list="$*"
-
-if [ "${tags_type}" != "Debug" ] && [ "${tags_type}" != "Trace" ]; then
-  echo "$0: Invalid tags type '${tags_type}' (must be 'Debug' or 'Trace')"
-  exit 1
-fi
-
-"${path}/mktags" "${tags_type}" "${source_files_list}" > "${tags_file}.tmp"
diff --git a/src/base/mktagheaders b/src/base/mktagheaders
deleted file mode 100755
index af44cee8d..000000000
--- a/src/base/mktagheaders
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/bash
-#
-# mktagheaders
-#
-# The purpose of this script is to generate the *_tag.h header file from the
-# *_tags file.
-#
-# Invocation:
-#
-#    mktagheaders <tag-name> <tag-file>
-#
-# <tag-name> will be the name of the generated array.
-# <tag-file> each line of this file is turned into a string in the generated
-#   array.
-
-TAG_NAME=$1
-TAG_FILE=$2
-
-echo 'static char const* const '$TAG_NAME'[] = {';
-for tag in `cat $TAG_FILE`; do
-  echo "\"$tag\",";
-done;
-echo 'NULL';
-echo '};'
diff --git a/src/base/mktags b/src/base/mktags
deleted file mode 100755
index 090e57014..000000000
--- a/src/base/mktags
+++ /dev/null
@@ -1,35 +0,0 @@
-#!/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} <input-files>
-#
-# <input-files> is expected to be passed a single space separated list of files.
-#  One can use quotes to achieve this. This is one reason to use "$(...)"
-#  instead of back ticks `...`.
-
-DebugOrTrace=$1
-InputFiles=$2
-
-grep -h '\<'$DebugOrTrace'\(\.isOn\)* *( *\".*\" *)' \
-  $InputFiles | \
-  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