max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(shell/lean): accept stand-alone files as input

Browse source 
@leodemoura
This commit is contained in:
Sebastian Ullrich 2019-03-22 14:03:52 +01:00
parent fa0381cecf
commit 5f7a63b34b
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/CMakeLists.txt
View file

@ -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

6
src/shell/lean.cpp
View file

@ -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});