New in 0.9.17:

--------------
* The --ideslave command line option has been replaced with a --ide-mode
  command line option with the same semantics.
* A new tactic "claim N TY" that introduces a new hole named N with type TY
* A new tactic "unfocus" that moves the current hole to the bottom of the
  hole stack
* Quasiquotation supports the generation of Language.Reflection.Raw terms
  in addition to Language.Reflection.TT. Types are used for disambiguation,
  defaulting to TT at the REPL.
* Language.Reflection.Quotable now takes an extra type parameter which
  determines the type to be quoted to. Instances are provided to quote
  common types to both TT and Raw.
* Library operators have been renamed for consistency with Haskell. In
  particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
  now an alias for Functor.map. Correspondingly, ($>) and (<$) have
  been renamed to (<*) and (*>). The cascading effects of this rename
  are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
  Matrix.(<.>) is now Matrix.(<:>).
* Binding forms in DSL notation are now given an extra argument: a
  reflected representation of the name that the user chose.
  Specifically, the rewritten lambda, pi, and let binders will now get
  an extra argument of type TTName. This allows more understandable
  dynamic errors in DSL code and more readable code generation results.
* DSL notation can now be applied with $
* Added FFI_Export type which allows Idris functions to be exportoed and
  called from foreign code
* Instances can now have documentation strings.
* Type providers can have documentation strings.
* Unification errors now (where possible) contain information about provenance
  of a type
* New REPL command ":core TM" that shows the elaborated form of TM along with
  its elaborated type using the syntax of TT. IDE mode has a corresponding
  command :elaborate-term for serialized terms.
* Effectful and IO function names for sending data to STDOUT have been
  aligned, semantically.
    + `print` is now for putting showable things to STDOUT.
    + `printLn` is for putting showable things to STDOUT with a new line
    + `putCharLn` for putting a single character to STDOUT, with a new line.
* Classes can now be annotated with 'determining parameters' to say which
  must be available before resolving instances. Only determining parameters
  are checked when checking for overlapping instances.
* New package 'contrib' containing things that are less mature or less used
  than the contents of 'base'. 'contrib' is not available by default, so you
  may need to add '-p contrib' to your .ipkg file or Idris command line.
* Arguments to class instances are now checked for injectivity.
  Unification assumes this, so we need to check when instances are defined.

Version 0.9.16

* Inductive-inductive definitions are now supported (i.e. simultaneously
  defined types where one is indexed by the other.)
* Implicits and type class constraints can now appear in scopes other than
  the top level.
* Importing a module no longer means it is automatically reexported. A new
  "public" modifier has been added to import statements, which will reexport
  the names exported from that module.
* Implemented @-patterns. A pattern of the form x@p on the left hand side
  matches p, with x in scope on the right hand side with value p.
* A new tactic sourceLocation that fills the current hole with the current
  source code span, if this information is available. If not, it raises an
  error.
* Better Unicode support for the JavaScript/Node codegen
* ':search' and ':apropos' commands can now be given optional package lists
  to search.
* Vect, Fin and So moved out of prelude into base, in modules Data.Vect,
  Data.Fin and Data.So respectively.
* Several long-standing issues resolved, particularly with pattern matching
  and coverage checking.
* Modules can now have API documentation strings.

Version 0.9.15.1

Includes important fix for partial evaluation problem in 0.9.15

Version 0.9.15 released

* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
  as an argument and produces it as an error.
* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
  of ErrorReportParts as an argument, like error handlers produce, allowing
  access to the pretty-printer.
* Stop showing irrelevant and inaccessible internal names in the interactive
  prover.
* The proof arguments in the List library functions are now implicit and
  solved automatically.
* More efficient representation of proof state, leading to faster elaboration
  of large expressions.
* EXPERIMENTAL Implementation of uniqueness types
* Unary negation now desugars to "negate", which is a method of the Neg type class.
  This allows instances of Num that can't be negative, like Nat, and it makes correct
  IEEE Float operations easier to encode. Additionally, unary negation is now available
  to DSL authors.
* The Java and LLVM backends have been factored out for separate maintenance. Now, the
  compiler distribution only ships with the C and JavaScript backends.
