From a71ead0fa0ad36e285e552114d441a004bce4d23 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 15 Dec 2023 12:51:13 +1100
Subject: [PATCH] more tests

---
 test/Mathlib/test/H20231215.expected.out   |  4 ++++
 test/Mathlib/test/H20231215.in             |  4 ++++
 test/Mathlib/test/H20231215_2.expected.out | 14 ++++++++++++++
 test/Mathlib/test/H20231215_2.in           |  3 +++
 test/pickle_open.expected.out              |  8 ++++++++
 test/pickle_open.in                        |  7 +++++++
 test/pickle_open_2.expected.out            |  4 ++++
 test/pickle_open_2.in                      |  3 +++
 test/pickle_open_scoped.in                 | 13 +++++++++++++
 test/pickle_open_scoped_2.in               |  5 +++++
 10 files changed, 65 insertions(+)
 create mode 100644 test/Mathlib/test/H20231215.expected.out
 create mode 100644 test/Mathlib/test/H20231215.in
 create mode 100644 test/Mathlib/test/H20231215_2.expected.out
 create mode 100644 test/Mathlib/test/H20231215_2.in
 create mode 100644 test/pickle_open.expected.out
 create mode 100644 test/pickle_open.in
 create mode 100644 test/pickle_open_2.expected.out
 create mode 100644 test/pickle_open_2.in
 create mode 100644 test/pickle_open_scoped.in
 create mode 100644 test/pickle_open_scoped_2.in

diff --git a/test/Mathlib/test/H20231215.expected.out b/test/Mathlib/test/H20231215.expected.out
new file mode 100644
index 0000000..c361ff1
--- /dev/null
+++ b/test/Mathlib/test/H20231215.expected.out
@@ -0,0 +1,4 @@
+{"env": 0}
+
+{"env": 0}
+
diff --git a/test/Mathlib/test/H20231215.in b/test/Mathlib/test/H20231215.in
new file mode 100644
index 0000000..246b30a
--- /dev/null
+++ b/test/Mathlib/test/H20231215.in
@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib\nopen BigOperators\nopen Real\nopen Nat"}
+
+{"pickleTo": "test/H20231215.olean", "env": 0}
+
diff --git a/test/Mathlib/test/H20231215_2.expected.out b/test/Mathlib/test/H20231215_2.expected.out
new file mode 100644
index 0000000..6eed89f
--- /dev/null
+++ b/test/Mathlib/test/H20231215_2.expected.out
@@ -0,0 +1,14 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 2, "column": 29},
+   "goal": "⊢ factorial 9 % 10 = 0",
+   "endPos": {"line": 2, "column": 34}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 30},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
diff --git a/test/Mathlib/test/H20231215_2.in b/test/Mathlib/test/H20231215_2.in
new file mode 100644
index 0000000..64b7c34
--- /dev/null
+++ b/test/Mathlib/test/H20231215_2.in
@@ -0,0 +1,3 @@
+{"unpickleEnvFrom": "test/H20231215.olean"}
+
+{"cmd": "theorem mathd_numbertheory_739 :\n  factorial 9 % 10 = 0 := by sorry", "env": 0}
diff --git a/test/pickle_open.expected.out b/test/pickle_open.expected.out
new file mode 100644
index 0000000..b00ebc3
--- /dev/null
+++ b/test/pickle_open.expected.out
@@ -0,0 +1,8 @@
+{"env": 0}
+
+{"env": 1}
+
+{"env": 2}
+
+{"env": 1}
+
diff --git a/test/pickle_open.in b/test/pickle_open.in
new file mode 100644
index 0000000..4684b7d
--- /dev/null
+++ b/test/pickle_open.in
@@ -0,0 +1,7 @@
+{"cmd": "def X.Y : Nat := 37"}
+
+{"cmd": "open X", "env": 0}
+
+{"cmd": "example : Y = 37 := rfl", "env": 1}
+
+{"pickleTo": "test/e.olean", "env": 1}
diff --git a/test/pickle_open_2.expected.out b/test/pickle_open_2.expected.out
new file mode 100644
index 0000000..ac49437
--- /dev/null
+++ b/test/pickle_open_2.expected.out
@@ -0,0 +1,4 @@
+{"env": 0}
+
+{"env": 1}
+
diff --git a/test/pickle_open_2.in b/test/pickle_open_2.in
new file mode 100644
index 0000000..d77744e
--- /dev/null
+++ b/test/pickle_open_2.in
@@ -0,0 +1,3 @@
+{"unpickleEnvFrom": "test/e.olean"}
+
+{"cmd": "example : Y = 37 := rfl", "env": 0}
diff --git a/test/pickle_open_scoped.in b/test/pickle_open_scoped.in
new file mode 100644
index 0000000..e268d6d
--- /dev/null
+++ b/test/pickle_open_scoped.in
@@ -0,0 +1,13 @@
+{"cmd": "namespace X"}
+
+{"cmd": "def f (x : Nat) := x + 37", "env": 0}
+
+{"cmd": "scoped notation:10000 n \"!\" => f n", "env": 1}
+
+{"cmd": "end X", "env": 2}
+
+{"cmd": "open X", "env": 3}
+
+{"cmd": "example : 39 = 2 ! := rfl", "env": 4}
+
+{"pickleTo": "test/f.olean", "env": 4}
diff --git a/test/pickle_open_scoped_2.in b/test/pickle_open_scoped_2.in
new file mode 100644
index 0000000..07d9bc6
--- /dev/null
+++ b/test/pickle_open_scoped_2.in
@@ -0,0 +1,5 @@
+{"unpickleEnvFrom": "test/f.olean"}
+
+{"cmd": "open scoped X", "env": 0}
+
+{"cmd": "example : 39 = X.f 2 := rfl", "env": 1}