test(tests/shared/env): add import module test

src/api/lean.h

@@ -17,5 +17,7 @@ Author: Leonardo de Moura
 #include "lean_expr.h"          // NOLINT
 #include "lean_decl.h"          // NOLINT
 #include "lean_env.h"           // NOLINT
+#include "lean_ios.h"           // NOLINT
+#include "lean_module.h"        // NOLINT
 
 #endif

src/api/lean_module.h

@@ -27,6 +27,12 @@ lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, le
 /** \brief Export to the given file name the declarations added to the environment */
 lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex);
 
+/** \brief Store in \c r the LEAN_PATH */
+lean_bool lean_get_std_path(char const ** r, lean_exception * ex);
+
+/** \brief Store in \c r the HLEAN_PATH */
+lean_bool lean_get_hott_path(char const ** r, lean_exception * ex);
+
 /*@}*/
 /*@}*/
 

src/api/module.cpp

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/lean_path.h"
 #include "library/module.h"
+#include "library/util.h"
 #include "api/decl.h"
 #include "api/string.h"
 #include "api/exception.h"
@@ -13,11 +15,21 @@ Author: Leonardo de Moura
 #include "api/lean_module.h"
 using namespace lean; // NOLINT
 
+static bool g_std_path = true;
+
+static void set_lean_path(bool std) {
+    if (g_std_path != std) {
+        initialize_lean_path(!std);
+        g_std_path = std;
+    }
+}
+
 lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, lean_env * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(env);
     check_nonnull(ios);
     check_nonnull(modules);
+    set_lean_path(is_standard(to_env_ref(env)));
     buffer<module_name> ms;
     for (name const & n : to_list_name_ref(modules)) {
         ms.push_back(module_name(n));
@@ -35,3 +47,17 @@ lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex)
     export_module(out, to_env_ref(env));
     LEAN_CATCH;
 }
+
+lean_bool lean_get_std_path(char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    set_lean_path(true);
+    *r = mk_string(get_lean_path());
+    LEAN_CATCH;
+}
+
+lean_bool lean_get_hott_path(char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    set_lean_path(false);
+    *r = mk_string(get_lean_path());
+    LEAN_CATCH;
+}

src/tests/shared/CMakeLists.txt

@@ -33,3 +33,5 @@ target_link_libraries(c_env_test ${EXTRA_LIBS} leanshared)
 add_test(ENV c_env_test
          WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
          COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_env_test")
+SET_TESTS_PROPERTIES(ENV
+  PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_SOURCE_DIR}/../library")

src/tests/shared/env.c

@@ -208,8 +208,52 @@ void test_id() {
     lean_name_del(id_name);
 }
 
+void test_path() {
+    lean_exception ex;
+    char const * p;
+    check(lean_get_std_path(&p, &ex));
+    printf("LEAN_PATH: %s\n", p);
+    lean_string_del(p);
+    check(lean_get_hott_path(&p, &ex));
+    printf("HLEAN_PATH: %s\n", p);
+    lean_string_del(p);
+}
+
+void print_decl_name_and_del(lean_decl d) {
+    lean_exception ex;
+    lean_name n;
+    char const * s;
+    check(lean_decl_get_name(d, &n, &ex));
+    check(lean_name_to_string(n, &s, &ex));
+    printf("declaration name: %s\n", s);
+    lean_string_del(s);
+    lean_decl_del(d);
+}
+
+void test_import() {
+    lean_exception ex;
+    lean_env  env = mk_env();
+    lean_name std = mk_name("standard");
+    lean_list_name ms = mk_unary_name_list(std);
+    lean_options o;
+    lean_ios ios;
+    lean_env new_env;
+    check(lean_options_mk_empty(&o, &ex));
+    check(lean_ios_mk_std(o, &ios, &ex));
+    check(lean_env_import(env, ios, ms, &new_env, &ex));
+    check(lean_env_for_each_decl(new_env, print_decl_name_and_del, &ex));
+    lean_env_del(env);
+    lean_name_del(std);
+    lean_list_name_del(ms);
+    lean_options_del(o);
+    lean_ios_del(ios);
+    lean_env_del(new_env);
+}
+
 int main() {
     test_add_univ();
     test_id();
+    test_path();
+    test_import();
     return 0;
 }