From 45da5872e6216ecaa925e72fc6ce86d4858bbcdc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Jun 2018 16:18:46 -0700 Subject: [PATCH] chore(checker): remove `leanchecker` --- src/CMakeLists.txt | 1 - src/checker/CMakeLists.txt | 5 - src/checker/checker.cpp | 138 ---------------- src/checker/simple_pp.cpp | 311 ------------------------------------ src/checker/simple_pp.h | 18 --- src/checker/text_import.cpp | 208 ------------------------ src/checker/text_import.h | 28 ---- src/shell/CMakeLists.txt | 6 - 8 files changed, 715 deletions(-) delete mode 100644 src/checker/CMakeLists.txt delete mode 100644 src/checker/checker.cpp delete mode 100644 src/checker/simple_pp.cpp delete mode 100644 src/checker/simple_pp.h delete mode 100644 src/checker/text_import.cpp delete mode 100644 src/checker/text_import.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4eb1afc576..74246d9075 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -399,7 +399,6 @@ add_subdirectory(kernel) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel/inductive) set(LEAN_OBJS ${LEAN_OBJS} $) -add_subdirectory(checker) add_subdirectory(library) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/tactic) diff --git a/src/checker/CMakeLists.txt b/src/checker/CMakeLists.txt deleted file mode 100644 index f5bf68f931..0000000000 --- a/src/checker/CMakeLists.txt +++ /dev/null @@ -1,5 +0,0 @@ -add_executable(leanchecker checker.cpp text_import.cpp simple_pp.cpp - $ $ $ - $ $) -target_link_libraries(leanchecker ${EXTRA_LIBS}) -install(TARGETS leanchecker DESTINATION bin) diff --git a/src/checker/checker.cpp b/src/checker/checker.cpp deleted file mode 100644 index aa9cfdbf4d..0000000000 --- a/src/checker/checker.cpp +++ /dev/null @@ -1,138 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Gabriel Ebner -*/ -#include -#include "runtime/sstream.h" -#include "util/init_module.h" -#include "util/test.h" -#include "util/sexpr/init_module.h" -#include "kernel/init_module.h" -#include "kernel/inductive/inductive.h" -#include "kernel/standard_kernel.h" -#include "kernel/for_each_fn.h" -#include "library/formatter.h" -#include "checker/text_import.h" -#include "checker/simple_pp.h" - -#if defined(LEAN_EMSCRIPTEN) -#include -#endif - -using namespace lean; // NOLINT - -struct checker_print_fn { - std::ostream & m_out; - environment m_env; - lowlevel_notations m_notations; - std::unordered_set m_already_printed; - - checker_print_fn(std::ostream & out, environment const & env, lowlevel_notations const & nots) : - m_out(out), m_env(env), m_notations(nots) {} - - format pp(expr const & e) { - return simple_pp(m_env, e, m_notations); - } - - void print_decl(declaration const & d) { - format fn = compose_many({simple_pp(d.get_name()), space(), format(":"), space(), pp(d.get_type())}); - - if (d.is_definition() && !d.is_theorem()) { - m_out << compose_many({format("def"), space(), fn, space(), format(":="), line(), pp(d.get_value()), line()}); - } else { - format cmd(d.is_theorem() ? "theorem" : (d.is_axiom() ? "axiom" : "constant")); - m_out << compose_many({cmd, space(), fn, line()}); - } - } - - void print_axioms(declaration const & decl) { - print_axioms(decl.get_type()); - if (decl.is_definition()) print_axioms(decl.get_value()); - } - - void print_axioms(expr const & ex) { - for_each(ex, [&] (expr const & e, unsigned) { - if (is_constant(e) && !m_already_printed.count(const_name(e))) { - auto decl = m_env.get(const_name(e)); - m_already_printed.insert(decl.get_name()); - print_axioms(decl); - if (decl.is_constant_assumption() && !m_env.is_builtin(decl.get_name())) - print_decl(decl); - } - return true; - }); - } - - void handle_cmdline_args(buffer const & ns) { - for (auto & n : ns) print_axioms(m_env.get(n)); - for (auto & n : ns) print_decl(m_env.get(n)); - } -}; - -int main(int argc, char ** argv) { -#if defined(LEAN_EMSCRIPTEN) - EM_ASM( - try { - // emscripten cannot mount all of / in the vfs, - // we can only mount subdirectories... - FS.mount(NODEFS, { root: '/home' }, '/home'); - FS.mkdir('/root'); - FS.mount(NODEFS, { root: '/root' }, '/root'); - - FS.chdir(process.cwd()); - } catch (e) { - console.log(e); - }); -#endif - - if (argc < 2) { - std::cout << "usage: leanchecker export.out lemma_to_print" << std::endl; - return 1; - } - - struct initer { - initer() { - save_stack_info(); - initialize_util_module(); - initialize_sexpr_module(); - initialize_kernel_module(); - initialize_inductive_module(); - } - ~initer() { - finalize_inductive_module(); - finalize_kernel_module(); - finalize_sexpr_module(); - finalize_util_module(); - } - } initer; - - try { - std::ifstream in(argv[1]); - if (!in) throw exception(sstream() << "file not found: " << argv[1]); - - unsigned trust_lvl = 0; - auto env = mk_environment(trust_lvl); - lowlevel_notations notations; - import_from_text(in, env, notations); - - buffer to_print; - for (int i = 2; i < argc; i++) - to_print.push_back(string_to_name(argv[i])); - - checker_print_fn(std::cout, env, notations).handle_cmdline_args(to_print); - - unsigned num_decls = 0; - env.for_each_declaration([&] (declaration const &) { num_decls++; }); - std::cout << "checked " << num_decls << " declarations" << std::endl; - - return 0; - } catch (throwable & ex) { - std::cerr << ex.what() << std::endl; - return 1; - } catch (std::exception & ex) { - std::cerr << ex.what() << std::endl; - return 1; - } -} diff --git a/src/checker/simple_pp.cpp b/src/checker/simple_pp.cpp deleted file mode 100644 index a9964986c3..0000000000 --- a/src/checker/simple_pp.cpp +++ /dev/null @@ -1,311 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Gabriel Ebner -*/ -#include "checker/simple_pp.h" -#include "kernel/instantiate.h" -#include "kernel/old_type_checker.h" -#include "kernel/for_each_fn.h" - -namespace lean { - -format compose_many(std::initializer_list const & fmts) { - format res; - bool first = true; - for (auto & fmt : fmts) { - if (first) { - res = fmt; - first = false; - } else { - res = compose(res, fmt); - } - } - return res; -} - -static format pp_name(name n) { - bool last = true; - format fmt; - while (n) { - auto limb = n.is_numeral() ? format(n.get_numeral()) : format(n.get_string()); - fmt = last ? limb : compose_many({limb, format("."), fmt}); - last = false; - n = n.get_prefix(); - } - return last ? format("[anonymous]") : fmt; -} - -struct simple_pp_fn { - old_type_checker m_tc; - lowlevel_notations m_notations; - unsigned m_indent = 0; - - simple_pp_fn(environment const & env, lowlevel_notations const & notations) : - m_tc(env), m_notations(notations) {} - - static constexpr unsigned MAX_PRIO = 1024; - struct result { - format m_fmt; - unsigned m_prio; - - result(format const & fmt, unsigned prio) : m_fmt(fmt), m_prio(prio) {} - result(format const & fmt) : m_fmt(fmt), m_prio(MAX_PRIO) {} - - result maybe_paren() const { return maybe_paren(MAX_PRIO); } - result maybe_paren(unsigned new_prio) const { - if (m_prio < new_prio) { - return paren(m_fmt); - } else { - return *this; - } - } - - operator format() const { return m_fmt; } - }; - - result pp_meta(name const & n) { - return compose(format("?"), pp_name(n)); - } - - result pp_level(level const & l) { - switch (l.kind()) { - case level_kind::Zero: return format("0"); - case level_kind::Succ: return result(compose(pp_level(succ_of(l)).maybe_paren(1), format("+1")), 0); - case level_kind::Max: - return result(compose_many({format("max"), space(), - pp_level(max_lhs(l)).maybe_paren(1), - pp_level(max_rhs(l)).maybe_paren(1)}), 0); - case level_kind::IMax: - return result(compose_many({format("imax"), space(), - pp_level(imax_lhs(l)).maybe_paren(1), - pp_level(imax_rhs(l)).maybe_paren(1)}), 0); - case level_kind::Param: return pp_name(param_id(l)); - case level_kind::Meta: return pp_meta(meta_id(l)); - } - lean_unreachable(); - } - - result pp_var(expr const & e) { - return compose(format("#"), format(var_idx(e))); - } - - result pp_sort(expr const & e) { - if (sort_level(e) == mk_level_zero()) { - return format("Prop"); - } else if (sort_level(e) == mk_level_one()) { - return format("Type"); - } else if (is_succ(sort_level(e))) { - return compose_many({format("Type"), space(), pp_level(succ_of(sort_level(e))).maybe_paren()}); - } else { - return compose_many({format("Sort"), space(), pp_level(sort_level(e)).maybe_paren()}); - } - } - - result pp_const(expr const & e) { - return pp_name(const_name(e)); - } - - result pp_meta(expr const & e) { - return pp_meta(mlocal_name(e)); - } - - result pp_local(expr const & e) { - return pp_name(mlocal_pp_name(e)); - } - - bool is_implicit(expr const & f) { - if (!closed(f)) { - // the Lean type checker assumes expressions are closed. - return false; - } - try { - expr t = m_tc.relaxed_whnf(m_tc.infer(f)); - if (is_pi(t)) { - binder_info bi = binding_info(t); - return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit(); - } else { - return false; - } - } catch (exception &) { - return false; - } - } - - expr get_explicit_args(expr e, buffer & args) { - while (is_app(e)) { - if (!is_implicit(app_fn(e))) { - args.push_back(app_arg(e)); - } - e = app_fn(e); - } - std::reverse(args.begin(), args.end()); - return e; - } - - result pp_app(expr const & e) { - buffer args; - auto fn = get_explicit_args(e, args); - - if (is_constant(fn)) { - auto it = m_notations.find(const_name(fn)); - if (it != m_notations.end()) { - format fmt; - auto prec = it->second.m_prec; - if (it->second.m_kind == lowlevel_notation_kind::Postfix && args.size() == 1) { - fmt = compose_many({pp(args[0]).maybe_paren(prec), format(it->second.m_token)}); - } - if (it->second.m_kind == lowlevel_notation_kind::Prefix && args.size() == 1) { - fmt = compose_many({format(it->second.m_token), pp(args[0]).maybe_paren(prec)}); - } - if (it->second.m_kind == lowlevel_notation_kind::Infix && args.size() == 2) { - fmt = compose_many({pp(args[0]).maybe_paren(prec), - format(it->second.m_token), - pp(args[1]).maybe_paren(prec)}); - } - if (!fmt.is_nil_fmt()) - return result(group(fmt), it->second.m_prec-1); - } - } - - format fmt = pp(fn).maybe_paren(); - for (auto & arg : args) { - fmt = compose_many({fmt, space(), pp(arg).maybe_paren()}); - } - return result(group(fmt), MAX_PRIO-1); - } - - std::unordered_set used_names; - name get_unused(name n) { - if (!used_names.count(n)) return n; - - n = n.get_subscript_base(); - for (unsigned i = 1;; i++) { - auto n_i = n.append_after(i); - if (!used_names.count(n_i)) - return n_i; - } - } - - struct local_const { - simple_pp_fn * m_fn; - name m_pp_name; - expr m_lc; - - local_const(simple_pp_fn * fn, name pp_name, expr const & domain, binder_info const & bi) : m_fn(fn) { - m_pp_name = m_fn->get_unused(pp_name); - m_fn->used_names.insert(m_pp_name); - m_lc = mk_local(m_pp_name, m_pp_name, domain, bi); - m_fn->m_tc.push_local(m_pp_name, domain, bi); - } - ~local_const() { - m_fn->used_names.erase(m_pp_name); - m_fn->m_tc.pop_local(); - } - - expr const & domain() const { return mlocal_type(m_lc); } - - local_const(simple_pp_fn * fn, expr const & binder) : - local_const(fn, binding_name(binder), binding_domain(binder), binding_info(binder)) {} - }; - - void mark_used_const_names(expr const & e) { - for_each(e, [&] (expr const & c, unsigned) { - if (is_constant(c)) - used_names.insert(const_name(c)); - return true; - }); - } - - format wrap_binder(std::initializer_list const & fmts, binder_info const & bi) { - auto fmt = compose_many(fmts); - if (bi.is_implicit()) { - return compose_many({format("{"), fmt, format("}")}); - } else if (bi.is_strict_implicit()) { - return compose_many({format("{{"), fmt, format("}}")}); - } else if (bi.is_inst_implicit()) { - return compose_many({format("["), fmt, format("]")}); - } else { - return fmt; - } - } - - result pp_lambda(expr const & e) { - local_const lc(this, e); - return result(group(compose_many({format("λ"), space(), - wrap_binder({pp(lc.m_lc), space(), format(":"), space(), - pp(binding_domain(e)).maybe_paren(1)}, binding_info(e)), - format(","), space(), pp(instantiate(binding_body(e), lc.m_lc))})), 0); - } - - result pp_pi(expr e) { - if (!has_free_vars(binding_body(e))) { - // implication - return result(group(compose_many({pp(binding_domain(e)).maybe_paren(25), space(), format("->"), - space(), pp(binding_body(e)).maybe_paren(24)})), 24); - } else { - auto bi = binding_info(e); - auto ty = binding_domain(e); - - buffer lcs; - do { - lcs.emplace_back(this, e); - e = instantiate(binding_body(e), lcs.back().m_lc); - } while (is_pi(e) && has_free_vars(binding_body(e)) && - binding_info(e) == bi && - m_tc.is_def_eq(binding_domain(e), ty)); - - format bound_vars; - for (auto & lc : lcs) { - if (!bound_vars.is_nil_fmt()) bound_vars = compose(bound_vars, space()); - bound_vars = compose_many({bound_vars, pp_name(lc.m_pp_name)}); - } - - auto fmt = compose_many({format("Π"), space(), - wrap_binder({bound_vars, space(), format(":"), space(), - pp(ty).maybe_paren(1)}, bi), - format(","), space(), pp(e)}); - return result(group(fmt), 0); - } - } - - result pp_macro(expr const &) { - return format("[macro]"); - } - - result pp_let(expr const & e) { - local_const lc(this, let_name(e), let_type(e), binder_info()); - return result(group(compose_many({format("let"), space(), pp(lc.m_lc), space(), format(":"), space(), - pp(let_type(e)).maybe_paren(1), space(), format(":="), space(), pp(let_value(e)), format(","), - space(), pp(instantiate(let_body(e), lc.m_lc))})), 0); - } - - result pp(expr const & e) { - switch (e.kind()) { - case expr_kind::Var: return pp_var(e); - case expr_kind::Sort: return pp_sort(e); - case expr_kind::Constant: return pp_const(e); - case expr_kind::Meta: return pp_meta(e); - case expr_kind::Local: return pp_local(e); - case expr_kind::App: return pp_app(e); - case expr_kind::Lambda: return pp_lambda(e); - case expr_kind::Pi: return pp_pi(e); - case expr_kind::Macro: return pp_macro(e); - case expr_kind::Let: return pp_let(e); - } - lean_unreachable(); - } -}; - -format simple_pp(name const & n) { - return pp_name(n); -} - -format simple_pp(environment const & env, expr const & e, lowlevel_notations const & notations) { - simple_pp_fn fn(env, notations); - fn.mark_used_const_names(e); - return fn.pp(e); -} - -} diff --git a/src/checker/simple_pp.h b/src/checker/simple_pp.h deleted file mode 100644 index 7d020c34bc..0000000000 --- a/src/checker/simple_pp.h +++ /dev/null @@ -1,18 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Gabriel Ebner -*/ -#pragma once -#include "kernel/environment.h" -#include "checker/text_import.h" - -namespace lean { - -format compose_many(std::initializer_list const & fmts); - -format simple_pp(name const & n); -format simple_pp(environment const & env, expr const & e, lowlevel_notations const & notations); - -} diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp deleted file mode 100644 index 28ee6d318b..0000000000 --- a/src/checker/text_import.cpp +++ /dev/null @@ -1,208 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Gabriel Ebner -*/ -#include -#include -#include -#include "runtime/sstream.h" -#include "kernel/environment.h" -#include "kernel/inductive/inductive.h" -#include "kernel/old_type_checker.h" -#include "kernel/quot.h" -#include "checker/text_import.h" - -namespace lean { - -struct text_importer { - std::unordered_map m_expr; - std::unordered_map m_name; - std::unordered_map m_level; - - lowlevel_notations m_notations; - - environment m_env; - - text_importer(environment const & env) : m_env(env) { - m_level[0] = {}; - m_name[0] = {}; - } - - levels read_levels(std::istream & in) { - unsigned idx; - buffer ls; - while (in >> idx) { - ls.push_back(m_level.at(idx)); - } - return levels(ls); - } - - level_param_names read_level_params(std::istream & in) { - unsigned idx; - buffer ls; - while (in >> idx) { - ls.push_back(m_name.at(idx)); - } - return names(ls); - } - - void handle_ind(std::istream & in) { - unsigned num_params, name_idx, type_idx, num_intros; - in >> num_params >> name_idx >> type_idx >> num_intros; - - buffer intros; - for (unsigned i = 0; i < num_intros; i++) { - unsigned name_idx, type_idx; in >> name_idx >> type_idx; - intros.push_back(inductive::mk_intro_rule(m_name.at(name_idx), m_expr.at(type_idx))); - } - - auto ls = read_level_params(in); - - inductive::inductive_decl decl(m_name.at(name_idx), ls, num_params, m_expr.at(type_idx), to_list(intros)); - m_env = inductive::add_inductive(m_env, decl, false).first; - } - - void handle_def(std::istream & in) { - unsigned name_idx, type_idx, val_idx; - in >> name_idx >> type_idx >> val_idx; - auto ls = read_level_params(in); - - auto decl = - old_type_checker(m_env).is_prop(m_expr.at(type_idx)) ? - mk_theorem(m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx)) : - mk_definition(m_env, m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx), true, false); - - m_env = m_env.add(check(m_env, decl)); - } - - void handle_ax(std::istream & in) { - unsigned name_idx, type_idx; - in >> name_idx >> type_idx; - auto ls = read_level_params(in); - m_env = m_env.add(check(m_env, mk_axiom(m_name.at(name_idx), ls, m_expr.at(type_idx)))); - } - - void handle_notation(std::istream & in, lowlevel_notation_kind kind) { - unsigned name_idx, prec; - in >> name_idx >> prec; - - std::string token; - std::getline(in, token); - if (!token.empty() && token.front()) - token.erase(token.begin()); - if (!token.empty() && token.back() == '\n') - token.erase(token.end() - 1); - - m_notations[m_name.at(name_idx)] = { kind, token, prec }; - } - - binder_info read_binder_info(std::string const & tok) { - if (tok == "#BI") { - return mk_implicit_binder_info(); - } else if (tok == "#BS") { - return mk_strict_implicit_binder_info(); - } else if (tok == "#BC") { - return mk_inst_implicit_binder_info(); - } else if (tok == "#BD") { - return {}; - } else { - throw exception(sstream() << "unknown binder info: " << tok); - } - } - - void handle_line(std::string const & line) { - std::istringstream in(line); - - unsigned idx; - std::string cmd; - in >> cmd; - if (cmd == "#IND") { - handle_ind(in); - } else if (cmd == "#DEF") { - handle_def(in); - } else if (cmd == "#AX") { - handle_ax(in); - } else if (cmd == "#QUOT") { - m_env = m_env.add_quot(); - } else if (cmd == "#PREFIX") { - handle_notation(in, lowlevel_notation_kind::Prefix); - } else if (cmd == "#POSTFIX") { - handle_notation(in, lowlevel_notation_kind::Postfix); - } else if (cmd == "#INFIX") { - handle_notation(in, lowlevel_notation_kind::Infix); - } else if (std::istringstream(cmd) >> idx) { - std::string kind; - in >> kind; - - if (kind == "#NS") { - unsigned p; std::string limb; in >> p >> std::skipws >> limb; - m_name[idx] = name(m_name.at(p), limb.c_str()); - } else if (kind == "#NI") { - unsigned p, limb; in >> p >> limb; - m_name[idx] = name(m_name.at(p), limb); - } else if (kind == "#US") { - unsigned l1; in >> l1; - m_level[idx] = mk_succ(m_level.at(l1)); - } else if (kind == "#UM") { - unsigned l1, l2; in >> l1 >> l2; - m_level[idx] = mk_max(m_level.at(l1), m_level.at(l2)); - } else if (kind == "#UIM") { - unsigned l1, l2; in >> l1 >> l2; - m_level[idx] = mk_imax(m_level.at(l1), m_level.at(l2)); - } else if (kind == "#UP") { - unsigned i1; in >> i1; - m_level[idx] = mk_param_univ(m_name.at(i1)); - } else if (kind == "#EV") { - unsigned v; in >> v; - m_expr[idx] = mk_var(v); - } else if (kind == "#ES") { - unsigned l; in >> l; - m_expr[idx] = mk_sort(m_level.at(l)); - } else if (kind == "#EC") { - unsigned n; in >> n; - auto ls = read_levels(in); - m_expr[idx] = mk_constant(m_name.at(n), ls); - } else if (kind == "#EA") { - unsigned e1, e2; in >> e1 >> e2; - m_expr[idx] = mk_app(m_expr.at(e1), m_expr.at(e2)); - } else if (kind == "#EZ") { - unsigned n, t, v, b; in >> n >> t >> v >> b; - m_expr[idx] = mk_let(m_name.at(n), m_expr.at(t), m_expr.at(v), m_expr.at(b)); - } else if (kind == "#EL") { - unsigned n, t, e; std::string b; in >> b >> n >> t >> e; - m_expr[idx] = mk_lambda(m_name.at(n), m_expr.at(t), m_expr.at(e), read_binder_info(b)); - } else if (kind == "#EP") { - unsigned n, t, e; std::string b; in >> b >> n >> t >> e; - m_expr[idx] = mk_pi(m_name.at(n), m_expr.at(t), m_expr.at(e), read_binder_info(b)); - } else { - throw exception(sstream() << "unknown term definition kind: " << kind); - } - } else { - throw exception(sstream() << "unknown command: " << cmd); - } - } -}; - -void import_from_text(std::istream & in, environment & env, lowlevel_notations & notations) { - text_importer importer(env); - - std::string line; - unsigned line_num = 0; - while (std::getline(in, line)) { - line_num++; - try { - importer.handle_line(line); - } catch (throwable & t) { - throw exception(sstream() << "line " << line_num << ": " << t.what()); - } catch (std::exception & e) { - throw exception(sstream() << "line " << line_num << ": " << e.what()); - } - } - - env = importer.m_env; - notations = std::move(importer.m_notations); -} - -} diff --git a/src/checker/text_import.h b/src/checker/text_import.h deleted file mode 100644 index 40e7e02cb9..0000000000 --- a/src/checker/text_import.h +++ /dev/null @@ -1,28 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Gabriel Ebner -*/ -#pragma once -#include -#include -#include -#include "kernel/environment.h" - -namespace lean { - -enum class lowlevel_notation_kind { - Prefix, Postfix, Infix, -}; -struct lowlevel_notation_info { - lowlevel_notation_kind m_kind; - std::string m_token; - unsigned m_prec; -}; - -using lowlevel_notations = std::unordered_map; - -void import_from_text(std::istream & in, environment & env, lowlevel_notations & notations); - -} diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c9bbe35de5..252816767d 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -61,12 +61,6 @@ else() endif() endif() -add_test(NAME leanchecker - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" - COMMAND bash "${LEAN_SOURCE_DIR}/cmake/run_checker.sh" "${CMAKE_CROSSCOMPILING_EMULATOR}" - "$" "$" "${CMAKE_CURRENT_BINARY_DIR}/library_export.out" - "${LEAN_SOURCE_DIR}/../library") - # add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") # add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean") add_test(lean_help1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)