max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove old frontend support from lean.cpp

Browse source 
We also remove the option `-n` (for new frontend)
This commit is contained in:
Leonardo de Moura 2020-10-25 10:16:52 -07:00
parent 2be41ad0ad
commit e28b337a2c
8 changed files with 26 additions and 124 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/CMakeLists.txt
View file

@ -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)

2
src/library/CMakeLists.txt
View file

@ -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)

3
src/frontends/lean/json.cpp → src/library/json.cpp
View file

@ -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 <string>
#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 {

0
src/frontends/lean/json.h → src/library/json.h
View file

12
src/shell/CMakeLists.txt
View file

@ -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})

124
src/shell/lean.cpp
View file

@ -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<name> main_module_name;
std::string mod_fn = "<unknown>";
@ -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<environment, pair_ref<messages, module_stx>> 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 (json_output) {
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);
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 (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;
}

3
tests/lean/newfrontend/t1.lean
View file

@ -1,3 +0,0 @@
variable {α : Type}
def f (a : α) : α := a
#check f 1

4
tests/lean/newfrontend/test_single.sh
View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
source ../../common.sh
exec_check lean -j0 --new-frontend "$f"