rename discard to record

Author: RexWzh

README.md

@@ -21,13 +21,13 @@ Commands may be of the form
 ```
 
 ```json
-{ "cmd" : "example : f = 2 := rfl", "env" : 1, "discard": true }
+{ "cmd" : "example : f = 2 := rfl", "env" : 1, "record": true }
 ```
 
 The input includes:
 * A required `cmd` field containing the Lean command to execute
 * An optional `env` field specifying a previous environment ID to build upon
-* An optional `discard` field (default: false) to discard the environment after execution
+* An optional `record` field (default: false) to record the environment after execution
 * Optional fields for additional information:
   * `allTactics`: when true, includes all tactic steps in the response
   * `rootGoals`: when true, includes root goals as sorries
@@ -46,7 +46,7 @@ You can backtrack simply by using earlier values for `env`.
 The response includes:
 * A numeric label for the `Environment` after your command,
   which you can use as the starting point for subsequent commands.
-  This will be `none` if `discard` was enabled.
+  This will be `none` if `record` was enabled.
 * Any messages generated while processing your command.
 * A list of the `sorry`s in your command, including
   * their expected type, and

REPL/JSON.lean

@@ -23,13 +23,13 @@ structure CommandOptions where
 /-- Run Lean commands.
 If `env = none`, starts a new session (in which you can use `import`).
 If `env = some n`, builds on the existing environment `n`.
-Setting `discard = true` will discard the environment after execution, useful for memory management.
-When `discard = true`, the response's `env` field will be `none`.
+Setting `record = false` will discard the environment after execution, useful for memory management.
+When `record = false`, the response's `env` field will be `none`.
 -/
 structure Command extends CommandOptions where
   env : Option Nat
   cmd : String
-  discard : Option Bool := false
+  record : Option Bool := true
 deriving ToJson, FromJson
 
 /-- Process a Lean file in a fresh environment. -/

REPL/Main.lean

@@ -322,11 +322,12 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         fileMap := default,
         snap? := none,
         cancelTk? := none } }
-  let env ← match s.discard with
-  | some true => pure none
-  | _ => do
+  let env ← match s.record with
+  | some true =>
     let id ← recordCommandSnapshot cmdSnapshot
     pure (some id)
+  | _ => do pure none
+
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.flatMap InfoTree.retainTacticInfo

test/Mathlib/test/discardCmd.expected.out

@@ -0,0 +1,10 @@
+{}
+
+{"message": "Unknown environment."}
+
+{"message": "Unknown proof state."}
+
+{"message": "Unknown environment."}
+
+{"message": "Unknown proof state."}
+

test/Mathlib/test/record_cmd.expected.out

@@ -1,6 +1,6 @@
 {"cmd": "import Mathlib"}
 
-{"cmd": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0 := sorry", "env":0, "discard": true}
+{"cmd": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0 := sorry", "env":0, "record": false}
 
 {"tactic": "norm_num", "proofState": 0}
 

test/Mathlib/test/discardCmd.in renamed to test/Mathlib/test/record_cmd.in

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

test/discardCmd.expected.out renamed to test/record_cmd.expected.out

@@ -1,6 +1,6 @@
 {"cmd": "def f := 37"}
 
-{"cmd": "#eval true", "discard": true}
+{"cmd": "#eval true", "record": false}
 
 {"cmd": "#eval false", "env":1}
 

test/discardCmd.in renamed to test/record_cmd.in

@@ -6,15 +6,13 @@
   {"severity": "error",
    "pos": {"line": 1, "column": 18},
    "endPos": {"line": 1, "column": 20},
-   "data": "unsolved goals\n⊢ 2 = 2"}],
- "env": 0}
+   "data": "unsolved goals\n⊢ 2 = 2"}]}
 
 {"messages":
  [{"severity": "info",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 2, "column": 3},
-   "data": "Goals accomplished!"}],
- "env": 1}
+   "data": "Goals accomplished!"}]}
 
 {"messages":
  [{"severity": "error",

test/discardCmd2.expected.out renamed to test/record_cmd2.expected.out

@@ -2,8 +2,8 @@
 
 {"cmd": "example  : 2=2 := by\nrfl"}
 
-{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by", "discard": true}
+{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by", "record": false}
 
-{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p", "discard": true}
+{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p", "record": false}
 
-{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p\napply?", "discard": true}
+{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p\napply?", "record": false}