Skip to content


Subversion checkout URL

You can clone with
Download ZIP
A Dependently Typed Functional Programming Language
Haskell TeX Idris C JavaScript C++ Other
Branch: master
Pull request Compare This branch is 2 commits ahead, 3979 commits behind idris-lang:master.
Failed to load latest commit information.
benchmarks Change from shebangs with absolute references to using /usr/bin/env
contribs Fix SimpleParser ambiguous type error
examples Tutorial changes.
iif Change TRACE mode to use -O2
jsrts javascript: switch to jsbn
libs Add Eq instance for Either
llvm Implement argument access under LLVM codegen
main Change idris.cabal so library only builds once
papers/impl-paper Finished proof-reading implementation paper
rts Fix typo in Concurrency.Raw
samples Whitespace cleanup.
src generates SError
support Don't build thread support (because it doesn't work...)
test Make note of unapplied unifiation solutions
.gitattributes typo fix in git attributes, adding test results to gitignore
.gitignore Fix source locations for generated version number
.travis.yml (Temporarily) Remove haddock tests from travis
CHANGELOG Make note of unapplied unifiation solutions Add campsite rule to
CONTRIBUTORS Add ECA to contributors
Makefile Add a test_c target for testing C back end only
README Add note about example
Setup.hs Add DragonFly to * Use cc as C compiler, instead of hardcoding gcc. Add example of for building with both optional dependencies
idris-tutorial.pdf Tutorial changes.
idris.cabal Addition of COBOL. Can now pass argument to call the cobol codegen


Idris ( is an experimental functional programming 
language with dependent types.

To configure, edit The default values should work for most people.

To install, type 'make'. This will install everything using cabal and
typecheck the libraries.

To run the tests, type 'make test' which will execute the test suite, and
'make relib', which will typecheck and recompile the standard library.

Idris has optional buildtime dependencies on the C libraries llvm-3.3 and libffi. If you would like to use the features that these enable, be sure these are compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc). By default, Idris builds without them. To build with them, pass the flags -f LLVM and -f FFI, respectively.

To build with LLVM and libffi by default, create or add the following line to it:
The file is a suitable example.

Idris has a runtime dependency on libgmp, and on Boehm GC (libgc) when using the LLVM codegen. These are needed for linking into compiled programs, so be sure these are compiled for Idris's default target architecture (usually 64 bit on x86_64 systems).

The Idris wiki contains instructions for building on various platforms and for getting involved with development. It is located at .
Something went wrong with that request. Please try again.