feat(frontends/lean): process "show goal" command line option

src/emacs/lean-mode.el

@@ -153,7 +153,10 @@ will be flushed everytime it's executed."
   (local-set-key "\C-c\C-f"  'lean-fill-placeholder)
   (local-set-key "\C-c\C-r"  'lean-server-restart-process)
   (local-set-key "\M-."      'lean-find-tag)
-  (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete))
+  (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)
+  (lean-define-key-binding "\C-c\C-g"
+                           '(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))
+  )
 
 (defun lean-define-key-binding (key cmd)
   (local-set-key key `(lambda () (interactive) ,cmd)))

src/frontends/lean/CMakeLists.txt

@@ -10,6 +10,6 @@ init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
 parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
 type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp
 obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp
-parse_with_options_tactic.cpp parse_simp_tactic.cpp)
+parse_with_options_tactic.cpp parse_simp_tactic.cpp opt_cmd.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/elaborator.cpp

@@ -1808,11 +1808,36 @@ static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq)
     }
 }
 
+void elaborator::show_goal(proof_state const & ps, expr const & end, expr const & curr) {
+    unsigned line, col;
+    if (!m_ctx.has_show_goal_at(line, col))
+        return;
+    auto end_pos  = pip()->get_pos_info(end);
+    auto curr_pos = pip()->get_pos_info(curr);
+    if (!end_pos || !curr_pos)
+        return;
+    if (end_pos->first < line || (end_pos->first == line && end_pos->second < col))
+        return;
+    if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col))
+        return;
+    m_ctx.reset_show_goal_at();
+    goals const & gs = ps.get_goals();
+    auto out = regular(env(), ios());
+    out << "LEAN_GOAL_INFORMATION\n";
+    if (empty(gs)) {
+        out << "no goals\n";
+    } else {
+        out << head(gs) << "\n";
+    }
+    out << "END_LEAN_GOAL_INFORMATION\n";
+}
+
 bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
     lean_assert(is_begin_end_annotation(pre_tac));
     buffer<expr> pre_tac_seq;
     extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
     for (expr ptac : pre_tac_seq) {
+        show_goal(ps, pre_tac, ptac);
         if (is_begin_end_annotation(ptac)) {
             goals gs = ps.get_goals();
             if (!gs)
@@ -1865,6 +1890,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
             }
         }
     }
+    show_goal(ps, pre_tac, pre_tac);
 
     if (!empty(ps.get_goals())) {
         display_unsolved_subgoals(mvar, ps, pre_tac);

src/frontends/lean/elaborator.h

@@ -186,6 +186,8 @@ class elaborator : public coercion_info_manager {
     expr visit_obtain_expr(expr const & e, constraint_seq & cs);
 
     void check_used_local_tactic_hints();
+
+    void show_goal(proof_state const & ps, expr const & end, expr const & curr);
 public:
     elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names = false);
     std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type);

src/frontends/lean/elaborator_context.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/sexpr/option_declarations.h"
 #include "frontends/lean/elaborator_context.h"
+#include "frontends/lean/opt_cmd.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@@ -71,6 +72,30 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
     m_flycheck_goals      = get_elaborator_flycheck_goals(ios.get_options());
     m_fail_missing_field  = get_elaborator_fail_missing_field(ios.get_options());
     m_lift_coercions      = get_elaborator_lift_coercions(ios.get_options());
+    init_options(ios.get_options());
+}
+
+void elaborator_context::init_options(options const & opts) {
+    if (has_show_goal(opts, m_show_goal_line, m_show_goal_col)) {
+        m_show_goal_at = true;
+    } else {
+        m_show_goal_at = false;
+    }
+
+}
+
+bool elaborator_context::has_show_goal_at(unsigned & line, unsigned & col) const {
+    if (m_show_goal_at) {
+        line = m_show_goal_line;
+        col  = m_show_goal_col;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+void elaborator_context::reset_show_goal_at() {
+    m_show_goal_at = false;
 }
 
 void initialize_elaborator_context() {

src/frontends/lean/elaborator_context.h

@@ -27,6 +27,16 @@ class elaborator_context {
     bool                      m_fail_missing_field;
     bool                      m_lift_coercions;
     friend class elaborator;
+
+    bool     m_show_goal_at;
+    unsigned m_show_goal_line;
+    unsigned m_show_goal_col;
+
+    /** \brief Support for showing information using hot-keys */
+    void init_options(options const & opts);
+    bool has_show_goal_at(unsigned & line, unsigned & col) const;
+    void reset_show_goal_at();
+
 public:
     elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
                        pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true);

src/frontends/lean/opt_cmd.cpp

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "frontends/lean/opt_cmd.h"
+
+namespace lean {
+options set_show_goal(options const & _opts, unsigned line, unsigned col) {
+    options opts = _opts;
+    opts = opts.update(name("show_goal"), true);
+    opts = opts.update(name("line"), line);
+    opts = opts.update(name("column"), col);
+    return opts;
+}
+
+bool has_show_goal(options const & opts, unsigned & line, unsigned & col) {
+    if (opts.get_bool("show_goal")) {
+        line = opts.get_unsigned("line", 0);
+        col  = opts.get_unsigned("column", 0);
+        return true;
+    } else {
+        return false;
+    }
+}
+}

src/frontends/lean/opt_cmd.h

@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/sexpr/options.h"
+
+namespace lean {
+// We use options to communicate auxiliary commands set by the lean.exe frontend.
+
+options set_show_goal(options const & opts, unsigned line, unsigned col);
+bool has_show_goal(options const & opts, unsigned & line, unsigned & col);
+}

src/frontends/lean/parser.cpp

@@ -50,6 +50,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parse_rewrite_tactic.h"
 #include "frontends/lean/update_environment_exception.h"
 #include "frontends/lean/local_ref_info.h"
+#include "frontends/lean/opt_cmd.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -101,6 +102,15 @@ parser::undef_id_to_local_scope::undef_id_to_local_scope(parser & p):
 
 static name * g_tmp_prefix = nullptr;
 
+void parser::init_stop_at(options const & opts) {
+    unsigned col;
+    if (has_show_goal(opts, m_stop_at_line, col)) {
+        m_stop_at      = true;
+    } else {
+        m_stop_at      = false;
+    }
+}
+
 parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
                bool use_exceptions, unsigned num_threads,
@@ -114,6 +124,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_local_decls_size_at_beg_cmd = 0;
     m_in_backtick = false;
     m_profile     = ios.get_options().get_bool("profile", false);
+    init_stop_at(ios.get_options());
     if (num_threads > 1 && m_profile)
         throw exception("option --profile cannot be used when theorems are compiled in parallel");
     m_has_params = false;
@@ -1830,6 +1841,9 @@ bool parser::parse_commands() {
 #endif
         }
         while (!done) {
+            if (m_stop_at && pos().first > m_stop_at_line) {
+                throw interrupt_parser();
+            }
             protected_call([&]() {
                     check_interrupted();
                     switch (curr()) {

src/frontends/lean/parser.h

@@ -147,6 +147,10 @@ class parser {
     // auxiliary field used to record the size of m_local_decls before a command is executed.
     unsigned               m_local_decls_size_at_beg_cmd;
 
+    // stop at line/col
+    bool                   m_stop_at; // if true, then parser stops execution after the given line and column is reached
+    unsigned               m_stop_at_line;
+
     void display_warning_pos(unsigned line, unsigned pos);
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
@@ -248,6 +252,8 @@ class parser {
     expr parse_tactic_opt_id_list();
     expr parse_tactic_using_expr();
 
+    void init_stop_at(options const & opts);
+
 public:
     parser(environment const & env, io_state const & ios,
            std::istream & strm, char const * str_name,

src/shell/lean.cpp

@@ -38,6 +38,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 #include "frontends/lean/server.h"
 #include "frontends/lean/dependencies.h"
+#include "frontends/lean/opt_cmd.h"
 #include "init/init.h"
 #include "shell/emscripten.h"
 #include "shell/simple_pos_info_provider.h"
@@ -366,9 +367,8 @@ int main(int argc, char ** argv) {
         }
     }
 
-    if (show_goal) {
-        std::cout << "SHOW GOAL @ " << *line << " : " << *column << "\n";
-        exit(0);
+    if (show_goal && line && column) {
+        opts = set_show_goal(opts, *line, *column);
     }
 
     #if !defined(LEAN_MULTI_THREAD)