test

3 files changed, 42 insertions, 8 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 85132563b..268191db3 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -175,8 +175,6 @@ jobs:
 
     - name: Run Clang-Tidy
       if: matrix.run-clang-tidy && runner.os == 'Linux'
-      run: |
-        ../.github/workflows/run-clang-tidy.py
-      working-directory: build
+      run: .github/workflows/run-clang-tidy.py
       env:
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.github/workflows/run-clang-tidy.py b/.github/workflows/run-clang-tidy.py
index 13d9c784f..309cef41b 100755
--- a/.github/workflows/run-clang-tidy.py
+++ b/.github/workflows/run-clang-tidy.py
@@ -1,11 +1,48 @@
 #!/usr/bin/env python3
 
 import collections
+import re
 import requests
+import subprocess
 import os
 
 Finding = collections.namedtuple("Finding", ["line", "text"])
 
+def checkable_file(fn):
+    if any(fn.endswith(ext) for ext in ['.h', '.cpp']):
+        return '_template.' not in fn
+    return False
+
+def get_commit_files(sha):
+    cmd = ['git', 'diff-tree', '--no-commit-id', '--name-only', '-r', sha]
+    files = subprocess.check_output(cmd).decode().splitlines()
+    return [fn for fn in files if checkable_file(fn)]
+
+def parse_clang_output(output):
+    error_re = ".*:(\d+):\d+: (.*)"
+    out = []
+    for l in output.splitlines():
+        m = re.match(error_re, l)
+        if m:
+            line = int(m.group(1))
+            msg = m.group(2)
+            out.append(Finding(line=line, text=msg))
+
+    return out
+
+def get_findings(files):
+    result = {}
+    for fn in files:
+        cmd = ['clang-tidy', '-p', 'build', fn]
+        proc = subprocess.Popen(
+            cmd,
+            stdin=subprocess.PIPE,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.PIPE)
+        out, err = proc.communicate()
+        result[fn] = parse_clang_output(out.decode())
+    return result
+
 def report_github_status(repo, token, sha, findings):
     url = "https://api.github.com/repos/{}/check-runs".format(repo)
     annotations = []
@@ -43,13 +80,12 @@ def report_github_status(repo, token, sha, findings):
 
 
 def main():
-    findings = {
-            'CMakeLists.txt': [Finding(5, 'foobar')]
-            }
+    sha = os.environ['GITHUB_SHA']
+    files = get_commit_files(sha)
+    findings = get_findings(files)
 
     if 'GITHUB_TOKEN' in os.environ:
         repo = os.environ['GITHUB_REPOSITORY']
-        sha = os.environ['GITHUB_SHA']
         token = os.environ['GITHUB_TOKEN']
         report_github_status(repo, token, sha, findings)
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 38c99f551..64886e15c 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -87,7 +87,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
       Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
                        << std::endl;
-      proofRecipe->dump("pf::sat");
+      proofRecipe->dump("pf::satxx");
 
       delete proofRecipe;
       proofRecipe = NULL;