feat: lake: provide help on Elan's + option (#7024)

This PR documents how to use Elan's `+` option with `lake new|init`. It
also provides an more informative error message if a `+` option leaks
into Lake (e.g., if a user provides the option to a Lake run without
Elan).

src/lake/Lake/CLI/Error.lean

@@ -20,6 +20,7 @@ inductive CliError
 | unknownShortOption (opt : Char)
 | unknownLongOption (opt : String)
 | unexpectedArguments (args : List String)
+| unexpectedPlus
 /- Init CLI Errors -/
 | unknownTemplate (spec : String)
 | unknownConfigLang (spec : String)
@@ -59,6 +60,9 @@ def toString : CliError → String
 | unknownShortOption opt  => s!"unknown short option '-{opt}'"
 | unknownLongOption opt   => s!"unknown long option '{opt}'"
 | unexpectedArguments as  => s!"unexpected arguments: {" ".intercalate as}"
+| unexpectedPlus          =>
+  s!"the `+` option is an Elan feature; \
+    rerun Lake via Elan and ensure this option comes first."
 | unknownTemplate spec    => s!"unknown package template `{spec}`"
 | unknownConfigLang spec  => s!"unknown configuration language `{spec}`"
 | unknownModule mod       => s!"unknown module `{mod.toString false}`"

src/lake/Lake/CLI/Help.lean

@@ -71,8 +71,11 @@ OUTPUT OPTIONS:
 
 See `lake help <command>` for more information on a specific command."
 
-def templateHelp :=
-s!"The initial configuration and starter files are based on the template:
+def newInitHelp :=
+s!"If you are using Lake through Elan (which is standard), you can create a
+package with a specific Lean version via the `+` option.
+
+The initial configuration and starter files are based on the template:
 
   std                   library and executable; default
   exe                   executable only
@@ -80,23 +83,23 @@ s!"The initial configuration and starter files are based on the template:
   math                  library only with a mathlib dependency
 
 Templates can be suffixed with `.lean` or `.toml` to produce a Lean or TOML
-version of the configuration file, respectively. The default is Lean."
+version of the configuration file, respectively. The default is TOML."
 
 def helpNew :=
 s!"Create a Lean package in a new directory
 
 USAGE:
-  lake new <name> [<template>][.<language>]
+  lake [+<lean-version>] new <name> [<template>][.<language>]
 
-{templateHelp}"
+{newInitHelp}"
 
 def helpInit :=
 s!"Create a Lean package in the current directory
 
 USAGE:
-  lake init [<name>] [<template>][.<language>]
+  lake [+<lean-version>] init [<name>] [<template>][.<language>]
 
-{templateHelp}
+{newInitHelp}
 
 You can create a package with current directory's name via `lake init .`
 or a bare `lake init`."

src/lake/Lake/CLI/Main.lean

@@ -642,7 +642,11 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "version-tags"        => lake.versionTags
 | "self-check"          => lake.selfCheck
 | "help"                => lake.help
-| cmd                   => throw <| CliError.unknownCommand cmd
+| cmd                   =>
+  if cmd.startsWith "+" then
+    throw <| CliError.unexpectedPlus
+  else
+    throw <| CliError.unknownCommand cmd
 
 def lake : CliM PUnit := do
   match (← getArgs) with