feat(frontends/lean/parser): disable verbose messages when importing files

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

src/frontends/lean/parser.cpp

@@ -2373,23 +2373,26 @@ class parser::imp {
             regular(m_io_state) << "  Set: " << id << endl;
     }
 
-    void import_lean_file(std::string const & fname) {
+    bool import_lean_file(std::string const & fname) {
         std::ifstream in(fname);
         if (!in.is_open())
             throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos);
         if (!m_env->mark_imported(fname.c_str())) {
             // module already imported
-            return;
+            return false;
         }
         try {
             script_state state; // Empty state object for the imported module
-            parser import_parser(m_env, m_io_state, in, &state, true /* use exceptions */, false /* not interactive */);
+            io_state ios = m_io_state;
+            ios.set_option(g_parser_verbose, false);
+            parser import_parser(m_env, ios, in, &state, true /* use exceptions */, false /* not interactive */);
             import_parser();
         } catch (interrupted &) {
             throw;
         } catch (exception &) {
             throw parser_error(sstream() << "failed to import file '" << fname << "'", m_last_cmd_pos);
         }
+        return true;
     }
 
     void parse_import() {
@@ -2401,16 +2404,23 @@ class parser::imp {
         } else {
             fname  = check_string_next("invalid import command, string (i.e., file name) or identifier expected");
         }
-        fname = find_file(fname);
-        if (is_lean_file(fname)) {
-            import_lean_file(fname);
-        } else if (is_lua_file(fname)) {
+        std::string ffname = find_file(fname);
+        bool r = false;
+        if (is_lean_file(ffname)) {
+            r = import_lean_file(ffname);
+        } else if (is_lua_file(ffname)) {
             if (!m_script_state)
                 throw parser_error(sstream() << "failed to import Lua file '" << fname << "', parser does not have an intepreter", m_last_cmd_pos);
-            m_script_state->import_explicit(fname.c_str());
+            r = m_script_state->import_explicit(ffname.c_str());
         } else {
             // assume is a Lean file
-            import_lean_file(fname);
+            r = import_lean_file(ffname);
+        }
+        if (m_verbose) {
+            if (r)
+                regular(m_io_state) << "  Imported '" << fname << "'" << endl;
+            else
+                regular(m_io_state) << "  Skipped '" << fname << "'" << endl;
         }
     }
 

src/util/script_state.cpp

@@ -119,18 +119,21 @@ struct script_state::imp {
         ::lean::dostring(m_state, str);
     }
 
-    void import_explicit(std::string const & fname) {
+    bool import_explicit(std::string const & fname) {
         if (m_imported_modules.find(fname) == m_imported_modules.end()) {
             dofile(fname.c_str());
             m_imported_modules.insert(fname);
+            return true;
+        } else {
+            return false;
         }
     }
 
-    void import_explicit(char const * fname) {
-        import_explicit(std::string(fname));
+    bool import_explicit(char const * fname) {
+        return import_explicit(std::string(fname));
     }
 
-    void import(char const * fname) {
+    bool import(char const * fname) {
         return import_explicit(find_file(fname));
     }
 };
@@ -161,12 +164,12 @@ void script_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
 
-void script_state::import(char const * str) {
-    m_ptr->import(str);
+bool script_state::import(char const * str) {
+    return m_ptr->import(str);
 }
 
-void script_state::import_explicit(char const * str) {
-    m_ptr->import_explicit(str);
+bool script_state::import_explicit(char const * str) {
+    return m_ptr->import_explicit(str);
 }
 
 mutex & script_state::get_mutex() {

src/util/script_state.h

@@ -46,14 +46,14 @@ public:
     void dostring(char const * str);
     /**
        \brief Import file \c fname from the LEAN_PATH.
-       If the file was already included, then nothing happens.
+       If the file was already included, then nothing happens, and method returns false.
     */
-    void import(char const * fname);
+    bool import(char const * fname);
     /**
        \brief Import file \c fname. \c fname is the explicit path to the file.
-       If the file was already included, then nothing happens.
+       If the file was already included, then nothing happens, and method returns false.
     */
-    void import_explicit(char const * fname);
+    bool import_explicit(char const * fname);
 
     /**
        \brief Execute \c f in the using the internal Lua State.

tests/lean/cast1.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Assumed: vector
   Assumed: N0
   Proved: V0

tests/lean/cast2.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Assumed: A
   Assumed: B
   Assumed: A'

tests/lean/cast3.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Assumed: A
   Assumed: A'
   Assumed: B

tests/lean/cast4.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU

tests/lean/discharge.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
 @Discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
   Proved: T

tests/lean/disj1.lean.expected.out

@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
   Proved: T1
   Proved: T2
 Theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a :=

tests/lean/mod1.lean.expected.out

@@ -1,9 +1,9 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: x
-  Assumed: y
-  Assumed: x
-  Assumed: y
+  Imported 'simple'
+  Skipped 'simple'
+  Imported 'simple.lean'
+  Skipped 'simple.lean'
 x + y : ℤ
   Assumed: z
 z : ℤ

tests/lean/norm_bug1.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU

tests/lean/norm_tac.lean.expected.out

@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
   Set: lean::pp::implicit
   Set: lean::pp::coercion
   Set: lean::pp::notation

tests/lean/type_inf_bug1.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU