feat(frontends/lean/parser): keep list of tasks that have to succeed

src/frontends/lean/definition_cmds.cpp

@@ -363,6 +363,8 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
         mk_theorem(c_real_name, to_list(lp_names), type, *val) :
         mk_definition(new_env, c_real_name, to_list(lp_names), type, *val, use_conv_opt, is_trusted));
     auto cdef         = check(p, new_env, c_name, def, pos);
+    if (cdef.get_declaration().is_theorem())
+        p.require_success(cdef.get_declaration().get_value_task());
     new_env           = module::add(new_env, cdef);
 
     check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, modifiers.m_is_noncomputable);
@@ -733,6 +735,7 @@ public:
                                       ERROR);
             error_msg.set_exception(ex);
             error_msg.report();
+            throw std::exception(); // this bypasses the default exception reporting
         }
         return {};
     }
@@ -787,15 +790,16 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
             auto elab_task = get_global_task_queue()->submit<proof_elaboration_task>(
                 decl_env, p.get_options(), header_pos, new_params, new_fn, val, thm_finfo, is_rfl, type,
                 elab.mctx(), elab.lctx(), p.get_parser_pos_provider(header_pos));
+            p.require_success(elab_task);
             env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, elab_task, modifiers, attrs,
                                        doc_string, header_pos);
         } else if (kind == Example) {
-            get_global_task_queue()->submit<example_checking_task>(
+            p.require_success(get_global_task_queue()->submit<example_checking_task>(
                     p.env(), p.get_options(),
                     modifiers, to_list(lp_names),
                     new_params, fn, val,
                     elab.mctx(), elab.lctx(),
-                    p.get_parser_pos_provider(header_pos));
+                    p.get_parser_pos_provider(header_pos)));
             return p.env();
         } else {
             std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);

src/frontends/lean/parser.cpp

@@ -2224,7 +2224,34 @@ void parser::get_imports(std::vector<module_name> & imports) {
     parse_imports(fingerprint, imports);
 }
 
-bool parser::parse_commands() {
+struct combine_parse_success_task : public task<bool> {
+    list<generic_task_result> m_required_successes;
+
+    combine_parse_success_task(list<generic_task_result> const & required_successes) :
+            task(), m_required_successes(required_successes) {}
+
+    void description(std::ostream & out) const override {
+        out << "Checking parse success (" << get_module_id() << ")";
+    }
+
+    std::vector<generic_task_result> get_dependencies() override {
+        std::vector<generic_task_result> deps;
+        for (auto & d : m_required_successes)
+            deps.push_back(d);
+        return deps;
+    }
+
+    bool is_tiny() const override { return true; }
+
+    bool do_priority_inversion() const override { return false; }
+
+    bool execute() override {
+        for (auto & d : m_required_successes) get_global_task_queue()->wait(d);
+        return true;
+    }
+};
+
+task_result<bool> parser::parse_commands() {
     protected_call([&]() {
         // We disable hash-consing while parsing to make sure the pos-info are correct.
         scoped_expr_caching disable(false);
@@ -2295,7 +2322,12 @@ bool parser::parse_commands() {
                 m_env = pop_scope_core(m_env, m_ios);
         }
     }, [](){});
-    return !m_found_errors;
+
+    if (m_found_errors) {
+        return mk_pure_task_result(false, "parse success");
+    } else {
+        return get_global_task_queue()->submit<combine_parse_success_task>(m_required_successes);
+    }
 }
 
 bool parser::curr_is_command_like() const {
@@ -2318,7 +2350,8 @@ void parser::save_snapshot(scope_message_context & smc, pos_info p) {
         m_snapshot_vector->push_back(std::make_shared<snapshot>(
                 m_env, smc.get_sub_buckets(), m_local_level_decls, m_local_decls,
                 m_level_variables, m_variables, m_include_vars,
-                m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_next_inst_idx, p));
+                m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_next_inst_idx, p,
+                m_required_successes));
     }
 }
 

src/frontends/lean/parser.h

@@ -67,12 +67,14 @@ struct snapshot {
     parser_scope_stack m_parser_scope_stack;
     unsigned           m_next_inst_idx;
     pos_info           m_pos;
+    list<generic_task_result> m_required_successes;
     snapshot(environment const & env, name_set const & sub_buckets, local_level_decls const & lds,
              local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
              name_set const & includes, options const & opts, bool imports_parsed, parser_scope_stack const & pss,
-             unsigned next_inst_idx, pos_info const & pos):
+             unsigned next_inst_idx, pos_info const & pos, list<generic_task_result> const & required_successes):
         m_env(env), m_sub_buckets(sub_buckets), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
-        m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos) {}
+        m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos),
+        m_required_successes(required_successes) {}
 };
 
 typedef std::vector<std::shared_ptr<snapshot const>> snapshot_vector;
@@ -171,6 +173,9 @@ class parser : public abstract_parser {
     // Docgen
     optional<std::string>  m_doc_string;
 
+    // Tasks that need to be successful (no exception) for parsing to succeed
+    list<generic_task_result> m_required_successes;
+
     void throw_parser_exception(char const * msg, pos_info p);
     void throw_nested_exception(throwable const & ex, pos_info p);
 
@@ -196,7 +201,7 @@ class parser : public abstract_parser {
 
     void process_imports();
     void parse_command();
-    bool parse_commands();
+    task_result<bool> parse_commands();
     void process_postponed(buffer<expr> const & args, bool is_left, buffer<notation::action_kind> const & kinds,
                            buffer<list<expr>> const & nargs, buffer<expr> const & ps, buffer<pair<unsigned, pos_info>> const & scoped_info,
                            list<notation::action> const & postponed, pos_info const & p, buffer<expr> & new_args);
@@ -516,11 +521,15 @@ public:
     bool used_sorry() const { return m_used_sorry; }
     void declare_sorry_if_used();
 
+    void require_success(generic_task_result const & t) {
+        m_required_successes = cons(t, m_required_successes);
+    }
+
     /** return true iff profiling is enabled */
     bool profiling() const { return m_profile; }
 
     /** parse all commands in the input stream */
-    bool operator()() { return parse_commands(); }
+    task_result<bool> operator()() { return parse_commands(); }
 
     void get_imports(std::vector<module_name> &);
 

src/kernel/declaration.cpp

@@ -60,7 +60,7 @@ unsigned declaration::get_num_univ_params() const { return length(get_univ_param
 expr const & declaration::get_type() const { return m_ptr->m_type; }
 
 task_result<expr> const & declaration::get_value_task() const {
-    lean_assert(is_definition());
+    lean_assert(is_theorem());
     return m_ptr->m_proof;
 }
 expr const & declaration::get_value() const {

src/library/module_mgr.cpp

@@ -18,6 +18,14 @@ Author: Gabriel Ebner
 
 namespace lean {
 
+bool module_info::parse_result::is_ok() const {
+    try {
+        return m_parsed_ok.get() && m_proofs_are_correct.get();
+    } catch (...) {
+        return false;
+    }
+}
+
 void module_mgr::mark_out_of_date(module_id const & id, buffer<module_id> & to_rebuild) {
     for (auto & mod : m_modules) {
         if (!mod.second || mod.second->m_out_of_date) continue;
@@ -123,7 +131,7 @@ public:
                  use_exceptions,
                  (m_snapshots.empty() || !m_use_snapshots) ? std::shared_ptr<snapshot>() : m_snapshots.back(),
                  m_use_snapshots ? &m_snapshots : nullptr);
-        bool parsed_ok = p();
+        auto parsed_ok = p();
 
         module_info::parse_result mod;
 
@@ -161,6 +169,7 @@ public:
         if (auto res = m_mod->m_result.peek()) {
             for (auto & mdf : res->m_loaded_module->m_modifications)
                 mdf->get_task_dependencies(deps);
+            deps.push_back(res->m_parsed_ok);
             deps.push_back(res->m_proofs_are_correct);
         }
 
@@ -257,7 +266,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set
                       parse_olean_modifications(parsed_olean.second, id), {} },
                     m_initial_env, [=] { return mk_loader(id, deps); });
 
-            res.m_parsed_ok = true;
+            res.m_parsed_ok = mk_pure_task_result(true, "olean parse success");
             res.m_proofs_are_correct = mk_pure_task_result(true, "");
             mod->m_result = mk_pure_task_result(res, "Loading " + olean_fn);
 

src/library/module_mgr.h

@@ -47,9 +47,9 @@ struct module_info {
     struct parse_result {
         options               m_opts;
 
-        bool m_parsed_ok = false;
+        task_result<bool> m_parsed_ok;
         task_result<bool> m_proofs_are_correct;
-        bool is_ok() const { return m_parsed_ok && m_proofs_are_correct.get(); }
+        bool is_ok() const;
 
         std::shared_ptr<loaded_module const> m_loaded_module;
 

tests/lean/fail/example.lean

@@ -0,0 +1,2 @@
+open tactic expr
+example : false := by do exact $ const `does_not_exist []

tests/lean/run/apply4.lean

@@ -20,7 +20,7 @@ set_option pp.all false
 example (a b : nat) : a = 0 → a = b :=
 by do
   intro `H,
-  apply_core semireducible tt ff (expr.const `foo [level.of_nat 1]),
+  apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]),
   trace_state,
   a ← get_local `a,
   trace_state,
@@ -45,6 +45,6 @@ by do
 example (a b : nat) : a = 0 → a = b :=
 by do
   `[intro],
-  apply_core semireducible tt ff (expr.const `foo [level.of_nat 1]),
+  apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]),
   `[exact inhabited.mk a],
   reflexivity

tests/lean/run/auto_quote1.lean

@@ -56,7 +56,7 @@ begin
   induction m with m' ih,
   { -- Remark: Used change here to make sure nat.zero is replaced with polymorphic zero.
     -- dsimp tactic should fix that in the future.
-    change n + 0 = 0 + n, rw zadd n },
+    change n + 0 = 0 + n, simp [zadd] },
   { change succ (n + m') = succ m' + n,
     rw [succ_add, ih] }
 end
@@ -72,7 +72,7 @@ begin
   induction m with m' ih,
   show n + 0 = 0 + n,
   begin
-    change n + 0 = 0 + n, rw zadd n
+    change n + 0 = 0 + n, simp [zadd]
   end,
   show n + succ m' = succ m' + n, {
     change succ (n + m') = succ m' + n,

tests/lean/run/elab_crash1.lean

@@ -4,10 +4,10 @@ meta definition to_expr_target (a : pexpr) : tactic expr :=
 do tgt ← target,
    to_expr `((%%a : %%tgt))
 
-example (A : Type) (a : A) : A :=
+noncomputable example (A : Type) (a : A) : A :=
 by do to_expr_target `(sorry) >>= exact
 
-example (A : Type) (a : A) : A :=
+noncomputable example (A : Type) (a : A) : A :=
 by do refine `(sorry)
 
 example (a : nat) : nat :=

tests/lean/run/simplify_with_hypotheses.lean

@@ -1,9 +1,9 @@
 open tactic
 
-example (A : Type) (a₁ a₂ : A) (f : A → A) (H₀ : a₁ = a₂) : f a₁ = f a₂ := by simp_using_hs >> try reflexivity
+example (A : Type) (a₁ a₂ : A) (f : A → A) (H₀ : a₁ = a₂) : f a₁ = f a₂ := by do simp_using_hs >> try reflexivity
 
 example (A : Type) (a₁ a₁' a₂ a₂' : A) (f : A → A) (H₀ : a₁' = a₂') (H₁ : f a₁ = a₁') (H₂ : f a₂ = a₂')
-: f a₁ = f a₂ := by simp_using_hs >> try reflexivity
+: f a₁ = f a₂ := by do simp_using_hs >> try reflexivity
 
 constants (A : Type.{1}) (x y z w : A) (f : A → A) (H₁ : f (f x) = f y) (H₂ : f (f y) = f z) (H₃ : f (f z) = w)