Idris 1.0 Released

Idris version 1.0 has been released. You can find it on hackage or from the download page. Documentation is available from

Thanks to everyone who has contributed, whether by providing code, documentation, testing, issue reports, or encouragement. You can find the names of the contributors in the source repository.

What do we mean by “1.0”?

Idris version 1.0 corresponds to the language as described in Type-Driven Development with Idris, published last week by Manning.

As described here, there is still much to do. Idris is primarily a research tool, arising from research into software development with dependent types which aims to make theorem proving and software verification accessible and practical for software developers in general. In calling this “1.0”, we mean no more than that the core language and base libraries are stable, and that you can expect any code that compiles with version 1.0 to compile with any version 1.x.

Since Idris has less than one person working on it full time, we don’t promise “production readiness”, in that there is still a lot to do to make the compiler and run time efficient, and there may be libraries you need which are not available. And, there will certainly be bugs! Please let us know via the issue tracker if you encounter any problems.


We will always welcome contributions, however small. Some specific contributions needed are described on the wiki.

Have fun!


You can get in touch in several ways:

Mailing list
Long-form discussion happens on the mailing list.
There is also an irc channel #idris on freenode. Point your irc client to then /join #idris. Alternatively, there is a web interface.
@idrislang on Twitter
The Idris source is available from our repository. Tools and code by the wider Idris community are available in a GitHub organisation.

All participants in these forums are requested to abide by the community standards.