feat(frontends/lean): display warning message when importing file that uses 'sorry'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -113,7 +113,8 @@ expr parser::mk_sorry(pos_info const & p) {
     m_used_sorry = true;
     {
         flycheck_warning wrn(regular_stream());
-        regular_stream() << get_stream_name() << ":" << p.first << ":" << p.second << ": warning using 'sorry'" << endl;
+        display_warning_pos(p.first, p.second);
+        regular_stream() << " using 'sorry'" << endl;
     }
     return get_sorry_constant();
 }
@@ -140,11 +141,13 @@ void parser::updt_options() {
     m_show_errors = get_parser_show_errors(m_ios.get_options());
 }
 
+void parser::display_warning_pos(unsigned line, unsigned pos) {
+    ::lean::display_warning_pos(regular_stream(), get_stream_name().c_str(), line, pos);
+}
+void parser::display_warning_pos(pos_info p) { display_warning_pos(p.first, p.second); }
+
 void parser::display_error_pos(unsigned line, unsigned pos) {
-    regular_stream() << get_stream_name() << ":" << line << ":";
+    ::lean::display_error_pos(regular_stream(), get_stream_name().c_str(), line, pos);
-    if (pos != static_cast<unsigned>(-1))
-        regular_stream() << pos << ":";
-    regular_stream() << " error:";
 }
 void parser::display_error_pos(pos_info p) { display_error_pos(p.first, p.second); }
 
@@ -154,9 +157,7 @@ void parser::display_error(char const * msg, unsigned line, unsigned pos) {
     regular_stream() << " " << msg << endl;
 }
 
-void parser::display_error(char const * msg, pos_info p) {
+void parser::display_error(char const * msg, pos_info p) { display_error(msg, p.first, p.second); }
-    display_error(msg, p.first, p.second);
-}
 
 void parser::display_error(exception const & ex) {
     parser_pos_provider pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos);
@@ -1099,6 +1100,11 @@ bool parser::parse_commands() {
     try {
         bool done = false;
         parse_imports();
+        if (has_sorry(m_env)) {
+            flycheck_warning wrn(regular_stream());
+            display_warning_pos(pos());
+            regular_stream() << " imported file uses 'sorry'" << endl;
+        }
         while (!done) {
             protected_call([&]() {
                     check_interrupted();

src/frontends/lean/parser.h

@@ -69,6 +69,8 @@ class parser {
     // We process theorems in parallel
     theorem_queue           m_theorem_queue;
 
+    void display_warning_pos(unsigned line, unsigned pos);
+    void display_warning_pos(pos_info p);
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
     void display_error(char const * msg, unsigned line, unsigned pos);

src/frontends/lean/sorry.cpp

@@ -16,7 +16,7 @@ static expr  g_sorry_type(mk_pi("A", mk_sort(mk_param_univ(g_l)), mk_var(0), bin
 
 bool has_sorry(environment const & env) {
     auto decl = env.find(g_sorry_name);
-    return decl && decl->get_type() != g_sorry_type;
+    return decl && decl->get_type() == g_sorry_type;
 }
 
 environment declare_sorry(environment const & env) {

src/library/error_handling/error_handling.cpp

@@ -34,13 +34,22 @@ flyinfo_scope::~flyinfo_scope() {
     if (m_flyinfo) m_ios << "FLYCHECK_END" << endl;
 }
 
-void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
+void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
     ios << strm_name << ":" << line << ":";
     if (pos != static_cast<unsigned>(-1))
         ios << pos << ":";
+}
+
+void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
+    display_pos(ios, strm_name, line, pos);
     ios << " error:";
 }
 
+void display_warning_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
+    display_pos(ios, strm_name, line, pos);
+    ios << " warning:";
+}
+
 void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e) {
     if (p) {
         auto pos = p->get_pos_info_or_some(e);

src/library/error_handling/error_handling.h

@@ -40,6 +40,10 @@ public:
    If it is not available, it just displays "error:"
 */
 void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e);
+/** \brief Display position information + "error:" */
+void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos);
+/** \brief Similar to #display_error_pos, but displays a "warning:" */
+void display_warning_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos);
 /**
    \brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios.
    Exceptions that contain expressions use the given \c pos_info_provider (if available) to retrieve line number information.