idris - Man Page
manual page for idris 1.3.4-git:PRE
Synopsis
idris [--nobanner | (-q|--quiet) | --ide-mode | --ide-mode-socket |
Description
Idris version 1.3.4-git:PRE , (C) The Idris Community 2016
--client ARG | --log LEVEL | --logging-categories CATS | --nobasepkgs | --noprelude | --nobuiltins | --check | (-o|--output FILE) | --interface | --typeintype | --total | --partial | --warnpartial | --warnreach | --warnipkg | --nocoverage | --errorcontext | --info | --listlogcats | --link | --listlibs | --libdir | --docdir | --include | --V2 | --V1 | (-V|--V0|--verbose) | --ibcsubdir FILE | (-i|--idrispath ARG) | --sourcepath ARG | --warn | (-p|--package ARG) | --port PORT | --build IPKG | --install IPKG | --repl IPKG | --clean IPKG | --mkdoc IPKG | --installdoc IPKG | --checkpkg IPKG | --testpkg IPKG | --indent-with INDENT | --indent-clause INDENT | --bytecode ARG | (-S|--codegenonly) | (-c|--compileonly) | --dumpdefuns ARG | --dumpcases ARG | --codegen TARGET | --portable-codegen TARGET | --cg-opt ARG | (-e|--eval EXPR) | --execute | --exec EXPR | (-X|--extension EXT) | --O3 | --O2 | --O1 | --O0 | --partial-eval | --no-partial-eval | (--optimise-nat-like-types|--optimize-nat-like-types) | (--no-optimise-nat-like-types|--no-optimize-nat-like-types) | (-O|--level ARG) | --target TRIPLE | --cpu CPU | (--color|--colour) | (--nocolor|--nocolour) | --consolewidth WIDTH | --highlight | --no-tactic-deprecation-warnings | --allow-capitalized-pattern-variables] [FILES] [-v|--version]
Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML.
+ Full dependent types with dependent pattern matching + Simple case expressions, where-clauses, with-rule + Pattern matching let- and lambda-bindings + Overloading via Interfaces (Type class-like), Monad comprehensions + do-notation, idiom brackets + Syntactic conveniences for lists, tuples, dependent pairs + Totality checking + Coinductive types + Indentation significant syntax, Extensible syntax + Tactic based theorem proving (influenced by Coq) + Cumulative universes + Simple Foreign Function Interface + Hugs style interactive environment
Available options
- --nobanner
Suppress the banner
- -q,--quiet
Quiet verbosity
- --ide-mode
Run the Idris REPL with machine-readable syntax
- --ide-mode-socket
Choose a socket for IDE mode to listen on
- --log LEVEL
Debugging log level
- --logging-categories CATS
Colon separated logging categories. Use --listlogcats to see list.
- --nobasepkgs
Do not use the given base package
- --noprelude
Do not use the given prelude
- --nobuiltins
Do not use the builtin functions
- --check
Typecheck only, don't start the REPL
- -o,--output FILE
Specify output file
- --interface
Generate interface files from ExportLists
- --typeintype
Turn off Universe checking
- --total
Require functions to be total by default
- --warnpartial
Warn about undeclared partial functions
- --warnreach
Warn about reachable but inaccessible arguments
- --warnipkg
Warn about possible incorrect package specifications
- --info
Display information about installation.
- --listlogcats
Display logging categories
- --link
Display link flags
- --listlibs
Display installed libraries
- --libdir
Display library directory
- --docdir
Display idrisdoc install directory
- --include
Display the includes flags
- --V2
Loudest verbosity
- --V1
Louder verbosity
- -V,--V0,--verbose
Loud verbosity
- --ibcsubdir FILE
Write IBC files into sub directory
- -i,--idrispath ARG
Add directory to the list of import paths
- --sourcepath ARG
Add directory to the list of source search paths
- -p,--package ARG
Add package as a dependency
- --port PORT
REPL TCP port - pass "none" to not bind any port
- --build IPKG
Build package
- --install IPKG
Install package
- --repl IPKG
Launch REPL, only for executables
- --clean IPKG
Clean package
- --mkdoc IPKG
Generate IdrisDoc for package
- --installdoc IPKG
Install IdrisDoc for package
- --checkpkg IPKG
Check package only
- --testpkg IPKG
Run tests for package
- --indent-with INDENT
Indentation to use with :makewith (default 2)
- --indent-clause INDENT
Indentation to use with :addclause (default 2)
- -S,--codegenonly
Do no further compilation of code generator output
- -c,--compileonly
Compile to object files rather than an executable
- --codegen TARGET
Select code generator: C, Javascript, Node and bytecode are bundled with Idris
- --portable-codegen TARGET
Pass the name of the code generator. This option is for codegens that take JSON formatted IR.
- --cg-opt ARG
Arguments to pass to code generator
- -e,--eval EXPR
Evaluate an expression without loading the REPL
- --execute
Execute as idris
- --exec EXPR
Execute as idris
- -X,--extension EXT
Turn on language extension (TypeProviders or ErrorReflection)
- --no-partial-eval
Switch off partial evaluation, mainly for debugging purposes
- --optimise-nat-like-types,--optimize-nat-like-types
Enable compilation of Nat-like types to bigints
- --no-optimise-nat-like-types,--no-optimize-nat-like-types
Disable compilation of Nat-like types to bigints
- --target TRIPLE
If supported the codegen will target the named triple.
- --cpu CPU
If supported the codegen will target the named CPU e.g. corei7 or cortex-m3
- --color,--colour
Force coloured output
- --nocolor,--nocolour
Disable coloured output
- --consolewidth WIDTH
Select console width: auto, infinite, nat
- --highlight
Emit source code highlighting
- --no-tactic-deprecation-warnings
Disable deprecation warnings for the old tactic sublanguage
- --allow-capitalized-pattern-variables
Allow pattern variables to be capitalized
- -v,--version
Print version information
- -h,--help
Show this help text
It is important to note that Idris is first and foremost a research tool and project. Thus the tooling provided and resulting programs created should not necessarily be seen as production ready nor for industrial use.
More details over Idris can be found online here: