From 1f601708e4aa7a722f2d46b6ffb48db5ceea70e6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 10 Nov 2019 13:40:48 +0100
Subject: [PATCH] fix: print messages to stderr

This ensures that errors during dependency resolution in the Makefile actually show up
---
 src/library/messages.cpp    | 2 +-
 tests/lean/test_single.sh   | 2 +-
 tests/plugin/test_single.sh | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/library/messages.cpp b/src/library/messages.cpp
index 2694e73578..c45d6645dd 100644
--- a/src/library/messages.cpp
+++ b/src/library/messages.cpp
@@ -34,7 +34,7 @@ std::ostream & operator<<(std::ostream & out, message const & msg) {
 void report_message(message const & msg0) {
     if (!get_global_ios().get_options().get_bool(name {"trace", "as_messages"}, false)) {
         // Print immediately. Still add as a message so that we get the error code correct.
-        get_global_ios().get_regular_stream() << msg0;
+        get_global_ios().get_diagnostic_stream() << msg0;
     }
     lean_assert(global_message_log());
     global_message_log()->add(msg0);
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index 8a3edf2438..61ecad6b7d 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -26,7 +26,7 @@ if diff --color --help >/dev/null 2>&1; then
 fi
 
 echo "-- testing $f"
-"$LEAN" "$ff" | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out"
+"$LEAN" "$ff" 2>&1 | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
         echo "-- checked"
diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh
index 11600b8801..e4316057a8 100755
--- a/tests/plugin/test_single.sh
+++ b/tests/plugin/test_single.sh
@@ -37,7 +37,7 @@ if [ $? -ne 0 ]; then
     exit 1
 fi
 
-$BIN_DIR/lean --plugin="$ff.so" "$ff" | sed "s|^$ff|$f|" > "$f.produced.out"
+$BIN_DIR/lean --plugin="$ff.so" "$ff" 2>&1 | sed "s|^$ff|$f|" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
         echo "-- checked"