more tests

test/Mathlib/test/H20231215.expected.out

@@ -0,0 +1,4 @@
+{"env": 0}
+
+{"env": 0}
+

test/Mathlib/test/H20231215.in

@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib\nopen BigOperators\nopen Real\nopen Nat"}
+
+{"pickleTo": "test/H20231215.olean", "env": 0}
+

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}
+

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}

test/pickle_open.expected.out

@@ -0,0 +1,8 @@
+{"env": 0}
+
+{"env": 1}
+
+{"env": 2}
+
+{"env": 1}
+

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}

test/pickle_open_2.expected.out

@@ -0,0 +1,4 @@
+{"env": 0}
+
+{"env": 1}
+

test/pickle_open_2.in

@@ -0,0 +1,3 @@
+{"unpickleEnvFrom": "test/e.olean"}
+
+{"cmd": "example : Y = 37 := rfl", "env": 0}

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}

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}