From 0c9c4be4aeb95d4daed5c4c9931b75d4d187de3c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 3 Oct 2016 15:19:02 +0200
Subject: [PATCH] bin: workaround flushing issues

* bin/common_cout.cc (check_cout): Force a flush of cout if more than
20ms has elapsed since the last explicit flush.
* bin/common_setup.cc (setup): Untie cin and cout if the input
is not a TTY, so that cout is flush less often.
* NEWS: Mention the change.
---
 NEWS                |  8 ++++++++
 bin/common_cout.cc  | 36 ++++++++++++++++++++++++++++++------
 bin/common_setup.cc |  6 ++++++
 3 files changed, 44 insertions(+), 6 deletions(-)

diff --git a/NEWS b/NEWS
index 6960c6da5..024ece6a1 100644
--- a/NEWS
+++ b/NEWS
@@ -13,6 +13,14 @@ New in spot 2.1.1.dev (not yet released)
   - Fix spurious uninitialized read reported by valgrind when
     is_Kleene_star() is compiled by clang++.
 
+  - Using "ltlfilt some-large-file --some-costly-filter" could take
+    to a lot of time before displaying the first results, because the
+    output of ltlfilt is buffered: the buffer had to fill up before
+    being flushed.  The issue did not manifest when the input is
+    standard input, because of the C++ feature that reading std::cin
+    should flush std::cout; however it was well visible when reading
+    from files.  Flushing is now done more regularly.
+
 New in spot 2.1.1 (2016-09-20)
 
   Command-line tools:
diff --git a/bin/common_cout.cc b/bin/common_cout.cc
index 887ea8f5c..2f5ada858 100644
--- a/bin/common_cout.cc
+++ b/bin/common_cout.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2016 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -20,18 +20,42 @@
 #include "common_sys.hh"
 #include "common_cout.hh"
 #include <iostream>
+#include <chrono>
 #include "error.h"
 
+namespace
+{
+  static std::chrono::steady_clock::time_point last_flush;
+
+  static void do_check_cout()
+  {
+    // Make sure we abort if we can't write to std::cout anymore
+    // (like disk full or broken pipe with SIGPIPE ignored).
+    if (!std::cout)
+      error(2, 0, "error writing to standard output");
+  }
+}
+
 void check_cout()
 {
-  // Make sure we abort if we can't write to std::cout anymore
-  // (like disk full or broken pipe with SIGPIPE ignored).
-  if (!std::cout)
-    error(2, 0, "error writing to standard output");
+  // If we haven't flushed explicitly for more than 20ms, do it now.
+  // Otherwise we would have to wait for the buffer to fill up, and
+  // this could take a long time.
+  auto now = std::chrono::steady_clock::now();
+  auto ms =
+    std::chrono::duration_cast<std::chrono::milliseconds>(now - last_flush);
+  if (ms.count() >= 20)
+    {
+      last_flush = now;
+      std::cout.flush();
+    }
+
+  do_check_cout();
 }
 
 void flush_cout()
 {
+  last_flush = std::chrono::steady_clock::now();
   std::cout.flush();
-  check_cout();
+  do_check_cout();
 }
diff --git a/bin/common_setup.cc b/bin/common_setup.cc
index 150375d9d..63e191f5e 100644
--- a/bin/common_setup.cc
+++ b/bin/common_setup.cc
@@ -22,6 +22,7 @@
 
 #include "argp.h"
 #include <cstdlib>
+#include <unistd.h>
 #include <iostream>
 #include <signal.h>
 #include <sys/wait.h>
@@ -83,6 +84,11 @@ setup(char** argv)
   argp_err_exit_status = 2;
 
   std::ios_base::sync_with_stdio(false);
+  // Do not flush std::cout every time we read from std::cin, unless
+  // we are reading from a terminal.  Note that we do flush regularly
+  // in check_cout().
+  if (!isatty(STDIN_FILENO))
+    std::cin.tie(nullptr);
 
   setup_default_output_format();
   setup_sig_handler();