diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 7c640ab768..14467d501c 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -6,4 +6,4 @@ inductive_cmds.cpp pp.cpp structure_cmd.cpp structure_instance.cpp init_module.cpp type_util.cpp decl_attributes.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp -brackets.cpp json.cpp typed_expr.cpp choice.cpp) +brackets.cpp typed_expr.cpp choice.cpp) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 81145ecfcb..09e3a8fb4c 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -12,5 +12,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp locals.cpp messages.cpp message_builder.cpp check.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp context_cache.cpp - scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp + scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp json.cpp pos_info_provider.cpp abstract_type_context.cpp aux_match.cpp) diff --git a/src/frontends/lean/json.cpp b/src/library/json.cpp similarity index 94% rename from src/frontends/lean/json.cpp rename to src/library/json.cpp index 1d5c59d262..dd60223d59 100644 --- a/src/frontends/lean/json.cpp +++ b/src/library/json.cpp @@ -5,14 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ #ifdef LEAN_JSON -#include "frontends/lean/json.h" +#include "library/json.h" #include #include "library/protected.h" #include "kernel/declaration.h" #include "library/type_context.h" #include "library/scoped_ext.h" #include "kernel/instantiate.h" -#include "frontends/lean/util.h" namespace lean { diff --git a/src/frontends/lean/json.h b/src/library/json.h similarity index 100% rename from src/frontends/lean/json.h rename to src/library/json.h diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index a799a38591..0f521d3533 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -21,7 +21,6 @@ add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v) endif() add_test(lean_ghash1 "${CMAKE_BINARY_DIR}/bin/lean" -g) add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash) -# add_test(lean_new_frontend "${CMAKE_BINARY_DIR}/bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean") add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean") @@ -47,17 +46,6 @@ FOREACH(T ${LEANRUNTESTS}) endif() ENDFOREACH(T) -# LEAN new frontend TESTS -file(GLOB LEANNEWFRONTENDTESTS "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend/*.lean") -FOREACH(T ${LEANNEWFRONTENDTESTS}) - if(NOT T MATCHES "\\.#") - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leannewfrontendtest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") - endif() -ENDFOREACH(T) - # LEAN COMPILER TESTS file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean") FOREACH(T ${LEANCOMPTESTS}) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 2cc45b31c9..ba82aeeaf2 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -35,13 +35,9 @@ Author: Leonardo de Moura #include "library/time_task.h" #include "library/private.h" #include "library/compiler/ir.h" -#include "frontends/lean/parser.h" -#include "frontends/lean/pp.h" -#include "frontends/lean/json.h" -#include "frontends/lean/util.h" #include "library/trace.h" +#include "library/json.h" #include "initialize/init.h" -#include "frontends/lean/simple_pos_info_provider.h" #include "library/compiler/ir_interpreter.h" #include "util/path.h" #ifdef _MSC_VER @@ -216,7 +212,6 @@ static void display_help(std::ostream & out) { std::cout << " --server start lean in server mode\n"; std::cout << " --server=file start lean in server mode, redirecting standard input from the specified file (for debugging)\n"; #endif - std::cout << " --new-frontend use new frontend\n"; std::cout << " --profile display elaboration/type checking time for each definition/theorem\n"; std::cout << " --stats display environment statistics\n"; DEBUG_CODE( @@ -247,7 +242,6 @@ static struct option g_long_options[] = { {"json", no_argument, 0, 'J'}, {"server", optional_argument, 0, 'S'}, #endif - {"new-frontend", optional_argument, 0, 'n'}, #if defined(LEAN_MULTI_THREAD) {"tstack", required_argument, 0, 's'}, #endif @@ -434,7 +428,6 @@ int main(int argc, char ** argv) { bool use_stdin = false; unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1; bool only_deps = false; - bool new_frontend = true; bool stats = false; unsigned num_threads = 0; #if defined(LEAN_MULTI_THREAD) @@ -545,9 +538,6 @@ int main(int argc, char ** argv) { lean::enable_debug(optarg); break; #endif - case 'n': - new_frontend = true; - break; case 'p': check_optarg("p"); load_plugin(optarg); @@ -576,15 +566,7 @@ int main(int argc, char ** argv) { } environment env(trust_lvl); - - io_state ios(opts, lean::mk_pretty_formatter_factory()); - - if (json_output) ios.set_regular_channel(ios.get_diagnostic_channel_ptr()); - scoped_task_manager scope_task_man(num_threads); - scope_global_ios scope_ios(ios); - type_context_old trace_ctx(env, opts); - scope_trace_env scope_trace(env, opts, trace_ctx); optional main_module_name; std::string mod_fn = ""; @@ -626,9 +608,7 @@ int main(int argc, char ** argv) { // TODO: trim auto lang_id = contents.substr(6, end_line_pos - 6); if (lang_id == "lean4") { - new_frontend = true; - } else if (lang_id == "lean4old") { - new_frontend = false; + // do nothing for now } else { std::cerr << "unknown language '" << lang_id << "'\n"; return 1; @@ -638,87 +618,30 @@ int main(int argc, char ** argv) { } bool ok = true; - if (new_frontend) { - if (!main_module_name) - main_module_name = name("_stdin"); - pair_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name); - env = r.fst(); - buffer 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 (json_output) { + if (!main_module_name) + main_module_name = name("_stdin"); + pair_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name); + env = r.fst(); + buffer 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 (json_output) { #if defined(LEAN_JSON) - for (auto msg : cpp_msgs) { - print_json(std::cout, msg); + for (auto msg : cpp_msgs) { + print_json(std::cout, msg); #endif - } - } else { - for (auto msg : cpp_msgs) { - std::cout << msg; - } } } else { - scope_traces_as_messages scope_trace_msgs(mod_fn, {1, 0}); - simple_pos_info_provider pip(mod_fn.c_str()); - scope_pos_info_provider scope_pip(pip); - message_log l; - scope_message_log scope_log(l); - std::istringstream in(contents); - object_ref imports; position pos(0, 0); message_log import_log; - std::tie(imports, pos, import_log) = parse_imports(contents, mod_fn); - // the C++ message log is printed immediately if --json is not active, so re-report all Lean message log - // messages... - for (message const & m : import_log.to_buffer()) { - report_message(m); + for (auto msg : cpp_msgs) { + std::cout << msg; } - if (import_log.has_errors()) { - return 1; - } - parser p(env, ios, in, mod_fn); - p.m_scanner.skip_to_pos(pos.to_pos_info()); - - try { - if (only_deps) { - print_deps(imports); - return 0; - } - - if (stats) { - timeit timer(std::cout, "import"); - env = import_modules(trust_lvl, opts, imports); - } else { - env = import_modules(trust_lvl, opts, imports); - } - if (main_module_name) { - env.set_main_module(*main_module_name); - } else { - env.set_main_module("_stdin"); - } - p.set_env(env); - p.parse_commands(); - } catch (lean::throwable & ex) { - report_message(lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR) - .set_exception(ex).build()); - } - - if (json_output) { -#if defined(LEAN_JSON) - for (auto const & msg : l.to_buffer()) { - print_json(std::cout, msg); -#endif - } - } else { - // Messages have already been printed directly to stdout - } - ok = !l.has_errors(); - env = p.env(); } if (stats) { @@ -727,7 +650,7 @@ int main(int argc, char ** argv) { if (run && ok) { uint32 ret = ir::run_main(env, opts, argc - optind, argv + optind); - environment_free_regions(std::move(env)); + // environment_free_regions(std::move(env)); return ret; } if (olean_fn && ok) { @@ -755,8 +678,7 @@ int main(int argc, char ** argv) { return ok ? 0 : 1; } catch (lean::throwable & ex) { - std::cerr << lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR).set_exception( - ex).build(); + std::cerr << ex.what() << "\n"; } catch (std::bad_alloc & ex) { std::cerr << "out of memory" << std::endl; } diff --git a/tests/lean/newfrontend/t1.lean b/tests/lean/newfrontend/t1.lean deleted file mode 100644 index 50ecb9dc2e..0000000000 --- a/tests/lean/newfrontend/t1.lean +++ /dev/null @@ -1,3 +0,0 @@ -variable {α : Type} -def f (a : α) : α := a -#check f 1 diff --git a/tests/lean/newfrontend/test_single.sh b/tests/lean/newfrontend/test_single.sh deleted file mode 100755 index 755d1ec72c..0000000000 --- a/tests/lean/newfrontend/test_single.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash -source ../../common.sh - -exec_check lean -j0 --new-frontend "$f"