- missingCommand : CliError
- unknownCommand (cmd : String) : CliError
- missingArg (arg : String) : CliError
- missingOptArg (opt arg : String) : CliError
- invalidOptArg (opt arg : String) : CliError
- unknownShortOption (opt : Char) : CliError
- unknownLongOption (opt : String) : CliError
- unexpectedArguments (args : List String) : CliError
- unexpectedPlus : CliError
- unknownTemplate (spec : String) : CliError
- unknownConfigLang (spec : String) : CliError
- unknownModule (mod : Lean.Name) : CliError
- unknownModulePath (path : System.FilePath) : CliError
- unknownPackage (spec : String) : CliError
- unknownFacet (type : String) (facet : Lean.Name) : CliError
- unknownTarget (target : Lean.Name) : CliError
- missingModule (pkg mod : Lean.Name) : CliError
- missingTarget (pkg : Lean.Name) (spec : String) : CliError
- invalidBuildTarget (key : String) : CliError
- invalidTargetSpec (spec : String) (tooMany : Char) : CliError
- invalidFacet (target facet : Lean.Name) : CliError
- unknownExe (spec : String) : CliError
- unknownScript (script : String) : CliError
- missingScriptDoc (script : String) : CliError
- invalidScriptSpec (spec : String) : CliError
- outputConfigExists
(path : System.FilePath)
: CliError
Translate Errors
- unknownLeanInstall : CliError
- unknownLakeInstall : CliError
- leanRevMismatch (expected actual : String) : CliError
- invalidEnv (msg : String) : CliError
- missingRootDir (path : System.FilePath) : CliError