From e0b39079eb07317a27cd361e2474325eaca5f1cc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 May 2015 15:26:13 -0700
Subject: [PATCH] test(tests/lean/extra): add test for issue #597

---
 src/shell/CMakeLists.txt      |  3 +++
 tests/lean/extra/597a.hlean   |  4 ++++
 tests/lean/extra/597b.hlean   |  4 ++++
 tests/lean/extra/issue_597.sh | 13 +++++++++++++
 4 files changed, 24 insertions(+)
 create mode 100644 tests/lean/extra/597a.hlean
 create mode 100644 tests/lean/extra/597b.hlean
 create mode 100755 tests/lean/extra/issue_597.sh

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 56aa9f1160..847f7c180f 100644
--- a/src/shell/CMakeLists.txt
+++ b/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")
diff --git a/tests/lean/extra/597a.hlean b/tests/lean/extra/597a.hlean
new file mode 100644
index 0000000000..4bed446749
--- /dev/null
+++ b/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
diff --git a/tests/lean/extra/597b.hlean b/tests/lean/extra/597b.hlean
new file mode 100644
index 0000000000..c7bdb2583e
--- /dev/null
+++ b/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
diff --git a/tests/lean/extra/issue_597.sh b/tests/lean/extra/issue_597.sh
new file mode 100755
index 0000000000..e0085b2e66
--- /dev/null
+++ b/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