test(tests/lean/extra): add test for issue #597

src/shell/CMakeLists.txt

@@ -43,6 +43,9 @@ add_test(NAME "lean_print_notation"
 add_test(NAME "auto_completion_issue_422"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./ac_bug.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "issue_597"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./issue_597.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")

tests/lean/extra/597a.hlean

@@ -0,0 +1,4 @@
+open equiv
+open equiv.ops
+constants (A B : Type₀) (f : A ≃ B)
+definition foo : A → B := f

tests/lean/extra/597b.hlean

@@ -0,0 +1,4 @@
+open equiv
+-- open equiv.ops
+constants (A B : Type₀) (f : A ≃ B)
+definition foo : A → B := f -- should fail

tests/lean/extra/issue_597.sh

@@ -0,0 +1,13 @@
+#!/bin/bash
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: bug_597.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export HLEAN_PATH=../../../hott
+"$LEAN" -c 597.clean 597a.hlean
+if "$LEAN" -c 597.clean 597b.hlean; then
+    echo "ERROR: using incorrect cached value..."
+    exit 1
+fi