Idris.CommandLine

Definitions

data PkgCommand : Type

Totality: total
Visibility: public export
Constructors:

Build : PkgCommand

Install : PkgCommand

InstallWithSrc : PkgCommand

MkDoc : PkgCommand

Typecheck : PkgCommand

Clean : PkgCommand

REPL : PkgCommand

Init : PkgCommand

DumpJson : PkgCommand

DumpInstallDir : PkgCommand

Hint: 

Show PkgCommand

data DirCommand : Type

Totality: total
Visibility: public export
Constructors:

LibDir : DirCommand

Prefix : DirCommand

  Show the installation prefix

BlodwenPaths : DirCommand

Hint: 

Show DirCommand

data HelpTopic : Type

  Help topics

Totality: total
Visibility: public export
Constructors:

HelpLogging : HelpTopic

  Interactive debugging topics

HelpPragma : HelpTopic

  The various pragmas

data CLOpt : Type

  CLOpt - possible command line options

Totality: total
Visibility: public export
Constructors:

CheckOnly : CLOpt

  Only typecheck the given file

OutputFile : String -> CLOpt

  The output file from the code generator

ExecFn : String -> CLOpt

  Execute a given function after checking the source file

SetCG : String -> CLOpt

  Use a specific code generator

Directive : String -> CLOpt

  Pass a directive to the code generator

NoPrelude : CLOpt

  Don't implicitly import Prelude

SourceDir : String -> CLOpt

  Set source directory

BuildDir : String -> CLOpt

  Set build directory

OutputDir : String -> CLOpt

  Set output directory

Profile : CLOpt

  Generate profile data when compiling (backend dependent)

Version : CLOpt

  Display Idris version

TTCVersion : CLOpt

  Display the TTC version currently used

Help : Maybe HelpTopic -> CLOpt

  Display help text

NoBanner : CLOpt

  Suppress the banner

Quiet : CLOpt

  Run Idris 2 in quiet mode

ShowImplicits : CLOpt

  Show implicits when pretty printing

ShowMachineNames : CLOpt

  Show machine names when pretty printing

ShowNamespaces : CLOpt

  Show namespaces when pretty printing

Verbose : CLOpt

  Run Idris 2 in verbose mode (cancels quiet if it's the default)

ConsoleWidth : Maybe Nat -> CLOpt

  Set the console width for REPL output

Color : Bool -> CLOpt

  Whether to use color in the console output

Logging : LogLevel -> CLOpt

  Set the log level globally

PkgPath : String -> CLOpt

  Add a package as a dependency

ListPackages : CLOpt

  List installed packages

Package : PkgCommand -> Maybe String -> CLOpt

  Build or install a given package, depending on PkgCommand

Directory : DirCommand -> CLOpt

  Show locations of data/library directories

InputFile : String -> CLOpt

  The input Idris file

IdeMode : CLOpt

  Whether or not to run in IdeMode (easily parsable for other tools)

IdeModeSocket : String -> CLOpt

  Whether or not to run IdeMode (using a socket instead of stdin/stdout)

Yaffle : String -> CLOpt

  Run as a checker for the core language TTImp

Metadata : String -> CLOpt

  Dump metadata from a .ttm file

DumpCases : String -> CLOpt

  Dump cases before compiling

DumpLifted : String -> CLOpt

  Dump lambda lifted defs before compiling

DumpANF : String -> CLOpt

  Dump ANF defs before compiling

DumpVMCode : String -> CLOpt

  Dump VM code defs before compiling

RunREPL : String -> CLOpt

  Run a REPL command then exit immediately

IgnoreMissingIPKG : CLOpt

FindIPKG : CLOpt

Timing : Maybe Nat -> CLOpt

DebugElabCheck : CLOpt

AltErrorCount : Nat -> CLOpt

WarningsAsErrors : CLOpt

  Treat warnings as errors

IgnoreShadowingWarnings : CLOpt

  Do not print shadowing warnings

HashesInsteadOfModTime : CLOpt

  Use SHA256 hashes to determine if a source file needs rebuilding instead
  of modification time.

CaseTreeHeuristics : CLOpt

  Apply experimental heuristics to case tree generation that
  sometimes improves performance and reduces compiled code
  size.

IncrementalCG : String -> CLOpt

  Use incremental code generation, if the backend supports it

WholeProgram : CLOpt

  Use whole program compilation - overrides IncrementalCG if set

BashCompletion : String -> String -> CLOpt

  Generate bash completion info

BashCompletionScript : String -> CLOpt

  Generate bash completion script

ZshCompletionScript : String -> CLOpt

  Generate zsh completion script

Total : CLOpt

  Turn on %default total globally

NoCSE : CLOpt

  Disable common subexpression elimination

ideSocketModeAddress : List CLOpt -> (String, Int)

  Extract the host and port to bind the IDE socket to

Totality: total
Visibility: export

versionMsg : String

Totality: total
Visibility: export

usage : String

Totality: total
Visibility: export

getOpts : List String -> Either String (List CLOpt)

Totality: total
Visibility: export

getCmdOpts : IO (Either String (List CLOpt))

Visibility: export

findNearMatchOpt : String -> Maybe String

  Find an opt that would have matched if only the user had prefixed it with
  double-dashes. It is common to see the user error of specifying a command
  like "idris2 repl ..." when they mean to write "idris2 --repl ..."

Totality: total
Visibility: export

nearMatchOptSuggestion : String -> Maybe (Doc IdrisAnn)

  Suggest an opt that would have matched if only the user had prefixed it with
  double-dashes. It is common to see the user error of specifying a command
  like "idris2 repl ..." when they mean to write "idris2 --repl ..."

Totality: total
Visibility: export

optionFlags : List String

  List of all command line option flags.

Totality: total
Visibility: export