[TRLC] include argument to output to logfile instead of stdout

Author: hoe-jo

trlc/errors.py

@@ -149,6 +149,12 @@ class Message_Handler:
     :attribute brief: When true displays as much context as possible
     :type: Boolean
 
+    :attribute out: Output stream (stdout if None)
+    :type: file or None
+
+    :attribute strip_prefix: Prefix stripped from file paths in messages
+    :type: str or None
+
     :attribute warnings: Number of system or user warnings raised
     :type: int
 
@@ -158,16 +164,44 @@ class Message_Handler:
     :attribute supressed: Number of messages supressed by policy
     :type: int
 
+    Can be used as a context manager (``with Message_Handler(...) as
+    mh:``), which will automatically close any file opened via
+    ``out_path``.
+
     """
-    def __init__(self, brief=False, detailed_info=True):
+    def __init__(self, brief=False, detailed_info=True,
+                 out=None, strip_prefix=None, out_path=None):
         assert isinstance(brief, bool)
+        assert isinstance(strip_prefix, str) or strip_prefix is None
+        assert isinstance(out_path, str) or out_path is None
         self.brief         = brief
         self.show_details  = detailed_info
         self.warnings      = 0
         self.errors        = 0
         self.suppressed    = 0
         self.sm            = None
         self.suppress_kind = set()
+        self.strip_prefix  = strip_prefix
+        if out_path is not None:
+            self._owned_file = open(out_path, "w", encoding="UTF-8")  # pylint: disable=consider-using-with
+            self.out         = self._owned_file
+        else:
+            self._owned_file = None
+            self.out         = out
+
+    def close(self):
+        if self._owned_file is not None:
+            self._owned_file.close()
+            self._owned_file = None
+
+    def __enter__(self):
+        return self
+
+    def __exit__(self, *_):
+        self.close()
+
+    def __del__(self):
+        self.close()
 
     def suppress(self, kind):
         assert isinstance(kind, Kind)
@@ -178,8 +212,7 @@ def cross_file_reference(self, location):
 
         if self.sm is None:
             return location.to_string(include_column=False)
-        else:
-            return self.sm.cross_file_reference(location)
+        return self.sm.cross_file_reference(location)
 
     def emit(self,
              location,
@@ -195,15 +228,21 @@ def emit(self,
         assert isinstance(extrainfo, str) or extrainfo is None
         assert isinstance(category, str) or category is None
 
+        def _loc_str(include_column=True):
+            loc = location.to_string(include_column)
+            if self.strip_prefix and loc.startswith(self.strip_prefix):
+                loc = loc[len(self.strip_prefix):]
+            return loc
+
         if self.brief:
             context = None
-            msg = "%s: trlc %s: %s" % (location.to_string(),
+            msg = "%s: trlc %s: %s" % (_loc_str(),
                                        str(kind),
                                        message)
 
         else:
             context = location.context_lines()
-            msg = "%s: %s: %s" % (location.to_string(len(context) == 0),
+            msg = "%s: %s: %s" % (_loc_str(len(context) == 0),
                                   str(kind),
                                   message)
 
@@ -216,10 +255,10 @@ def emit(self,
         else:
             if context:
                 assert len(context) == 2
-                print(context[0].replace("\t", " "))
-                print(context[1].replace("\t", " "), msg)
+                print(context[0].replace("\t", " "), file=self.out)
+                print(context[1].replace("\t", " "), msg, file=self.out)
             else:
-                print(msg)
+                print(msg, file=self.out)
 
             if not self.brief \
                and self.show_details \
@@ -230,7 +269,7 @@ def emit(self,
                     indent = 0
                 for line in extrainfo.splitlines():
                     print("%s| %s" % (" " * indent,
-                                      line.rstrip()))
+                                      line.rstrip()), file=self.out)
 
         if fatal:
             raise TRLC_Error(location, kind, message)

trlc/trlc.py

@@ -636,6 +636,14 @@ def trlc():
                            action="store_true",
                            help=("If there are no errors, produce a summary"
                                  " naming every file processed."))
+    og_output.add_argument("--log",
+                           nargs    = 2,
+                           metavar  = ("FILE", "PREFIX"),
+                           default  = None,
+                           help     = ("Write all output to FILE, strip PREFIX"
+                                       " from file paths in messages."
+                                       " Intended for use as a Bazel build"
+                                       " action."))
     og_output.add_argument("--error-on-warnings",
                            action="store_true",
                            help=("If there are warnings, return status code"
@@ -688,7 +696,10 @@ def trlc():
         except subprocess.CalledProcessError:
             ap.error("cannot run %s" % options.use_cvc5_binary)
 
-    mh = Message_Handler(options.brief, not options.no_detailed_info)
+    mh = Message_Handler(options.brief,
+                          not options.no_detailed_info,
+                          out_path     = options.log[0] if options.log else None,
+                          strip_prefix = options.log[1] if options.log else None)
 
     if options.no_user_warnings:  # pragma: no cover
         mh.suppress(Kind.USER_WARNING)
@@ -731,6 +742,7 @@ def trlc():
         ok &= sm.register_directory(".")
 
     if not ok:
+        mh.close()
         return 1
 
     if sm.process() is None:
@@ -747,7 +759,7 @@ def trlc():
                     if isinstance(tmp[obj.name][key], Fraction):
                         tmp[obj.name][key] = float(tmp[obj.name][key])
 
-            print(json.dumps(tmp, indent=2, sort_keys=True))
+            print(json.dumps(tmp, indent=2, sort_keys=True), file=mh.out)
 
     total_models = len(sm.rsl_files)
     parsed_models = len([item
@@ -791,7 +803,7 @@ def count(parsed, total, what):
     if mh.suppressed:  # pragma: no cover
         summary += " with %u supressed messages" % mh.suppressed
 
-    print(summary)
+    print(summary, file=mh.out)
 
     if options.show_file_list and ok:  # pragma: no cover
         def get_status(parser):
@@ -807,21 +819,25 @@ def get_status(parser):
             print("> %s Model %s (Package %s)" %
                   (get_status(parser),
                    filename,
-                   parser.cu.package.name))
+                   parser.cu.package.name), file=mh.out)
         if not options.skip_trlc_files:
             for filename in sorted(sm.trlc_files):
                 parser = sm.trlc_files[filename]
                 print("> %s Requirements %s (Package %s)" %
                       (get_status(parser),
                        filename,
-                       parser.cu.package.name))
+                       parser.cu.package.name), file=mh.out)
 
     if ok:
         if options.error_on_warnings and mh.warnings \
            or mh.errors:  # pragma: no cover
-            return 1
-        return 0
-    return 1
+            rv = 1
+        else:
+            rv = 0
+    else:
+        rv = 1
+    mh.close()
+    return rv
 
 
 def main():