Skip to content

Commit f867ab2

Browse files
RexWzhRexWzh
committed
rename gc to discard 
1 parent bac41b9 commit f867ab2

11 files changed

+102
-11
lines changed

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,13 @@ Commands may be of the form
2121
```
2222

2323
```json
24-
{ "cmd" : "example : f = 2 := rfl", "env" : 1, "gc": true }
24+
{ "cmd" : "example : f = 2 := rfl", "env" : 1, "discard": true }
2525
```
2626

2727
The input includes:
2828
* A required `cmd` field containing the Lean command to execute
2929
* An optional `env` field specifying a previous environment ID to build upon
30-
* An optional `gc` field (default: false) to discard the environment after execution
30+
* An optional `discard` field (default: false) to discard the environment after execution
3131
* Optional fields for additional information:
3232
* `allTactics`: when true, includes all tactic steps in the response
3333
* `rootGoals`: when true, includes root goals as sorries
@@ -46,7 +46,7 @@ You can backtrack simply by using earlier values for `env`.
4646
The response includes:
4747
* A numeric label for the `Environment` after your command,
4848
which you can use as the starting point for subsequent commands.
49-
This will be `none` if `gc` was enabled.
49+
This will be `none` if `discard` was enabled.
5050
* Any messages generated while processing your command.
5151
* A list of the `sorry`s in your command, including
5252
* their expected type, and

‎REPL/JSON.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,13 @@ structure CommandOptions where
2323
/-- Run Lean commands.
2424
If `env = none`, starts a new session (in which you can use `import`).
2525
If `env = some n`, builds on the existing environment `n`.
26-
Setting `gc = true` will discard the environment after execution, useful for memory management.
27-
When `gc = true`, the response's `env` field will be `none`.
26+
Setting `discard = true` will discard the environment after execution, useful for memory management.
27+
When `discard = true`, the response's `env` field will be `none`.
2828
-/
2929
structure Command extends CommandOptions where
3030
env : Option Nat
3131
cmd : String
32-
gc : Option Bool := false
32+
discard : Option Bool := false
3333
deriving ToJson, FromJson
3434

3535
/-- Process a Lean file in a fresh environment. -/

‎REPL/Main.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -322,7 +322,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
322322
fileMap := default,
323323
snap? := none,
324324
cancelTk? := none } }
325-
let env ← match s.gc with
325+
let env ← match s.discard with
326326
| some true => pure none
327327
| _ => do
328328
let id ← recordCommandSnapshot cmdSnapshot

‎test/Mathlib/test/discardCmd.expected.out‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
{"env": 0}
2+
3+
{"sorries":
4+
[{"proofState": 0,
5+
"pos": {"line": 1, "column": 93},
6+
"goal": "⊢ (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0",
7+
"endPos": {"line": 1, "column": 98}}],
8+
"messages":
9+
[{"severity": "warning",
10+
"pos": {"line": 1, "column": 8},
11+
"endPos": {"line": 1, "column": 30},
12+
"data": "declaration uses 'sorry'"}],
13+
"env": 1}
14+
15+
{"proofStatus": "Completed", "proofState": 1, "goals": []}
16+
17+
{"sorries":
18+
[{"proofState": 2,
19+
"pos": {"line": 1, "column": 93},
20+
"goal": "⊢ (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0",
21+
"endPos": {"line": 1, "column": 98}}],
22+
"messages":
23+
[{"severity": "warning",
24+
"pos": {"line": 1, "column": 8},
25+
"endPos": {"line": 1, "column": 30},
26+
"data": "declaration uses 'sorry'"}],
27+
"env": 2}
28+
29+
{"proofStatus": "Completed", "proofState": 3, "goals": []}
30+

‎test/Mathlib/test/discardCmd.in‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
{"cmd": "import Mathlib"}
2+
3+
{"cmd": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0 := sorry", "env":0, "discard": true}
4+
5+
{"tactic": "norm_num", "proofState": 0}
6+
7+
{"cmd": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0 := sorry", "env":0}
8+
9+
{"tactic": "norm_num", "proofState": 2}

‎test/gc.expected.out‎ renamed to ‎test/discardCmd.expected.out‎

File renamed without changes.

‎test/gc.in‎ renamed to ‎test/discardCmd.in‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
{"cmd": "def f := 37"}
22

3-
{"cmd": "#eval true", "gc": true}
3+
{"cmd": "#eval true", "discard": true}
44

55
{"cmd": "#eval false", "env":1}
66

‎test/gc_tactic.expected.out‎ renamed to ‎test/discardCmd2.expected.out‎

File renamed without changes.

‎test/gc_tactic.in‎ renamed to ‎test/discardCmd2.in‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22

33
{"cmd": "example : 2=2 := by\nrfl"}
44

5-
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by", "gc": true}
5+
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by", "discard": true}
66

7-
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p", "gc": true}
7+
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p", "discard": true}
88

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

‎test/discardCmd_proof.expected.out‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
{"sorries":
2+
[{"proofState": 0,
3+
"pos": {"line": 1, "column": 20},
4+
"goal": "⊢ 1 = 1",
5+
"endPos": {"line": 1, "column": 25}}],
6+
"messages":
7+
[{"severity": "warning",
8+
"pos": {"line": 1, "column": 0},
9+
"endPos": {"line": 1, "column": 7},
10+
"data": "declaration uses 'sorry'"}]}
11+
12+
{"sorries":
13+
[{"proofState": 1,
14+
"pos": {"line": 1, "column": 20},
15+
"goal": "⊢ 1 = 1",
16+
"endPos": {"line": 1, "column": 25}}],
17+
"messages":
18+
[{"severity": "warning",
19+
"pos": {"line": 1, "column": 0},
20+
"endPos": {"line": 1, "column": 7},
21+
"data": "declaration uses 'sorry'"}],
22+
"env": 0}
23+
24+
{"sorries":
25+
[{"proofState": 2,
26+
"pos": {"line": 1, "column": 20},
27+
"goal": "⊢ 1 = 1",
28+
"endPos": {"line": 1, "column": 25}}],
29+
"messages":
30+
[{"severity": "warning",
31+
"pos": {"line": 1, "column": 0},
32+
"endPos": {"line": 1, "column": 7},
33+
"data": "declaration uses 'sorry'"}],
34+
"env": 1}
35+
36+
{"proofStatus": "Completed", "proofState": 3, "goals": []}
37+
38+
{"proofStatus": "Completed", "proofState": 4, "goals": []}
39+
40+
{"proofStatus": "Completed", "proofState": 5, "goals": []}
41+

0 commit comments

Comments
 (0)