feat(frontends/lean): make sure all scopes are closed in the end of the module

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

src/frontends/lean/parser.cpp

@@ -1183,6 +1183,13 @@ bool parser::parse_commands() {
                 },
                 [&]() { sync_command(); });
         }
+        if (has_open_scopes(m_env)) {
+            m_found_errors = true;
+            if (!m_use_exceptions && m_show_errors)
+                display_error("invalid end of module, expecting 'end'", pos());
+            else if (m_use_exceptions)
+                throw_parser_exception("invalid end of module, expecting 'end'", pos());
+        }
     } catch (interrupt_parser) {}
     for (certified_declaration const & thm : m_theorem_queue.join()) {
         m_env.replace(thm);

src/library/scoped_ext.cpp

@@ -136,6 +136,11 @@ environment pop_scope(environment const & env, name const & n) {
     return r;
 }
 
+bool has_open_scopes(environment const & env) {
+    scope_mng_ext ext = get_extension(env);
+    return !is_nil(ext.m_namespaces);
+}
+
 static int using_namespace_objects(lua_State * L) {
     int nargs = lua_gettop(L);
     environment const & env = to_environment(L, 1);

src/library/scoped_ext.h

@@ -26,6 +26,7 @@ environment using_namespace(environment const & env, io_state const & ios, name
 environment push_scope(environment const & env, io_state const & ios, bool section, name const & n = name());
 /** \brief Delete the most recent scope, all scoped extensions are notified. */
 environment pop_scope(environment const & env, name const & n = name());
+bool has_open_scopes(environment const & env);
 
 name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);

tests/lean/crash.lean

@@ -9,3 +9,4 @@ theorem crash
             from H,
             _.
 
+end

tests/lean/run/cody1.lean

@@ -22,3 +22,4 @@ theorem false_aux : ¬ (δ (i delta))
             have H' : r (i delta) (i delta),
               from eq_rec H (symm retract),
             H H'.
+end

tests/lean/run/cody2.lean

@@ -21,3 +21,5 @@ theorem delta_aux : ¬ (δ (i delta))
             H (subst (symm retract) H).
 
 check delta_aux.
+
+end

tests/lean/run/elab_bug1.lean

@@ -65,3 +65,4 @@ iff_elim_left (@congr_app _ _ R iff P C a b H) H1
 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 subst_iff H1 H2
 
+end congruence

tests/lean/run/univ_bug2.lean

@@ -27,3 +27,5 @@ theorem test1 (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) (Hf : f1 = f2)
 have Rs [fact] : simplifies_to f1 f2, from mk Hf,
 have Cs [fact] : simplifies_to s1 s2, from mk Hs,
 infer_eq _ _
+
+end simp