feat(frontends/lean): add option 'elaborator.flycheck_goals'

src/frontends/lean/elaborator.cpp

@@ -1049,6 +1049,14 @@ void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
                     display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
                     return;
                 }
+                if (m_ctx.m_flycheck_goals) {
+                    if (auto p = pip()->get_pos_info(ptac)) {
+                        auto out = regular(env(), ios());
+                        flycheck_information info(out);
+                        display_information_pos(out, pip()->get_file_name(), p->first, p->second);
+                        out << " proof state:\n" << ps.pp(env(), ios()) << "\n";
+                    }
+                }
                 ps = r->first;
             } catch (tactic_exception & ex) {
                 auto out = regular(env(), ios());

src/frontends/lean/elaborator_context.cpp

@@ -15,11 +15,16 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES false
 #endif
 
+#ifndef LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS
+#define LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS false
+#endif
+
 namespace lean {
 // ==========================================
 // elaborator configuration options
 static name * g_elaborator_local_instances  = nullptr;
 static name * g_elaborator_ignore_instances = nullptr;
+static name * g_elaborator_flycheck_goals   = nullptr;
 
 name const & get_elaborator_ignore_instances_name() {
     return *g_elaborator_ignore_instances;
@@ -32,6 +37,10 @@ bool get_elaborator_local_instances(options const & opts) {
 bool get_elaborator_ignore_instances(options const & opts) {
     return opts.get_bool(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES);
 }
+
+bool get_elaborator_flycheck_goals(options const & opts) {
+    return opts.get_bool(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS);
+}
 // ==========================================
 
 elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
@@ -39,18 +48,24 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
     m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) {
     m_use_local_instances = get_elaborator_local_instances(ios.get_options());
     m_ignore_instances    = get_elaborator_ignore_instances(ios.get_options());
+    m_flycheck_goals      = get_elaborator_flycheck_goals(ios.get_options());
 }
 
 void initialize_elaborator_context() {
-    g_elaborator_local_instances = new name{"elaborator", "local_instances"};
+    g_elaborator_local_instances  = new name{"elaborator", "local_instances"};
     g_elaborator_ignore_instances = new name{"elaborator", "ignore_instances"};
+    g_elaborator_flycheck_goals   = new name{"elaborator", "flycheck_goals"};
     register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES,
                          "(lean elaborator) use local declarates as class instances");
     register_bool_option(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES,
                          "(lean elaborator) if true, then elaborator does not perform class-instance resolution");
+    register_bool_option(*g_elaborator_flycheck_goals, LEAN_DEFAULT_ELABORATOR_FLYCHECK_GOALS,
+                         "(lean elaborator) if true, then elaborator display current goals for flycheck before each "
+                         "tactic is executed in a `begin ... end` block");
 }
 void finalize_elaborator_context() {
     delete g_elaborator_local_instances;
     delete g_elaborator_ignore_instances;
+    delete g_elaborator_flycheck_goals;
 }
 }

src/frontends/lean/elaborator_context.h

@@ -23,6 +23,7 @@ class elaborator_context {
     bool                      m_check_unassigned;
     bool                      m_use_local_instances;
     bool                      m_ignore_instances;
+    bool                      m_flycheck_goals;
     friend class elaborator;
 public:
     elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,