feat(shell/json): json-formatted error messages

src/shell/CMakeLists.txt

@@ -2,7 +2,7 @@ if(${EMSCRIPTEN})
   add_executable(lean.js lean.cpp emscripten.cpp ${LEAN_OBJS})
   target_link_libraries(lean.js ${EXTRA_LIBS} "--embed-file library --memory-init-file 0")
 else()
-  add_executable(lean lean.cpp emscripten.cpp)
+  add_executable(lean lean.cpp emscripten.cpp json.cpp)
   target_link_libraries(lean leanstatic ${EXTRA_LIBS})
   ADD_CUSTOM_COMMAND(TARGET lean
     POST_BUILD

src/shell/json.cpp

@@ -0,0 +1,35 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#include "shell/json.h"
+
+namespace lean {
+
+json json_of_severity(message_severity sev) {
+    switch (sev) {
+        case INFORMATION: return "information";
+        case WARNING:     return "warning";
+        case ERROR:       return "error";
+        default: lean_unreachable();
+    }
+}
+
+json json_of_message(message const & msg) {
+    json j;
+    j["file_name"] = msg.get_file_name();
+    j["pos_line"]  = msg.get_pos().first;
+    j["pos_col"]   = msg.get_pos().second;
+    j["severity"]  = json_of_severity(msg.get_severity());
+    j["caption"]   = msg.get_caption();
+    j["text"]      = msg.get_text();
+    return j;
+}
+
+void json_message_stream::report(message const & msg) {
+    m_out << json_of_message(msg) << std::endl;
+}
+
+}

src/shell/json.h

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#pragma once
+
+#include "library/messages.h"
+#include "util/json.hpp"
+
+namespace lean {
+
+using json = nlohmann::json;
+
+json json_of_severity(message_severity sev);
+
+json json_of_message(message const & msg);
+
+class json_message_stream : public message_stream {
+    std::ostream & m_out;
+public:
+    json_message_stream(std::ostream & out) : m_out(out) {}
+    ~json_message_stream() {}
+    void report(message const & msg) override;
+};
+
+}

src/shell/lean.cpp

@@ -41,6 +41,7 @@ Author: Leonardo de Moura
 #include "init/init.h"
 #include "shell/emscripten.h"
 #include "shell/simple_pos_info_provider.h"
+#include "shell/json.h"
 #include "version.h"
 #include "githash.h" // NOLINT
 
@@ -98,6 +99,7 @@ static void display_help(std::ostream & out) {
 #endif
     std::cout << "  --deps            just print dependencies of a Lean input\n";
     std::cout << "  --flycheck        print structured error message for flycheck\n";
+    std::cout << "  --json            print JSON-formatted structured error messages\n";
     std::cout << "  --cache=file -c   load/save cached definitions from/to the given file\n";
     std::cout << "  --profile         display elaboration/type checking time for each definition/theorem\n";
 #if defined(LEAN_USE_BOOST)
@@ -138,6 +140,7 @@ static struct option g_long_options[] = {
     {"cache",        required_argument, 0, 'c'},
     {"deps",         no_argument,       0, 'd'},
     {"flycheck",     no_argument,       0, 'F'},
+    {"json",         no_argument,       0, 'J'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",       required_argument, 0, 's'},
 #endif
@@ -223,6 +226,7 @@ int main(int argc, char ** argv) {
     bool read_cache         = false;
     bool save_cache         = false;
     bool flycheck           = false;
+    bool json_output        = false;
     options opts;
     std::string output;
     std::string cache_name;
@@ -294,6 +298,10 @@ int main(int argc, char ** argv) {
             opts = opts.update(lean::name{"trace", "as_messages"}, true);
             flycheck = true;
             break;
+        case 'J':
+            opts = opts.update(lean::name{"trace", "as_messages"}, true);
+            json_output = true;
+            break;
         case 'P':
             opts = opts.update("profile", true);
             break;
@@ -358,6 +366,11 @@ int main(int argc, char ** argv) {
         // Redirect uncaptured non-flycheck messages to stdout
         ios.set_regular_channel(ios.get_diagnostic_channel_ptr());
     }
+    if (json_output) {
+        ios.set_message_channel(std::make_shared<lean::json_message_stream>(std::cout));
+        // Redirect uncaptured non-flycheck messages to stdout
+        ios.set_regular_channel(ios.get_diagnostic_channel_ptr());
+    }
 
     if (smt2) {
         // Note: the smt2 flag may override other flags