From 2a6ccb252e86febe96e303f5f82414cd4d26a733 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Feb 2015 10:55:03 -0800
Subject: [PATCH] test(tests/lean/extra): add regression tests for issue #422

---
 src/shell/CMakeLists.txt       |  3 +++
 tests/lean/extra/ac_bug.sh     | 19 +++++++++++++++++++
 tests/lean/extra/ac_bug1.input |  9 +++++++++
 tests/lean/extra/ac_bug2.input |  9 +++++++++
 tests/lean/extra/ac_bug3.input | 10 ++++++++++
 tests/lean/extra/ac_bug4.input | 10 ++++++++++
 tests/lean/extra/ac_bug5.input |  9 +++++++++
 tests/lean/extra/ac_bug6.input | 10 ++++++++++
 8 files changed, 79 insertions(+)
 create mode 100755 tests/lean/extra/ac_bug.sh
 create mode 100644 tests/lean/extra/ac_bug1.input
 create mode 100644 tests/lean/extra/ac_bug2.input
 create mode 100644 tests/lean/extra/ac_bug3.input
 create mode 100644 tests/lean/extra/ac_bug4.input
 create mode 100644 tests/lean/extra/ac_bug5.input
 create mode 100644 tests/lean/extra/ac_bug6.input

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 7e87e0903..a5f782b42 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -40,6 +40,9 @@ add_test(NAME "lean_eqn_macro"
 add_test(NAME "lean_print_notation"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_tests.lean")
+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")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/tests/lean/extra/ac_bug.sh b/tests/lean/extra/ac_bug.sh
new file mode 100755
index 000000000..aecc6c5d2
--- /dev/null
+++ b/tests/lean/extra/ac_bug.sh
@@ -0,0 +1,19 @@
+#!/bin/sh
+# Regression test for issue https://github.com/leanprover/lean/issues/422
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: ac_bug.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export LEAN_PATH=../../../library:.
+for f in `ls ac_bug*.input`; do
+    echo "testing $f..."
+    $LEAN --server-trace $f > $f.produced.out
+    if grep "nat.mul.assoc" $f.produced.out; then
+        echo "FAILED"
+        exit 1
+    fi
+    rm -f $f.produced.out
+done
+echo "done"
diff --git a/tests/lean/extra/ac_bug1.input b/tests/lean/extra/ac_bug1.input
new file mode 100644
index 000000000..15faa9dab
--- /dev/null
+++ b/tests/lean/extra/ac_bug1.input
@@ -0,0 +1,9 @@
+VISIT ac_bug.lean
+SYNC 4
+import data.nat
+namespace nat
+check mul.as
+exit
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug2.input b/tests/lean/extra/ac_bug2.input
new file mode 100644
index 000000000..83f1e944c
--- /dev/null
+++ b/tests/lean/extra/ac_bug2.input
@@ -0,0 +1,9 @@
+VISIT ac_bug.lean
+SYNC 4
+import data.nat
+namespace nat
+check mul.as
+end nat
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug3.input b/tests/lean/extra/ac_bug3.input
new file mode 100644
index 000000000..6ab990690
--- /dev/null
+++ b/tests/lean/extra/ac_bug3.input
@@ -0,0 +1,10 @@
+VISIT ac_bug.lean
+SYNC 5
+import data.nat
+namespace nat
+check mul.as
+end
+nat
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug4.input b/tests/lean/extra/ac_bug4.input
new file mode 100644
index 000000000..1a513b7f2
--- /dev/null
+++ b/tests/lean/extra/ac_bug4.input
@@ -0,0 +1,10 @@
+VISIT ac_bug.lean
+SYNC 5
+import data.nat
+namespace nat
+check mul.as
+def a := 10
+end nat
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug5.input b/tests/lean/extra/ac_bug5.input
new file mode 100644
index 000000000..3ec26dcfe
--- /dev/null
+++ b/tests/lean/extra/ac_bug5.input
@@ -0,0 +1,9 @@
+VISIT ac_bug.lean
+SYNC 4
+import data.nat
+namespace nat
+check mul.as
+def a := 10
+WAIT
+FINDP 3
+mul.as
diff --git a/tests/lean/extra/ac_bug6.input b/tests/lean/extra/ac_bug6.input
new file mode 100644
index 000000000..8495814ae
--- /dev/null
+++ b/tests/lean/extra/ac_bug6.input
@@ -0,0 +1,10 @@
+VISIT ac_bug.lean
+SYNC 5
+import data.nat
+namespace nat
+check mul.as
+def a := 10
+exit
+WAIT
+FINDP 3
+mul.as