diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 56e222404..9bc741d33 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1679,6 +1679,7 @@ void parser::parse_imports() { bool prelude = false; std::string base = dirname(get_stream_name().c_str()); bool imported = false; + unsigned fingerprint = 0; if (curr_is_token(get_prelude_tk())) { next(); prelude = true; @@ -1716,6 +1717,9 @@ void parser::parse_imports() { if (!curr_is_identifier()) break; name f = get_name_val(); + fingerprint = hash(fingerprint, f.hash()); + if (k) + fingerprint = hash(fingerprint, *k); if (auto it = try_file(f, ".lua")) { if (k) throw parser_error(sstream() << "invalid import, failed to import '" << f @@ -1733,6 +1737,7 @@ void parser::parse_imports() { bool keep_imported_thms = (m_keep_theorem_mode == keep_theorem_mode::All); m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads, keep_imported_thms, m_ios); + m_env = update_fingerprint(m_env, fingerprint); for (auto const & f : lua_files) { std::string rname = find_file(f, {".lua"}); system_import(rname.c_str()); diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 847f7c180..22e9d2903 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -46,6 +46,9 @@ add_test(NAME "auto_completion_issue_422" add_test(NAME "issue_597" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" COMMAND bash "./issue_597.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") +add_test(NAME "issue_616" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" + COMMAND bash "./issue_616.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/tests/lean/extra/616a.hlean b/tests/lean/extra/616a.hlean new file mode 100644 index 000000000..32edb4a9d --- /dev/null +++ b/tests/lean/extra/616a.hlean @@ -0,0 +1 @@ +attribute type_quotient.rec [recursor] diff --git a/tests/lean/extra/616b.hlean b/tests/lean/extra/616b.hlean new file mode 100644 index 000000000..82bc0f39e --- /dev/null +++ b/tests/lean/extra/616b.hlean @@ -0,0 +1,9 @@ +import .f616a +open eq +definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : type_quotient R) : P := +begin + induction x, + exact (Pc a), + refine (!tr_constant ⬝ Pp H) +end diff --git a/tests/lean/extra/616c.hlean b/tests/lean/extra/616c.hlean new file mode 100644 index 000000000..1ac3d79d8 --- /dev/null +++ b/tests/lean/extra/616c.hlean @@ -0,0 +1,8 @@ +open eq +definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : type_quotient R) : P := +begin + induction x, + exact (Pc a), + refine (!tr_constant ⬝ Pp H) +end diff --git a/tests/lean/extra/issue_616.sh b/tests/lean/extra/issue_616.sh new file mode 100755 index 000000000..5c7437c91 --- /dev/null +++ b/tests/lean/extra/issue_616.sh @@ -0,0 +1,14 @@ +#!/bin/bash +set -e +if [ $# -ne 1 ]; then + echo "Usage: issue_616.sh [lean-executable-path]" + exit 1 +fi +LEAN=$1 +export HLEAN_PATH=../../../hott +"$LEAN" -o f616a.olean 616a.hlean +"$LEAN" -c 616.clean 616b.hlean +if "$LEAN" -c 616.clean 616c.hlean; then + echo "ERROR: using incorrect cached value..." + exit 1 +fi