A Dependently Typed Functional Programming Language
Go to file
Edwin Brady fcfbfaa0b5 Make GMP optional (default off)
This removes the last common obstacle to getting Idris built, at the
expense of using mini-gmp which is supposedly slower (but I haven't yet
measured how much this is likely to affect us).
2013-11-25 17:42:15 +00:00
benchmarks Change from shebangs with absolute references to using /usr/bin/env 2013-11-18 17:10:00 +00:00
contribs remove auto-idris, now that the functionality is supported via ideslave 2013-11-21 20:15:31 +01:00
iif Change TRACE mode to use -O2 2012-09-05 17:24:37 +01:00
jsrts javascript: switch to jsbn 2013-10-12 01:46:58 +02:00
libs Replace some Heap proofs with impossible. 2013-11-24 14:14:42 -05:00
llvm Implement argument access under LLVM codegen 2013-11-13 19:51:00 -08:00
papers/impl-paper Finished proof-reading implementation paper 2013-09-15 17:11:17 +01:00
rts Make GMP optional (default off) 2013-11-25 17:42:15 +00:00
samples Whitespace cleanup. 2013-11-01 14:33:45 +01:00
src Make GMP optional (default off) 2013-11-25 17:42:15 +00:00
support Don't build thread support (because it doesn't work...) 2012-05-10 11:37:46 +01:00
test Improve type class overlap check 2013-11-24 01:17:47 +00:00
tutorial Updated idrislang.sty 2013-11-20 16:18:34 +00:00
.gitattributes typo fix in git attributes, adding test results to gitignore 2012-11-26 21:09:59 -05:00
.gitignore Various 'beneath the hood' improvements made to the tutorial project. 2013-11-12 10:22:02 +00:00
.travis.yml Ask travis to install optional dependencies 2013-10-31 21:33:46 +00:00
CHANGELOG Improve type class overlap check 2013-11-24 01:17:47 +00:00
config.mk * Use cc as C compiler, instead of hardcoding gcc. 2013-11-19 16:14:55 +01:00
CONTRIBUTORS Add ECA to contributors 2013-11-05 14:39:27 -05:00
custom.mk-alldeps Add example of custom.mk for building with both optional dependencies 2013-11-08 07:52:33 +01:00
idris.cabal Make GMP optional (default off) 2013-11-25 17:42:15 +00:00
LICENSE Fix LICENSE 2011-09-14 18:01:24 +01:00
Makefile Moved libraries around, removed 'effects' flag 2013-11-20 17:38:22 +00:00
README Add note about custom.mk example 2013-11-08 08:00:02 +01:00
Setup.hs Make GMP optional (default off) 2013-11-25 17:42:15 +00:00

Idris (http://idris-lang.org/) is an experimental functional programming 
language with dependent types.

To configure, edit config.mk. 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 custom.mk or add the following line to it:
CABALFLAGS += -f LLVM -f FFI
The file custom.mk-alldeps 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 https://github.com/idris-lang/Idris-dev/wiki .