From ed85ac254ad647f9de76333f1b47b5d4e6a5970f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Feb 2015 20:02:49 -0800
Subject: [PATCH] test(tests/lean): add more tests for error messages

---
 tests/lean/bad_namespace.lean              | 1 +
 tests/lean/bad_namespace.lean.expected.out | 1 +
 tests/lean/bad_open.lean                   | 3 +++
 tests/lean/bad_open.lean.expected.out      | 2 ++
 tests/lean/bad_print.lean                  | 7 +++++++
 tests/lean/bad_print.lean.expected.out     | 3 +++
 6 files changed, 17 insertions(+)
 create mode 100644 tests/lean/bad_namespace.lean
 create mode 100644 tests/lean/bad_namespace.lean.expected.out
 create mode 100644 tests/lean/bad_open.lean
 create mode 100644 tests/lean/bad_open.lean.expected.out
 create mode 100644 tests/lean/bad_print.lean
 create mode 100644 tests/lean/bad_print.lean.expected.out

diff --git a/tests/lean/bad_namespace.lean b/tests/lean/bad_namespace.lean
new file mode 100644
index 000000000..b5a3ba24b
--- /dev/null
+++ b/tests/lean/bad_namespace.lean
@@ -0,0 +1 @@
+namespace _root_
diff --git a/tests/lean/bad_namespace.lean.expected.out b/tests/lean/bad_namespace.lean.expected.out
new file mode 100644
index 000000000..0238afd21
--- /dev/null
+++ b/tests/lean/bad_namespace.lean.expected.out
@@ -0,0 +1 @@
+bad_namespace.lean:1:10: error: invalid namespace name, '_root_' is reserved
diff --git a/tests/lean/bad_open.lean b/tests/lean/bad_open.lean
new file mode 100644
index 000000000..254a12fea
--- /dev/null
+++ b/tests/lean/bad_open.lean
@@ -0,0 +1,3 @@
+open "nat"
+
+open [classes] "nat"
diff --git a/tests/lean/bad_open.lean.expected.out b/tests/lean/bad_open.lean.expected.out
new file mode 100644
index 000000000..ef40eec37
--- /dev/null
+++ b/tests/lean/bad_open.lean.expected.out
@@ -0,0 +1,2 @@
+bad_open.lean:1:5: error: invalid 'open/export' command, identifier expected
+bad_open.lean:3:15: error: invalid 'open/export' command, identifier expected
diff --git a/tests/lean/bad_print.lean b/tests/lean/bad_print.lean
new file mode 100644
index 000000000..d11b42dcb
--- /dev/null
+++ b/tests/lean/bad_print.lean
@@ -0,0 +1,7 @@
+constant boo : nat
+
+print definition boo
+
+print 2
+
+print fields nat
diff --git a/tests/lean/bad_print.lean.expected.out b/tests/lean/bad_print.lean.expected.out
new file mode 100644
index 000000000..4401d8835
--- /dev/null
+++ b/tests/lean/bad_print.lean.expected.out
@@ -0,0 +1,3 @@
+bad_print.lean:3:17: error: invalid 'print definition', 'boo' is not a definition
+bad_print.lean:5:6: error: invalid print command
+bad_print.lean:7:13: error: invalid 'print fields' command, 'nat' is not a structure