michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add option '-X': discard all proofs after theorems are checked

Browse source 
This option is useful for generating compact .olean files for web demos
This commit is contained in:
Leonardo de Moura 2014-10-13 10:05:38 -07:00
parent 698dc0472d
commit bc70e7244d
4 changed files with 52 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/frontends/lean/decl_cmds.cpp
View file

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

19
src/frontends/lean/parser.cpp
View file

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

13
src/frontends/lean/parser.h
View file

@ -78,6 +78,8 @@ struct snapshot {
typedef std::vector<snapshot> 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<typename T> 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();

31
src/shell/lean.cpp
View file

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