chore: remove --json option

nix/lean-dev.in

@@ -2,22 +2,6 @@
 set -euo pipefail
 PATH=@nix@/bin:$PATH
 
-call() {
-    if [[ $json == 1 ]]; then
-        $@ 2>&1 | awk '
-/{/ { print $0; next }
-# Hide some Nix warnings. You will still see them with `nix build` etc., but they are pretty annoying in the editor.
-/warning: ignoring/ { next }
-{
-  gsub(/"/, "\\\"", $0);
-  gsub(/\n/, "\\n", $0);
-  printf "{\"severity\": \"error\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"<stdin>\", \"text\": \"%s\"}\n", $0 }'
-    else
-        $@
-    fi
-}
-
-json=0
 input=
 inputFile=
 server=0
@@ -27,7 +11,6 @@ deps=
 args=(-- "$@")
 for p in "$@"; do
     case "$p" in
-        --json) json=1;;
         --stdin) input="$(< /dev/stdin)";;
         --server)
             server=1
@@ -65,7 +48,7 @@ for dep in $deps; do
     target="$target.\"$dep\""
 done
 if [[ -z "$input" ]]; then
-    call nix run "$target" ${args[*]}
+    nix run "$target" ${args[*]}
 else
-    echo -n "$input" | call nix run "$target" ${args[*]}
+    echo -n "$input" | nix run "$target" ${args[*]}
 fi

src/CMakeLists.txt

@@ -32,8 +32,6 @@ option(MULTI_THREAD       "MULTI_THREAD"       ON)
 option(CCACHE             "use ccache"         ON)
 option(STATIC             "STATIC"             OFF)
 option(SPLIT_STACK        "SPLIT_STACK"        OFF)
-# When OFF we disable JSON support to support older compilers
-option(JSON               "JSON"               ON)
 # When OFF we disable LLVM support
 option(LLVM               "LLVM"               OFF)
 option(COMPRESSED_OBJECT_HEADER "Use compressed object headers in 64-bit machines, this option is ignored in 32-bit machines, and assumes the 64-bit OS can only address 2^48 bytes" ON)
@@ -157,12 +155,6 @@ if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin"))
   set(LEAN_EXTRA_MAKE_OPTS -s40000 ${LEAN_EXTRA_MAKE_OPTS})
 endif ()
 
-if(JSON)
-  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_JSON")
-else()
-  message(WARNING "Disabling JSON support, compile server will not be available")
-endif()
-
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
   set(AUTO_THREAD_FINALIZATION OFF)

src/Lean/Elab/Frontend.lean

@@ -82,18 +82,15 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
   pure (s.commandState.env, s.commandState.messages)
 
-@[export lean_process_input]
-def processExport (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do
-  let (env, messages) ← process input env opts fileName
-  pure (env, messages.toList)
-
 @[export lean_run_frontend]
-def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) : IO (Environment × List Message × Module) := do
+def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) : IO (Environment × Bool) := do
   let inputCtx := Parser.mkInputContext input fileName
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let (env, messages) ← processHeader header opts messages inputCtx
   let env := env.setMainModule mainModuleName
   let s ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
-  pure (s.commandState.env, s.commandState.messages.toList, { header := header, commands := s.commands })
+  for msg in s.commandState.messages.toList do
+    IO.print (← msg.toString)
+  pure (s.commandState.env, !s.commandState.messages.hasErrors)
 
 end Lean.Elab

src/library/CMakeLists.txt

@@ -7,5 +7,5 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
   aux_recursors.cpp trace.cpp
   messages.cpp message_builder.cpp
   profiling.cpp time_task.cpp
-  formatter.cpp json.cpp
+  formatter.cpp
   abstract_type_context.cpp)

src/library/json.cpp

@@ -1,45 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Gabriel Ebner
-*/
-#ifdef LEAN_JSON
-#include "library/json.h"
-#include <string>
-#include "library/protected.h"
-#include "kernel/declaration.h"
-#include "kernel/instantiate.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_filename();
-    j["pos_line"]  = msg.get_pos().first;
-    j["pos_col"]   = msg.get_pos().second;
-    if (auto end_pos = msg.get_end_pos()) {
-        j["end_pos_line"] = end_pos->first;
-        j["end_pos_col"]  = end_pos->second;
-    }
-    j["severity"]  = json_of_severity(msg.get_severity());
-    j["caption"]   = msg.get_caption();
-    j["text"]      = msg.get_text();
-    return j;
-}
-
-void print_json(std::ostream & out, message const & msg) {
-    out << json_of_message(msg) << std::endl;
-}
-
-}
-#endif

src/library/json.h

@@ -1,24 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Gabriel Ebner
-*/
-#ifdef LEAN_JSON
-#pragma once
-#include "library/messages.h"
-#include "kernel/environment.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);
-
-void print_json(std::ostream &, message const & msg);
-
-}
-#endif

src/shell/lean.cpp

@@ -34,7 +34,6 @@ Author: Leonardo de Moura
 #include "library/time_task.h"
 #include "library/compiler/ir.h"
 #include "library/trace.h"
-#include "library/json.h"
 #include "library/print.h"
 #include "initialize/init.h"
 #include "library/compiler/ir_interpreter.h"
@@ -162,8 +161,6 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
 
 using namespace lean; // NOLINT
 
-// object * lean_process_file(object * filename, object * contents, uint8 json, object * env, object * world);
-
 #ifndef LEAN_SERVER_DEFAULT_MAX_MEMORY
 #define LEAN_SERVER_DEFAULT_MAX_MEMORY 1024
 #endif