* New REPL command :printdef displays the internal definition of a name
* New REPL command :pprint pretty-prints a definition or term with LaTeX or
  HTML highlighting
* Naming of data and type constructors is made consistent across the standard
  library (see idris-lang#1516)
* Terms in `code blocks` inside of documentation strings are now parsed and
  type checked. If this succeeds, they are rendered in full color in
  documentation lookups, and with semantic highlighting for IDEs.
* Fenced code blocks in docs defined with the "example" attribute are rendered
  as code examples.
* Fenced code blocks declared to be Idris code that fail to parse or type check now
  provide error messages to IDE clients.
* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
  Engine style)

0.9.14.2

Released for the CUFP 2014 Idris tutorial

0.9.14.1 - fix for dependency issues

New in 0.9.14:

--------------
* Tactic for case analysis in proofs
* Induction and case tactic now work on expressions
* Support for running tests for a package with the tests section of .ipkg files and the
  --testpkg command-line option
* Clearly distinguish between type providers and postulate providers at the use site
* Allow dependent function syntax to be overridden in dsl blocks, similarly to
  functions and let. The keyword for this is "pi".
* Updated 'effects' library, with simplified API
* All new JavaScript backend (avoids callstack overflows)
* Add support for %lib directive for NodeJS
* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
  `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
  version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
  terms to splice in, while on the LHS they are patterns.
  A quasiquote expression can be given a goal type for the elaborator, which helps with
  disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)
  quotes the unit type.
  Both goal types and quasiquote are typechecked in the global environment.
* Better inference of unbound implicits

Version 0.9.13.1

Bugfix release fixing some minor problems in 0.9.13

Release 0.9.13

New in 0.9.13:
--------------
* IDE support for retrieving structured information about metavariables
* Experimental Bits support for JavaScript
* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
* Command line option -e (or --eval) to evaluate expressions without loading the
  REPL. This is useful for writing more portable tests.
* Many more of the basic functions and datatypes are documented.
* Primitive types such as Int and String are documented
* Removed javascript lib in favor of idris-hackers/iQuery
* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
* Remove :info REPL command, subsume and enhance its functionality in the :doc command
* New (first class) nested record update/access syntax:
  record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
  record { a->b->c } x -- accesses field, equivalent to c (b (a x))
* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
* :apropos now accepts space-delimited lists of query items, and searches for the conjunction
  of its inputs. It also accepts binder syntax as search strings - for instance, -> finds
  functions.
* Totality errors are now treated as warnings until code generation time, when they become
  errors again. This allows users to use the interactive editing features to fix totality
  issues, but no programs that violate the stated assumptions will actually run.
* Added :makelemma command, which adds a new top level definition to solve
  a metavariable.
* Extend :addclause to add instance bodies as well as definitions
* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
* Move foldl into Foldable so it can be overridden.
* Experimental :search REPL command for finding functions by type

Internal changes

* New implementation of erasure

New in 0.9.12:

--------------

* Proof search now works for metavariables in types, giving some interactive
  type inference.
* New 'Lazy' type, replacing laziness annotations.
* JavaScript and Node codegen now understand the %include directive.
* Concept of 'null' is now understood in the JavaScript and Node codegen.
* Lots of performance patches for generated JavaScript.
* New commands :eval (:e) and :type (:t) in the prover, which either normalise
  or show the type of expressions.
* Allow type providers to return postulates in addition to terms.
* Syntax for dealing with match failure in <- and pattern matching let.
* New syntax for inline documentation. Documentation starts with |||, and
  arguments are documented by preceding their name with @. Example:
  ||| Add two natural numbers
  ||| @ n the first number (examined by the function)
  ||| @ m the second number (not examined)
  plus (n, m : Nat) -> Nat
* Allow the auto-solve behaviour in the prover to be disabled, for easier
  debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
* Updated 'effects' library
* New :apropos command at REPL to search documentation, names, and types
* Unification errors are now slightly more informative
* Support mixed induction/coinduction with 'Inf' type
* Add 'covering' function option, which checks whether a function and all
  descendants cover all possible inputs