diff --git a/lean4-mode/lean4-flycheck.el b/lean4-mode/lean4-flycheck.el index 44fd6c0b56..38e0e97bcd 100644 --- a/lean4-mode/lean4-flycheck.el +++ b/lean4-mode/lean4-flycheck.el @@ -22,7 +22,7 @@ (let ((command (-concat `(,(lean4-get-executable lean4-executable-name)) lean4-extra-arguments - '("--json" "--make" "--stdin")))) + '("--json" "--stdin")))) command)) (defun lean4-bootstrapped-flycheck-command () diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 344124a785..4f7563af6e 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -98,69 +98,24 @@ if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) # COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean") endif() -# LEAN TESTS -file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") -add_test(NAME leantest_clear_all - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND "${CMAKE_COMMAND}" -E remove "*.test_suite.out" "*.status") -set_tests_properties(leantest_clear_all PROPERTIES FIXTURES_SETUP AllFiles) - -file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") -add_test(NAME leantest_all - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND bash "./test_all.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -set_tests_properties(leantest_all PROPERTIES DEPENDS leantest_clear_all # for cmake < 3.7 - FIXTURES_REQUIRED AllFiles - RUN_SERIAL 1) - FOREACH(T ${LEANTESTS}) if(NOT T MATCHES "\\.#") GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) - set_tests_properties("leantest_${T_NAME}" PROPERTIES DEPENDS "leantest_all;leantest_clear_all" - FIXTURES_REQUIRED AllFiles) endif() ENDFOREACH(T) -# LEAN RUN TESTS -file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean") -add_test(NAME leanruntest_clear_all - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND "${CMAKE_COMMAND}" -E remove "*.test_suite.out" "*.status") -set_tests_properties(leanruntest_clear_all PROPERTIES FIXTURES_SETUP AllFiles) - -file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean") -add_test(NAME leanruntest_all - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash "./test_all.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -set_tests_properties(leanruntest_all PROPERTIES DEPENDS leanruntest_clear_all # for cmake < 3.7 - FIXTURES_REQUIRED AllFiles - RUN_SERIAL 1) - FOREACH(T ${LEANRUNTESTS}) if(NOT T MATCHES "\\.#") GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) - set_tests_properties("leanruntest_${T_NAME}" PROPERTIES DEPENDS "leanruntest_all;leanruntest_clear_all" - FIXTURES_REQUIRED AllFiles) endif() ENDFOREACH(T) -# LEAN FAIL TESTS -file(GLOB LEANFAILTESTS "${LEAN_SOURCE_DIR}/../tests/lean/fail/*.lean") -add_test(NAME leanfailtest_clear_all - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/fail" - COMMAND "${CMAKE_COMMAND}" -E remove "*.test_suite.out" "*.status") -set_tests_properties(leanfailtest_clear_all PROPERTIES FIXTURES_SETUP AllFiles) -add_test(NAME leanfailtest_all - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/fail" - COMMAND bash "./test_all.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -set_tests_properties(leanfailtest_all PROPERTIES DEPENDS leanfailtest_clear_all # for cmake < 3.7 - FIXTURES_REQUIRED AllFiles RUN_SERIAL 1) FOREACH(T ${LEANFAILTESTS}) if(NOT T MATCHES "\\.#") GET_FILENAME_COMPONENT(T_NAME ${T} NAME) @@ -171,10 +126,6 @@ FOREACH(T ${LEANFAILTESTS}) add_test(NAME "leanfailtest2_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/fail" COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) - set_tests_properties("leanfailtest_${T_NAME}" PROPERTIES DEPENDS "leanfailtest_all;leanfailtest_clear_all" - FIXTURES_REQUIRED AllFiles) - set_tests_properties("leanfailtest2_${T_NAME}" PROPERTIES DEPENDS "leanfailtest_${T_NAME};leanfailtest_all;leanfailtest_clear_all" - FIXTURES_REQUIRED AllFiles) endif() ENDFOREACH(T) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 9a9f42334e..50cb35b9a7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -179,10 +179,9 @@ static void display_help(std::ostream & out) { std::cout << " --version -v display version number\n"; std::cout << " --githash display the git commit hash number used to build this binary\n"; std::cout << " --run executes the 'main' definition\n"; - std::cout << " --make create olean files\n"; + std::cout << " --make create olean file\n"; std::cout << " --cpp=fname -c name of the C++ output file\n"; - std::cout << " --stdin interpret stdin as content of single .lean file\n"; - std::cout << " --recursive recursively find *.lean files in directory arguments\n"; + std::cout << " --stdin take input from stdin\n"; std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n" << " and type check all imported modules\n"; std::cout << " --quiet -q do not print verbose messages\n"; @@ -206,7 +205,6 @@ static void display_help(std::ostream & out) { std::cout << " --debug=tag enable assertions with the given tag\n"; ) std::cout << " -D name=value set a configuration option (see set_option command)\n"; - std::cout << " --test-suite capture output and status code from each input file $f in $f.produced and $f.status, respectively\n"; } static struct option g_long_options[] = { @@ -215,14 +213,12 @@ static struct option g_long_options[] = { {"githash", no_argument, 0, 'g'}, {"make", no_argument, 0, 'm'}, {"stdin", no_argument, 0, 'i'}, - {"recursive", no_argument, 0, 'R'}, {"memory", required_argument, 0, 'M'}, {"trust", required_argument, 0, 't'}, {"profile", no_argument, 0, 'P'}, {"threads", required_argument, 0, 'j'}, {"quiet", no_argument, 0, 'q'}, {"deps", no_argument, 0, 'd'}, - {"test-suite", no_argument, 0, 'e'}, {"timeout", optional_argument, 0, 'T'}, {"cpp", optional_argument, 0, 'c'}, #if defined(LEAN_JSON) @@ -315,18 +311,16 @@ int main(int argc, char ** argv) { }); #endif ::initializer init; - bool make_mode = false; - bool use_stdin = false; - bool recursive = false; - unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1; - bool only_deps = false; - bool test_suite = false; + bool make_mode = false; + bool use_stdin = false; + unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1; + bool only_deps = false; // unsigned num_threads = 0; #if defined(LEAN_MULTI_THREAD) // num_threads = hardware_concurrency(); #endif #if defined(LEAN_JSON) - bool json_output = false; + bool json_output = false; #endif standard_search_path path; @@ -340,107 +334,100 @@ int main(int argc, char ** argv) { if (c == -1) break; // end of command line switch (c) { - case 'j': - // num_threads = static_cast(atoi(optarg)); - break; - case 'v': - display_header(std::cout); - return 0; - case 'g': - std::cout << LEAN_GITHASH << "\n"; - return 0; - case 'h': - display_help(std::cout); - return 0; - case 'c': - cpp_output = optarg; - break; - case 's': - lean::lthread::set_thread_stack_size(static_cast((atoi(optarg)/4)*4)*static_cast(1024)); - break; - case 'i': - use_stdin = true; - break; - case 'm': - make_mode = true; - recursive = true; - break; - case 'R': - recursive = true; - break; - case 'n': - native_output = optarg; - break; - case 'M': - opts = opts.update(get_max_memory_opt_name(), atoi(optarg)); - break; - case 'T': - opts = opts.update(get_timeout_opt_name(), atoi(optarg)); - break; - case 't': - trust_lvl = atoi(optarg); - break; - case 'q': - opts = opts.update(lean::get_verbose_opt_name(), false); - break; - case 'd': - only_deps = true; - break; - case 'D': - try { - opts = set_config_option(opts, optarg); - } catch (lean::exception & ex) { - std::cerr << ex.what() << std::endl; - return 1; - } - break; + case 'j': + // num_threads = static_cast(atoi(optarg)); + break; + case 'v': + display_header(std::cout); + return 0; + case 'g': + std::cout << LEAN_GITHASH << "\n"; + return 0; + case 'h': + display_help(std::cout); + return 0; + case 'c': + cpp_output = optarg; + break; + case 's': + lean::lthread::set_thread_stack_size( + static_cast((atoi(optarg) / 4) * 4) * static_cast(1024)); + break; + case 'i': + use_stdin = true; + break; + case 'm': + make_mode = true; + break; + case 'n': + native_output = optarg; + break; + case 'M': + opts = opts.update(get_max_memory_opt_name(), atoi(optarg)); + break; + case 'T': + opts = opts.update(get_timeout_opt_name(), atoi(optarg)); + break; + case 't': + trust_lvl = atoi(optarg); + break; + case 'q': + opts = opts.update(lean::get_verbose_opt_name(), false); + break; + case 'd': + only_deps = true; + break; + case 'D': + try { + opts = set_config_option(opts, optarg); + } catch (lean::exception & ex) { + std::cerr << ex.what() << std::endl; + return 1; + } + break; #if defined(LEAN_JSON) - case 'J': - opts = opts.update(lean::name{"trace", "as_messages"}, true); - json_output = true; - break; - case 'p': { - json out; + case 'J': + opts = opts.update(lean::name{"trace", "as_messages"}, true); + json_output = true; + break; + case 'p': { + json out; - auto & out_path = out["path"] = json::array(); - for (auto & p : path.get_path()) out_path.push_back(p); + auto & out_path = out["path"] = json::array(); + for (auto & p : path.get_path()) out_path.push_back(p); - out["leanpkg_path_file"] = path.m_leanpkg_path_fn ? *path.m_leanpkg_path_fn : path.m_user_leanpkg_path_fn; - out["is_user_leanpkg_path"] = !path.m_leanpkg_path_fn; + out["leanpkg_path_file"] = path.m_leanpkg_path_fn ? *path.m_leanpkg_path_fn + : path.m_user_leanpkg_path_fn; + out["is_user_leanpkg_path"] = !path.m_leanpkg_path_fn; - std::cout << std::setw(2) << out << std::endl; - return 0; - } + std::cout << std::setw(2) << out << std::endl; + return 0; + } #endif - case 'P': - opts = opts.update("profiler", true); - break; - case 'e': - test_suite = true; - opts = opts.update(lean::name{"trace", "as_messages"}, true); - break; + case 'P': + opts = opts.update("profiler", true); + break; #if defined(LEAN_DEBUG) - case 'B': - lean::enable_debug(optarg); - break; + case 'B': + lean::enable_debug(optarg); + break; #endif - default: - std::cerr << "Unknown command line option\n"; - display_help(std::cerr); - return 1; + default: + std::cerr << "Unknown command line option\n"; + display_help(std::cerr); + return 1; } } - if (use_stdin) - recursive = false; - if (auto max_memory = opts.get_unsigned(get_max_memory_opt_name(), - opts.get_bool("server") ? LEAN_SERVER_DEFAULT_MAX_MEMORY : LEAN_DEFAULT_MAX_MEMORY)) { + opts.get_bool("server") ? LEAN_SERVER_DEFAULT_MAX_MEMORY + : LEAN_DEFAULT_MAX_MEMORY)) { set_max_memory_megabyte(max_memory); } if (auto timeout = opts.get_unsigned(get_timeout_opt_name(), - opts.get_bool("server") ? LEAN_SERVER_DEFAULT_MAX_HEARTBEAT : LEAN_DEFAULT_MAX_HEARTBEAT)) { + opts.get_bool("server") ? LEAN_SERVER_DEFAULT_MAX_HEARTBEAT + : LEAN_DEFAULT_MAX_HEARTBEAT)) { set_max_heartbeat_thousands(timeout); } @@ -454,122 +441,83 @@ int main(int argc, char ** argv) { type_context_old trace_ctx(env, opts); scope_trace_env scope_trace(env, opts, trace_ctx); + std::string mod_fn, contents; + if (use_stdin) { + if (argc - optind != 0) { + std::cerr << "Expected exactly one of file name or --stdin\n"; + display_help(std::cerr); + return 1; + } + mod_fn = ""; + std::stringstream buf; + buf << std::cin.rdbuf(); + contents = buf.str(); + } else { + if (argc - optind != 1) { + std::cerr << "Expected exactly one file name\n"; + display_help(std::cerr); + return 1; + } + mod_fn = argv[optind]; + contents = read_file(mod_fn); + } try { module_mgr mod_mgr(path.get_path(), env, ios); mod_mgr.set_save_olean(make_mode); - std::vector args(argv + optind, argv + argc); - if (recursive) { - if (args.empty()) args.push_back("."); - std::vector files; - for (auto & f : args) { - if (auto i_d = is_dir(f)) { - if (*i_d) { - find_files(f, ".lean", files); - } else { - files.push_back(f); - } - } - } - args.clear(); - for (auto & f : files) { - if (is_lean_file(f)) - args.push_back(f); - } - } - std::vector module_args; - for (auto & f : args) module_args.push_back(lrealpath(f)); - + auto imports = mod_mgr.get_direct_imports(mod_fn, contents); if (only_deps) { - for (auto const & mod_fn : module_args) { - auto contents = read_file(mod_fn); - for (auto const & import : mod_mgr.get_direct_imports(mod_fn, contents)) { - std::string m_name = find_file(path.get_path(), import, {".lean"}); - auto last_idx = m_name.find_last_of("."); - std::string rawname = m_name.substr(0, last_idx); - std::string ext = m_name.substr(last_idx); - m_name = rawname + ".olean"; - std::cout << m_name << "\n"; - } + for (auto const & import : imports) { + std::string m_name = find_file(path.get_path(), import, {".lean"}); + auto last_idx = m_name.find_last_of("."); + std::string rawname = m_name.substr(0, last_idx); + std::string ext = m_name.substr(last_idx); + m_name = rawname + ".olean"; + std::cout << m_name << "\n"; } return 0; } - struct input_mod { - std::string m_file_name; - std::shared_ptr m_mod_info; - }; - std::vector mods; - for (auto & mod : module_args) { - auto mod_info = mod_mgr.get_module(module_name_of_file(path.get_path(), mod)); - mods.push_back({mod, mod_info}); + scope_traces_as_messages scope_trace_msgs(mod_fn, {1, 0}); + message_log l; + scope_message_log scope_log(l); + for (auto & d : imports) { + auto d_mod = mod_mgr.get_module(d); } - bool ok = true; + auto mod_env = import_modules(env, imports, mod_mgr.mk_loader()); + try { + std::stringstream ss; + ss << contents; + parser p(mod_env, ios, ss, mod_fn); + p.parse_commands(); + mod_env = p.env(); - if (use_stdin) { - std::stringstream buf; - buf << std::cin.rdbuf(); - - // This is where we will later spin off the server - scope_global_ios scope_ios(ios); - scope_traces_as_messages scope_trace_msgs("", {1, 0}); - message_log l; - scope_message_log scope_log(l); - auto imports = mod_mgr.get_direct_imports("", buf.str()); - std::set failed_imports; - for (auto & d : imports) { - auto d_mod = mod_mgr.get_module(d); - if (d_mod->m_log.has_errors()) - // error in this import - failed_imports.insert(d_mod->m_name); - else - // errors (maybe 0) in a transitive import - failed_imports.insert(d_mod->m_failed_deps.begin(), d_mod->m_failed_deps.end()); - } - for (auto const & d : failed_imports) { - message_builder msg(env, ios, "", {1, 0}, ERROR); - msg << "import " << d << " has errors, aborting"; - msg.report(); - ok = false; + if (make_mode && !l.has_errors()) { + auto olean_fn = olean_of_lean(mod_fn); + lean_trace("import", tout() << "saving " << olean_fn << "\n";); + time_task t(".olean serialization", + message_builder(environment(), get_global_ios(), mod_fn, pos_info(), + message_severity::INFORMATION)); + exclusive_file_lock output_lock(olean_fn); + std::ofstream out(olean_fn, std::ios_base::binary); + write_module(export_module(p.env(), mod_fn), out); + out.close(); + if (!out) throw exception("failed to write olean file"); } + } catch (exception const & ex) { + message_builder msg(env, ios, mod_fn, {1, 0}, ERROR); + msg.set_exception(ex); + report_message(msg.build()); + } - if (ok) { - try { - auto mod_env = import_modules(env, imports, mod_mgr.mk_loader()); - parser p(mod_env, ios, buf, ""); - // The server will obviously do something more complicated from here - p.parse_commands(); - } catch (exception const & ex) { - message_builder msg(env, ios, "", {1, 0}, ERROR); - msg.set_exception(ex); - report_message(msg.build()); - } - } - - for (auto const & msg : l.to_buffer()) { - if (json_output) { + for (auto const & msg : l.to_buffer()) { + if (json_output) { #if defined(LEAN_JSON) - print_json(std::cout, msg); + print_json(std::cout, msg); #endif - } else { - std::cout << msg; - } - } - if (l.has_errors()) - ok = false; - } - - for (auto & mod : mods) { - if (test_suite) { - std::ofstream out(mod.m_file_name + ".test_suite.out"); - for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) { - out << msg; - } - } - if (test_suite) { - std::ofstream status(mod.m_file_name + ".status"); - status << (!mod.m_mod_info->has_errors() ? 0 : 1); + } else { + std::cout << msg; } } @@ -577,37 +525,13 @@ int main(int argc, char ** argv) { display_cumulative_profiling_times(std::cerr); if (cpp_output) { - if (mods.size() != 1) { - std::cerr << "Error, option `--cpp=` expects one and only one input module\n"; - return 1; - } - module_name mod_name = mods[0].m_mod_info->m_name; - buffer dep_names; - for (auto d : mods[0].m_mod_info->m_deps) { - dep_names.push_back(d.m_mod_info->m_name); - } std::ofstream out(*cpp_output); - print_cpp_code(out, env, mod_name, to_list(dep_names)); + print_cpp_code(out, mod_env, mod_fn, to_list(imports.begin(), imports.end())); } - - if (!test_suite) { - for (auto & mod : mods) { - for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) { - if (json_output) { -#if defined(LEAN_JSON) - print_json(std::cout, msg); -#endif - } else { - std::cout << msg; - } - } - if (mod.m_mod_info->has_errors()) - ok = false; - } - } - return ok ? 0 : 1; + return l.has_errors() ? 1 : 0; } catch (lean::throwable & ex) { - std::cerr << lean::message_builder(env, ios, "", lean::pos_info(1, 1), lean::ERROR).set_exception(ex).build(); + std::cerr << lean::message_builder(env, ios, "", lean::pos_info(1, 1), lean::ERROR).set_exception( + ex).build(); } catch (std::bad_alloc & ex) { std::cerr << "out of memory" << std::endl; } diff --git a/tests/lean/fail/test_all.sh b/tests/lean/fail/test_all.sh deleted file mode 100755 index 04cc7c8eb2..0000000000 --- a/tests/lean/fail/test_all.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env bash -if [ $# -ne 1 ]; then - echo "Usage: test_all.sh [lean-executable-path]" - exit 1 -fi -ulimit -s 8192 -LEAN=$1 -export LEAN_PATH=../../../library:. -fs=() -for f in *.lean -do - ff=$(../readlinkf.sh "$f") - if [[ "$OSTYPE" == "msys" ]]; then - # Windows running MSYS2 - # Replace /c/ with c:, and / with \\ - ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g') - fi - fs+=("$ff") -done -"$LEAN" --test-suite "${fs[@]}" || (rm *.test_suite.out *.status; false) diff --git a/tests/lean/fail/test_single.sh b/tests/lean/fail/test_single.sh index 6f69077c11..484dc1e948 100644 --- a/tests/lean/fail/test_single.sh +++ b/tests/lean/fail/test_single.sh @@ -8,15 +8,8 @@ LEAN=$1 export LEAN_PATH=../../../library:. f=$2 echo "-- testing $f" -if [[ -f $f.status ]]; then - echo "-- using result from test_all.sh" - cat $f.test_suite.out - status=$(cat $f.status) - rm $f.test_suite.out $f.status -else - "$LEAN" -j 0 "$f" - status=$? -fi +"$LEAN" -j 0 "$f" +status=$? if [ "$status" -eq 1 ]; then echo "-- checked" else diff --git a/tests/lean/run/test_all.sh b/tests/lean/run/test_all.sh deleted file mode 100644 index db1928444d..0000000000 --- a/tests/lean/run/test_all.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/usr/bin/env bash -if [ $# -ne 1 ]; then - echo "Usage: test_all.sh [lean-executable-path]" - exit 1 -fi -ulimit -s 8192 -LEAN=$1 -export LEAN_PATH=../../../library:. -"$LEAN" --test-suite *.lean || (rm *.test_suite.out *.status; false) diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh index 900d380269..fff42176ae 100755 --- a/tests/lean/run/test_single.sh +++ b/tests/lean/run/test_single.sh @@ -8,15 +8,8 @@ LEAN=$1 export LEAN_PATH=../../../library:. f=$2 echo "-- testing $f" -if [[ -f $f.status ]]; then - echo "-- using result from test_all.sh" - cat $f.test_suite.out - status=$(cat $f.status) - rm $f.test_suite.out $f.status -else - "$LEAN" -j 0 "$f" - status=$? -fi +"$LEAN" -j 0 "$f" +status=$? if [ "$status" -eq 0 ]; then echo "-- checked" else diff --git a/tests/lean/test_all.sh b/tests/lean/test_all.sh deleted file mode 100755 index fa6965fb09..0000000000 --- a/tests/lean/test_all.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env bash -if [ $# -ne 1 ]; then - echo "Usage: test_all.sh [lean-executable-path]" - exit 1 -fi -ulimit -s 8192 -LEAN=$1 -export LEAN_PATH=../../library:. -fs=() -for f in *.lean -do - ff=$(./readlinkf.sh "$f") - if [[ "$OSTYPE" == "msys" ]]; then - # Windows running MSYS2 - # Replace /c/ with c:, and / with \\ - ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g') - fi - fs+=("$ff") -done -"$LEAN" --test-suite "${fs[@]}" || (rm *.test_suite.out *.status; false) diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index b475d397de..8a3edf2438 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -26,13 +26,7 @@ if diff --color --help >/dev/null 2>&1; then fi echo "-- testing $f" -if [[ -f "$f.status" ]]; then - echo "-- using result from test_all.sh" -else - "$LEAN" --test-suite "$ff" -fi -sed 's|does\\not\\exist|does/not/exist|' "$f.test_suite.out" | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out" -rm "$f.test_suite.out" "$f.status" +"$LEAN" "$ff" | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out" if test -f "$f.expected.out"; then if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then echo "-- checked"