@@ -203,14 +200,11 @@ static void display_help(std::ostream & out) {
 #if defined(LEAN_MULTI_THREAD)
     std::cout << "  --threads=num -j   number of threads used to process lean files\n";
     std::cout << "  --tstack=num -s    thread stack size in Kb\n";
-#endif
-    std::cout << "  --plugin=file      load and initialize shared library for registering linters etc.\n";
-    std::cout << "  --deps             just print dependencies of a Lean input\n";
-#if defined(LEAN_JSON)
-    std::cout << "  --json             print JSON-formatted structured error messages\n";
     std::cout << "  --server           start lean in server mode\n";
     std::cout << "  --worker           start lean in server-worker mode\n";
 #endif
+    std::cout << "  --plugin=file      load and initialize shared library for registering linters etc.\n";
+    std::cout << "  --deps             just print dependencies of a Lean input\n";
     std::cout << "  --profile          display elaboration/type checking time for each definition/theorem\n";
     std::cout << "  --stats            display environment statistics\n";
     DEBUG_CODE(
@@ -231,19 +225,16 @@ static struct option g_long_options[] = {
     {"trust",        required_argument, 0, 't'},
     {"profile",      no_argument,       0, 'P'},
     {"stats",        no_argument,       0, 'a'},
-    {"threads",      required_argument, 0, 'j'},
     {"quiet",        no_argument,       0, 'q'},
     {"deps",         no_argument,       0, 'd'},
     {"timeout",      optional_argument, 0, 'T'},
     {"c",            optional_argument, 0, 'c'},
     {"exitOnPanic",  no_argument,       0, 'e'},
-#if defined(LEAN_JSON)
-    {"json",         no_argument,       0, 'J'},
+#if defined(LEAN_MULTI_THREAD)
+    {"threads",      required_argument, 0, 'j'},
+    {"tstack",       required_argument, 0, 's'},
     {"server",       no_argument,       0, 'S'},
     {"worker",       no_argument,       0, 'W'},
-#endif
-#if defined(LEAN_MULTI_THREAD)
-    {"tstack",       required_argument, 0, 's'},
 #endif
     {"plugin",       required_argument, 0, 'p'},
 #ifdef LEAN_DEBUG
@@ -333,11 +324,9 @@ public:
 };
 
 namespace lean {
-typedef list_ref<object_ref> messages;
-typedef object_ref module_stx;
 extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, object * w);
-pair_ref<environment, pair_ref<messages, module_stx>> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) {
-    return get_io_result<pair_ref<environment, pair_ref<messages, module_stx>>>(
+pair_ref<environment, object_ref> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) {
+    return get_io_result<pair_ref<environment, object_ref>>(
         lean_run_frontend(mk_string(input), opts.to_obj_arg(), mk_string(file_name), main_module_name.to_obj_arg(), io_mk_world()));
 }
 
@@ -455,9 +444,6 @@ int main(int argc, char ** argv) {
 #if defined(LEAN_MULTI_THREAD)
     num_threads = hardware_concurrency();
 #endif
-#if defined(LEAN_JSON)
-    bool json_output = false;
-#endif
 #if defined(LEAN_LLVM)
     // Initialize LLVM backends for native code generation.
     llvm::InitializeNativeTarget();
@@ -545,18 +531,12 @@ int main(int argc, char ** argv) {
                     return 1;
                 }
                 break;
-#if defined(LEAN_JSON)
-            case 'J':
-                opts = opts.update(lean::name{"trace", "as_messages"}, true);
-                json_output = true;
-                break;
             case 'S':
                 run_server = 1;
                 break;
             case 'W':
                 run_server = 2;
                 break;
-#endif
             case 'P':
                 opts = opts.update("profiler", true);
                 break;
@@ -652,33 +632,11 @@ int main(int argc, char ** argv) {
             contents.erase(0, end_line_pos);
         }
 
-        bool ok = true;
         if (!main_module_name)
             main_module_name = name("_stdin");
-        pair_ref<environment, pair_ref<messages, module_stx>> r = run_new_frontend(contents, opts, mod_fn, *main_module_name);
+        pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name);
         env = r.fst();
-        buffer<message> cpp_msgs;
-        // HACK: convert Lean Message into C++ message
-        for (auto msg : r.snd().fst()) {
-            pos_info pos = get_message_pos(msg);
-            message_severity sev = get_message_severity(msg);
-            if (sev == message_severity::ERROR)
-                ok = false;
-            std::string str = get_message_string(msg);
-            cpp_msgs.push_back(message(mod_fn, pos, sev, str));
-        }
-#if defined(LEAN_JSON)
-        if (json_output) {
-            for (auto msg : cpp_msgs) {
-                print_json(std::cout, msg);
-            }
-        } else
-#endif
-        {
-            for (auto msg : cpp_msgs) {
-                std::cout << msg;
-            }
-        }
+        bool ok = unbox(r.snd().raw());
 
         if (stats) {
             env.display_stats();
@@ -709,10 +667,7 @@ int main(int argc, char ** argv) {
             out.close();
         }
 
-#ifdef LEAN_JSON
-        if (!json_output)
-#endif
-            display_cumulative_profiling_times(std::cerr);
+        display_cumulative_profiling_times(std::cerr);
 
         return ok ? 0 : 1;
     } catch (lean::throwable & ex) {