diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index ed567a4b58..d250e56c0f 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -86,7 +86,7 @@ add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g) add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash) add_test(lean_path1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -p) add_test(lean_path2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --path) -# add_test(lean_new_frontend "${CMAKE_CURRENT_BINARY_DIR}/lean" --new-frontend "${LEAN_SOURCE_DIR}/../library/init/core.lean") +add_test(lean_new_frontend "${CMAKE_CURRENT_BINARY_DIR}/lean" --new-frontend "${LEAN_SOURCE_DIR}/../library/init/core.lean") add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") # The following test needs new elaborator to support match diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index a8b4daa172..8e9e52fef2 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -467,7 +467,11 @@ int main(int argc, char ** argv) { } mod_fn = lrealpath(argv[optind]); contents = read_file(mod_fn); - env = set_main_module_name(env, module_name_of_file(path.get_path(), mod_fn)); + search_path input_path = path.get_path(); + /* We accept stand-alone files as input, but imports should always be part of a package so that we can give + * them a (stable) absolute name. */ + input_path.push_back(dirname(mod_fn)); + env = set_main_module_name(env, module_name_of_file(input_path, mod_fn)); } try { scope_traces_as_messages scope_trace_msgs(mod_fn, {1, 0});