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

feat(frontends/lean): enable hash_consing during tactic execution

Browse source 
This commit is trying to address a memory consumption problem in
@dselsam project.
This commit is contained in:
Leonardo de Moura 2017-06-22 17:24:27 -07:00
parent 9cb94847cb
commit e63c79c81e
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/definition_cmds.cpp
View file

@ -677,7 +677,6 @@ static expr elaborate_proof(
bool is_rfl_lemma, expr const & final_type,
metavar_context const & mctx, local_context const & lctx,
parser_pos_provider pos_provider, bool use_info_manager, std::string const & file_name) {
scoped_expr_caching disable(false); // FIXME: otherwise sigma.eq fails to elaborate
auto tc = std::make_shared<type_context>(decl_env, opts, mctx, lctx);
scope_trace_env scope2(decl_env, opts, *tc);
scope_traces_as_messages scope2a(file_name, header_pos);
@ -722,7 +721,6 @@ static void check_example(environment const & decl_env, options const & opts,
expr const & fn, expr const & val0,
metavar_context const & mctx, local_context const & lctx,
parser_pos_provider pos_provider, bool use_info_manager, std::string const & file_name) {
scoped_expr_caching disable(false); // FIXME: otherwise sigma.eq fails to elaborate
auto tc = std::make_shared<type_context>(decl_env, opts, mctx, lctx);
scope_trace_env scope2(decl_env, opts, *tc);
scope_pos_info_provider scope3(pos_provider);

4
src/frontends/lean/elaborator.cpp
View file

@ -3341,6 +3341,7 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
tactic_state s = mk_tactic_state_for(mvar);
try {
scoped_expr_caching scope(true);
vm_obj r = tactic_evaluator(m_ctx, m_opts, ref)(tactic, s);
if (auto new_s = tactic::is_success(r)) {
metavar_context mctx = new_s->mctx();
@ -3642,6 +3643,7 @@ static expr replace_with_simple_metavars(metavar_context mctx, name_map<expr> &
expr elaborator::elaborate(expr const & e) {
scoped_info_manager scope_infom(&m_info);
scoped_expr_caching scope_no_caching(false);
expr r = visit(e, none_expr());
trace_elab_detail(tout() << "result before final checkpoint\n" << r << "\n";);
synthesize();
@ -3683,6 +3685,8 @@ expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) {
void elaborator::finalize_core(sanitize_param_names_fn & S, buffer<expr> & es,
bool check_unassigned, bool to_simple_metavar, bool collect_local_ctx) {
scoped_expr_caching scope(true);
flush_expr_cache();
name_map<expr> to_simple_mvar_cache;
for (expr & e : es) {
e = instantiate_mvars(e);