message: configuration: do not use strings for limits
diff: },
  "lean.memoryLimit": {
  "type": "number",
  - "default": "4096",
  + "default": 4096,
  "description": "Set a memory limit (in Megabytes) for the Lean server."
  },
  "lean.timeLimit": {
  "type": "number",
  - "default": "100000",
  + "default": 100000,
  "description": "Set a Deterministic timeout (it is approximately the maximum number of memory allocations in thousands) for the Lean server."
  },
  "lean.extraOptions": {
  