fix(frontends/lean): bug in pop::context command, and add new tests for the universe command

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

src/frontends/lean/parser_cmds.cpp

@@ -656,11 +656,15 @@ static name g_geq(">=");
 void parser_imp::parse_universe() {
     next();
     name id   = check_identifier_next("invalid universe constraint, identifier expected");
-    name geq  = check_identifier_next("invalid universe constraint, '>=' expected");
-    if (geq != g_geq && geq != g_geq_unicode)
-        throw parser_error("invalid universe constraint, '>=' expected", m_last_cmd_pos);
-    level lvl = parse_level();
-    m_env->add_uvar_cnstr(id, lvl);
+    if (curr_is_identifier()) {
+        name geq  = check_identifier_next("invalid universe constraint, '>=' expected");
+        if (geq != g_geq && geq != g_geq_unicode)
+            throw parser_error("invalid universe constraint, '>=' expected", m_last_cmd_pos);
+        level lvl = parse_level();
+        m_env->add_uvar_cnstr(id, lvl);
+    } else {
+        m_env->add_uvar_cnstr(id);
+    }
 }
 
 void parser_imp::parse_alias() {
@@ -728,6 +732,7 @@ void parser_imp::parse_pop() {
     m_scope_kinds.pop_back();
     reset_env(m_env->parent());
     m_using_decls.pop();
+    m_script_state->apply([&](lua_State * L) { lua_gc(L, LUA_GCCOLLECT, 0); });
 }
 
 void parser_imp::parse_namespace() {
@@ -744,7 +749,7 @@ void parser_imp::parse_end() {
         throw parser_error("invalid 'end', not inside of a scope or namespace", m_last_cmd_pos);
     scope_kind k = m_scope_kinds.back();
     m_scope_kinds.pop_back();
-    m_script_state->apply([&](lua_State * L) { lua_gc(L, LUA_GCCOLLECT, LUA_TUSERDATA); });
+    m_script_state->apply([&](lua_State * L) { lua_gc(L, LUA_GCCOLLECT, 0); });
     switch (k) {
     case scope_kind::Scope: {
         if (!m_env->has_parent())

tests/lean/univ.lean

@@ -0,0 +1,40 @@
+
+universe Z ≥ M+3
+(*
+local env = get_environment()
+assert(env:get_universe_distance("Z", "M") == 3)
+assert(not env:get_universe_distance("Z", "U"))
+*)
+
+scope
+  universe Z ≥ U + 10
+  (*
+    local env = get_environment()
+    assert(env:get_universe_distance("Z", "U") == 10)
+    assert(env:get_universe_distance("Z", "M") ==
+              env:get_universe_distance("Z", "U") +
+              env:get_universe_distance("U", "M"))
+  *)
+pop::scope
+
+(*
+local env = get_environment()
+assert(env:get_universe_distance("Z", "M") == 3)
+assert(not env:get_universe_distance("Z", "U"))
+*)
+
+universe Z1 ≥ U + 1073741824.
+universe Z2 ≥ Z1 + 1073741824.
+
+universe U1
+universe U2 ≥ U1 + 1
+universe U3 ≥ U1 + 1
+universe U4 ≥ U2 + 1
+universe U4 ≥ U3 + 3
+(*
+local env = get_environment()
+assert(env:get_universe_distance("U4", "U1") == 4)
+assert(env:get_universe_distance("U4", "U3") == 3)
+assert(env:get_universe_distance("U4", "U2") == 1)
+*)
+universe U1 ≥ U4.

tests/lean/univ.lean.expected.out

@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+Error (line: 27, pos: 31) integer overflow
+Error (line: 40, pos: 0) universe constraint inconsistency: U1 >= U4 + 0