test(tests/lean): new tests for exercising the environment object

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

src/builtin/CMakeLists.txt

@@ -34,7 +34,7 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
   add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS})
   add_dependencies(builtin ${BASENAME}_builtin)
   install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
-  add_test("${BASENAME}_builtin_test" ${SHELL_DIR}/lean ${ARG} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE})
+  add_test("${BASENAME}_builtin_test" ${SHELL_DIR}/lean -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}_test ${ARG} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE})
 endfunction()
 
 # When cross compiling, we cannot execute lean during the build.

src/kernel/environment.cpp

@@ -386,7 +386,7 @@ void environment_cell::init_uvars() {
 */
 void environment_cell::check_no_cached_type(expr const & e) {
     if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); }))
-        throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers");
+        throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); // LCOV_EXCL_LINE
 }
 
 /**
@@ -411,7 +411,7 @@ void environment_cell::check_new_definition(name const & n, expr const & t, expr
 /** \brief Add a new builtin value to this environment */
 void environment_cell::add_builtin(expr const & v) {
     if (!is_value(v))
-        throw invalid_builtin_value_declaration(env(), v);
+        throw invalid_builtin_value_declaration(env(), v); // LCOV_EXCL_LINE
     name const & n = to_value(v).get_name();
     check_name(n);
     name const & u = to_value(v).get_unicode_name();
@@ -427,7 +427,7 @@ void environment_cell::add_builtin(expr const & v) {
 /** \brief Add a new builtin value set to this environment */
 void environment_cell::add_builtin_set(expr const & r) {
     if (!is_value(r))
-        throw invalid_builtin_value_declaration(env(), r);
+        throw invalid_builtin_value_declaration(env(), r); // LCOV_EXCL_LINE
     check_name(to_value(r).get_name());
     register_named_object(mk_builtin_set(r));
 }
@@ -531,17 +531,6 @@ expr environment_cell::normalize(expr const & e, context const & ctx, bool unfol
     return m_type_checker->get_normalizer()(e, ctx, unfold_opaque);
 }
 
-/** \brief Display universal variable constraints and objects stored in this environment and its parents. */
-void environment_cell::display(std::ostream & out) const {
-    if (has_parent())
-        m_parent->display(out);
-    for (object const & obj : m_objects) {
-        if (obj.has_name()) {
-            out << obj.keyword() << " " << obj.get_name() << "\n";
-        }
-    }
-}
-
 bool environment_cell::already_imported(name const & n) const {
     if (m_imported_modules.find(n) != m_imported_modules.end())
         return true;
@@ -752,7 +741,7 @@ name_map<std::pair<mk_builtin_fn, bool>> & get_available_builtins() {
 void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) {
     auto & bs = get_available_builtins();
     if (bs.find(n) != bs.end())
-        throw exception("invalid builtin object, system already has a builtin object with the given name");
+        throw exception("invalid builtin object, system already has a builtin object with the given name"); // LCOV_EXCL_LINE
     bs[n] = mk_pair(mk, is_builtin_set);
 }
 

src/kernel/environment.h

@@ -289,9 +289,6 @@ public:
     object_iterator end_local_objects() const { return object_iterator(m_this.lock(), get_num_objects(true), true); }
     // =======================================
 
-    /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
-    void display(std::ostream & out) const;
-
     /**
        \brief Register an environment extension. Every environment
        object will contain this extension. The funciton mk creates a

tests/lean/env_errors.lean

@@ -0,0 +1,29 @@
+
+variable x : Nat
+
+set::opaque x true.
+
+print "before import"
+(*
+local env = get_environment()
+env:import("tstblafoo.lean")
+*)
+
+print "before load1"
+(*
+local env = get_environment()
+env:load("tstblafoo.lean")
+*)
+
+print "before load2"
+(*
+local env = get_environment()
+env:load("fake1.olean")
+*)
+
+print "before load3"
+(*
+local env = get_environment()
+env:load("fake2.olean")
+*)
+

tests/lean/env_errors.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+Error (line: 4, pos: 0) set_opaque failed, 'x' is not a definition
+before import
+Error (line: 12, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH
+before load1
+Error (line: 18, pos: 0) failed to open file 'tstblafoo.lean'
+before load2
+Error (line: 24, pos: 0) corrupted binary file
+before load3
+Error (line: 30, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file

tests/lean/fake1.olean

@@ -0,0 +1 @@
+This is an invalid .olean file. It is used only for debugging purposes

tests/lean/univ2.lean

@@ -0,0 +1,7 @@
+universe Z >= max U+1 M+1
+print environment 2
+(*
+local env = get_environment()
+assert(env:get_universe_distance("Z", "U") == 1)
+assert(env:get_universe_distance("Z", "M") == 513)
+*)

tests/lean/univ2.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+import "kernel"
+import "Nat"
+universe Z ≥ U+1 ⊔ M+1