add gc option tests

Author: RexWzh

test/gc.expected.in

@@ -0,0 +1,17 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 5},
+   "data": "true"}]}
+
+{"message": "Unknown environment."}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 5},
+   "data": "37"}],
+ "env": 1}
+

test/gc.in

@@ -0,0 +1,7 @@
+{"cmd": "def f := 37"}
+
+{"cmd": "#eval true", "gc": true}
+
+{"cmd": "#eval false", "env":1}
+
+{"cmd": "#eval f", "env":0}

test/gc_tactic.expected.in

@@ -0,0 +1,44 @@
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 20},
+   "endPos": null,
+   "data": "unexpected end of input; expected '{'"},
+  {"severity": "error",
+   "pos": {"line": 1, "column": 18},
+   "endPos": {"line": 1, "column": 20},
+   "data": "unsolved goals\n⊢ 2 = 2"}],
+ "env": 0}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 2, "column": 3},
+   "data": "Goals accomplished!"}],
+ "env": 1}
+
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 66},
+   "endPos": null,
+   "data": "unexpected end of input; expected '{'"},
+  {"severity": "error",
+   "pos": {"line": 1, "column": 64},
+   "endPos": {"line": 1, "column": 66},
+   "data": "unsolved goals\nP Q R : Prop\n⊢ (P → Q) → (Q → R) → P → R"}]}
+
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 64},
+   "endPos": {"line": 2, "column": 13},
+   "data": "unsolved goals\nP Q R : Prop\nh1 : P → Q\nh2 : Q → R\np : P\n⊢ R"}]}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 3, "column": 0},
+   "endPos": {"line": 3, "column": 6},
+   "data": "Try this: exact h2 (h1 p)"},
+  {"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 3, "column": 6},
+   "data": "Goals accomplished!"}]}
+

test/gc_tactic.in

@@ -0,0 +1,9 @@
+{"cmd": "example  : 2=2 := by"}
+
+{"cmd": "example  : 2=2 := by\nrfl"}
+
+{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by", "gc": true}
+
+{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p", "gc": true}
+
+{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p\napply?", "gc": true}