feat: #version command (leanprover#5768)

Prints `Lean.versionString` and target/platform information. Example:
```
Lean 4.12.0, commit 8218940
Target: arm64-apple-darwin23.5.0 macOS
```

src/Lean/Elab/BuiltinCommand.lean

@@ -12,6 +12,7 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
+import Init.System.Platform
 
 namespace Lean.Elab.Command
 
@@ -404,6 +405,16 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       includedVars := sc.includedVars.filter (!omittedVars.contains ·) }
   | _ => throwUnsupportedSyntax
 
+@[builtin_command_elab version] def elabVersion : CommandElab := fun _ => do
+  let mut target := System.Platform.target
+  if target.isEmpty then target := "unknown"
+  -- Only one should be set, but good to know if multiple are set in error.
+  let platforms :=
+    (if System.Platform.isWindows then [" Windows"] else [])
+    ++ (if System.Platform.isOSX then [" macOS"] else [])
+    ++ (if System.Platform.isEmscripten then [" Emscripten"] else [])
+  logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
+
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
   logWarning "using 'exit' to interrupt Lean"
 

src/Lean/Parser/Command.lean

@@ -505,6 +505,9 @@ Displays all available tactic tags, with documentation.
 -/
 @[builtin_command_parser] def printTacTags   := leading_parser
   "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
+/-- Shows the current Lean version. Prints `Lean.versionString`. -/
+@[builtin_command_parser] def version        := leading_parser
+  "#version"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit