A Dependently Typed Functional Programming Language
Haskell Idris C JavaScript Shell TeX Other
Pull request Compare This branch is 3401 commits behind idris-lang:master.
Latest commit 853c9c5 Dec 12, 2014 @david-christiansen david-christiansen Merge pull request #1783 from jfdm/contrib/updates
Updates to idrislang.sty
Failed to load latest commit information.
codegen javascript: lift out node backend Aug 22, 2014
contribs Several updates to idrislang.sty Dec 10, 2014
iif Change TRACE mode to use -O2 Sep 5, 2012
jsrts javascript: fix for #1580 Oct 4, 2014
libs Move Pair/Sigma into Builtins namespace Dec 9, 2014
main Call gcc using rawSystem Nov 5, 2014
man Fix typo in help message (language extension) Sep 12, 2014
samples Finished making standard library naming consistent Sep 26, 2014
test Move Pair/Sigma into Builtins namespace Dec 9, 2014
.gitattributes typo fix in git attributes, adding test results to gitignore Nov 27, 2012
.gitignore Merge pull request #1704 from eamsden/master Nov 28, 2014
.travis.yml Don't build Idris twice in CI Nov 28, 2014
CHANGELOG Support for inductive-inductive types Dec 10, 2014
CONTRIBUTING.md Updated contributed.md. Oct 15, 2014
LICENSE Fix LICENSE Sep 14, 2011
Makefile Fixed makefile spacing issues Jun 12, 2014
README.md Fix a few typos in the README Nov 30, 2014
Setup.hs Factor out LLVM backend Sep 19, 2014
config.mk Add -DIDRIS_ENABLE_STATS to CodegenC. Add missing #ifdef IDRIS_ENABLE… Sep 26, 2014
custom.mk-alldeps Automatically detect console width Feb 2, 2014
idris-tutorial.pdf Tutorial changes. Nov 28, 2013
mkpkg.sh Update version number to 0.9.11 Feb 4, 2014



Build Status Hackage

Idris (http://idris-lang.org/) is a general-purpose 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 an optional buildtime dependency on the C library libffi. If you would like to use the features that it enables, make sure that it is compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc). By default, Idris builds without it. To build with it, pass the flag -f FFI.

To build with libffi by default, create custom.mk or add the following line to it: CABALFLAGS += -f FFI The file custom.mk-alldeps is a suitable example.

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.

Idris has support for external code generators. Supplied with the distribution is a C code generator to compile executables, and a JavaScript code generator with support for node.js and browser JavaScript.

At the point of this writing, there are external repositories with a Java code generator and an LLVM-based code generator which can be found at https://github.com/idris-hackers/idris-java and https://github.com/idris-hackers/idris-llvm respectively.