update readme

Author: RexWzh

README.md

@@ -20,6 +20,19 @@ Commands may be of the form
 { "cmd" : "example : f = 2 := rfl", "env" : 1 }
 ```
 
+```json
+{ "cmd" : "example : f = 2 := rfl", "env" : 1, "gc": 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
+* Optional fields for additional information:
+  * `allTactics`: when true, includes all tactic steps in the response
+  * `rootGoals`: when true, includes root goals as sorries
+  * `infotree`: specifies the level of info tree detail ("full", "tactics", "original", or "substantive")
+
 The `env` field, if present,
 must contain a number received in the `env` field of a previous response,
 and causes the command to be run in the existing environment.

REPL/JSON.lean

@@ -23,6 +23,8 @@ 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`.
 -/
 structure Command extends CommandOptions where
   env : Option Nat