rename to discardCmd

Author: RexWzh

README.md

@@ -21,13 +21,13 @@ Commands may be of the form
 ```
 
 ```json
-{ "cmd" : "example : f = 2 := rfl", "env" : 1, "gc": true }
+{ "cmd" : "example : f = 2 := rfl", "env" : 1, "discardCmd": 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 `gc` field (default: false) to discard the environment after execution
+* An optional `discardCmd` field (default: false) to discard 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 `gc` was enabled.
+  This will be `none` if `discardCmd` 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 `gc = true` will discard the environment after execution, useful for memory management.
-When `gc = true`, the response's `env` field will be `none`.
+Setting `discardCmd = true` will discard the environment after execution, useful for memory management.
+When `discardCmd = true`, the response's `env` field will be `none`.
 -/
 structure Command extends CommandOptions where
   env : Option Nat
   cmd : String
-  gc : Option Bool := false
+  discardCmd : Option Bool := false
 deriving ToJson, FromJson
 
 /-- Process a Lean file in a fresh environment. -/

REPL/Main.lean

@@ -322,7 +322,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         fileMap := default,
         snap? := none,
         cancelTk? := none } }
-  let env ← match s.gc with
+  let env ← match s.discardCmd with
   | some true => pure none
   | _ => do
     let id ← recordCommandSnapshot cmdSnapshot