diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 3e1129942..58b4a7bed 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -424,10 +424,15 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo try { level_param_names c_ls; expr c_type, c_value; std::tie(c_ls, c_type, c_value) = *it; - if (is_theorem) + if (is_theorem) { cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value)); - else + if (!p.keep_new_thms()) { + // discard theorem + cd = check(env, mk_axiom(real_n, c_ls, c_type)); + } + } else { cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, is_opaque)); + } if (!is_private) p.add_decl_index(real_n, n_pos, p.get_cmd_token(), c_type); env = module::add(env, *cd); @@ -451,7 +456,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo } else { std::tie(type, value, new_ls) = p.elaborate_definition(n, type_as_is, value, is_opaque); new_ls = append(ls, new_ls); - env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value))); + auto cd = check(env, mk_theorem(real_n, new_ls, type, value)); + if (!p.keep_new_thms()) { + // discard theorem + cd = check(env, mk_axiom(real_n, new_ls, type)); + } + env = module::add(env, cd); p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value); } } else { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7684925f8..eb90b9a77 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -87,13 +87,13 @@ parser::parser(environment const & env, io_state const & ios, std::istream & strm, char const * strm_name, bool use_exceptions, unsigned num_threads, snapshot const * s, snapshot_vector * sv, info_manager * im, - bool keep_imported_proofs): + keep_theorem_mode tmode): m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix), m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name, s ? s->m_line : 1), m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) { - m_keep_imported_thms = keep_imported_proofs; + m_keep_theorem_mode = tmode; if (s) { m_local_level_decls = s->m_lds; m_local_decls = s->m_eds; @@ -1287,8 +1287,9 @@ void parser::parse_imports() { unsigned num_threads = 0; if (get_parser_parallel_import(m_ios.get_options())) num_threads = m_num_threads; + bool keep_imported_thms = (m_keep_theorem_mode == keep_theorem_mode::All); m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads, - m_keep_imported_thms, m_ios); + keep_imported_thms, m_ios); for (auto const & f : lua_files) { std::string rname = find_file(f, {".lua"}); system_import(rname.c_str()); @@ -1364,7 +1365,8 @@ bool parser::parse_commands() { } catch (interrupt_parser) {} commit_info(m_scanner.get_line()+1); for (certified_declaration const & thm : m_theorem_queue.join()) { - m_env.replace(thm); + if (keep_new_thms()) + m_env.replace(thm); } return !m_found_errors; } @@ -1455,8 +1457,9 @@ void parser::save_type_info(expr const & e) { } bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, - unsigned num_threads, definition_cache * cache, declaration_index * index, bool keep_thms) { - parser p(env, ios, in, strm_name, use_exceptions, num_threads, nullptr, nullptr, nullptr, keep_thms); + unsigned num_threads, definition_cache * cache, declaration_index * index, + keep_theorem_mode tmode) { + parser p(env, ios, in, strm_name, use_exceptions, num_threads, nullptr, nullptr, nullptr, tmode); p.set_cache(cache); p.set_index(index); bool r = p(); @@ -1466,11 +1469,11 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c } bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, - definition_cache * cache, declaration_index * index, bool keep_thms) { + definition_cache * cache, declaration_index * index, keep_theorem_mode tmode) { std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); - return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index, keep_thms); + return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index, tmode); } void initialize_parser() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index e960e8d83..4324b188c 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -78,6 +78,8 @@ struct snapshot { typedef std::vector snapshot_vector; +enum class keep_theorem_mode { All, DiscardImported, DiscardAll }; + class parser { environment m_env; io_state m_ios; @@ -120,7 +122,7 @@ class parser { // index support declaration_index * m_index; - bool m_keep_imported_thms; + keep_theorem_mode m_keep_theorem_mode; // curr command token name m_cmd_token; @@ -208,7 +210,7 @@ public: std::istream & strm, char const * str_name, bool use_exceptions = false, unsigned num_threads = 1, snapshot const * s = nullptr, snapshot_vector * sv = nullptr, - info_manager * im = nullptr, bool keep_imported_proofs = true); + info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); ~parser(); void set_cache(definition_cache * c) { m_cache = c; } @@ -235,6 +237,8 @@ public: bool has_tactic_decls(); expr mk_by(expr const & t, pos_info const & pos); + bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; } + void updt_options(); template void set_option(name const & n, T const & v) { m_ios.set_option(n, v); } @@ -397,9 +401,10 @@ public: bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, - declaration_index * index = nullptr, bool keep_imported_proofs = true); + declaration_index * index = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, - definition_cache * cache = nullptr, declaration_index * index = nullptr, bool keep_imported_proofs = true); + definition_cache * cache = nullptr, declaration_index * index = nullptr, + keep_theorem_mode tmode = keep_theorem_mode::All); void initialize_parser(); void finalize_parser(); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 991dac827..cbdbe2d9e 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -54,6 +54,7 @@ using lean::optional; using lean::expr; using lean::options; using lean::declaration_index; +using lean::keep_theorem_mode; enum class input_kind { Unspecified, Lean, Lua }; @@ -92,6 +93,8 @@ static void display_help(std::ostream & out) { std::cout << " 0 means 'do not check'.\n"; std::cout << " --trust=num -t trust level (default: 0) \n"; std::cout << " --discard -T discard the proof of imported theorems after checking\n"; + std::cout << " --to_axiom -X discard proofs of all theorems after checking them, i.e.,\n"; + std::cout << " theorems become axioms after checking\n"; std::cout << " --quiet -q do not print verbose messages\n"; #if defined(LEAN_MULTI_THREAD) std::cout << " --server start Lean in 'server' mode\n"; @@ -133,6 +136,7 @@ static struct option g_long_options[] = { {"cpp", required_argument, 0, 'C'}, {"trust", required_argument, 0, 't'}, {"discard", no_argument, 0, 'T'}, + {"to_axiom", no_argument, 0, 'X'}, #if defined(LEAN_MULTI_THREAD) {"server", no_argument, 0, 'S'}, {"threads", required_argument, 0, 'j'}, @@ -148,7 +152,7 @@ static struct option g_long_options[] = { {0, 0, 0, 0} }; -#define BASIC_OPT_STR "TFC:dD:qlupgvhk:012t:012o:c:i:" +#define BASIC_OPT_STR "XTFC:dD:qlupgvhk:012t:012o:c:i:" #if defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD) static char const * g_opt_str = BASIC_OPT_STR "Sj:012s:012"; @@ -220,15 +224,15 @@ static void export_as_cpp_file(std::string const & fname, char const * varname, int main(int argc, char ** argv) { lean::initializer init; - bool export_objects = false; - unsigned trust_lvl = 0; - bool server = false; - bool only_deps = false; - unsigned num_threads = 1; - bool use_cache = false; - bool gen_index = false; - bool export_cpp = false; - bool keep_thms = true; + bool export_objects = false; + unsigned trust_lvl = 0; + bool server = false; + bool only_deps = false; + unsigned num_threads = 1; + bool use_cache = false; + bool gen_index = false; + bool export_cpp = false; + keep_theorem_mode tmode = keep_theorem_mode::All; options opts; std::string output; std::string cpp_output; @@ -289,7 +293,10 @@ int main(int argc, char ** argv) { trust_lvl = atoi(optarg); break; case 'T': - keep_thms = false; + tmode = keep_theorem_mode::DiscardImported; + break; + case 'X': + tmode = keep_theorem_mode::DiscardAll; break; case 'q': opts = opts.update("verbose", false); @@ -356,7 +363,7 @@ int main(int argc, char ** argv) { if (!display_deps(env, std::cout, std::cerr, argv[i])) ok = false; } else if (!parse_commands(env, ios, argv[i], false, num_threads, - cache_ptr, index_ptr, keep_thms)) { + cache_ptr, index_ptr, tmode)) { ok = false; } } else if (k == input_kind::Lua) {