New in 0.10:

============

* 'class' and 'instance' are now deprecated keywords. They have been
  replaced by 'interface' and 'implementation' respectively. This is to
  properly reflect their purpose.
* (/) operator moved into new Fractional interface.
* Idris' logging infrastructure has been categorised. Command line and repl
  are available. For command line the option `--logging-categories CATS`
  is used to pass in the categories. Here `CATS` is a colon separated quoted
  string containing the categories to log. The REPL command is `logcats CATS`.
  Where `CATS` is a whitespace separated list of categoriese. Default is for
  all categories to be logged.
* New flag `--listlogcats` to list logging categories.`

0.9.20.2

Patch release for consistency with TypeDD Book

0.9.20.1, Minor patch release

New in 0.9.20:

==============

Language updates
----------------

* Improved unification by implementing a pattern unification rule
* The syntax `{{n}} quotes n without resolving it, allowing short syntax
  for defining new names. `{n} still quotes n to an existing name in scope.
* A new primitive operator prim__strSubstr for more efficient extraction of
  substrings. External code generators should implement this.
* The previous syntax for tactic proofs and the previous interactive prover
  are now deprecated in favour of reflected elaboration. They will be removed
  at some point in the future.
* Changed scoping rules for unbound implicits: any name which would be a
  valid unbound implicit is now *always* an unbound implicit. This is much
  more resilient to changes in inputs, but does require that function names
  be explicitly qualified when in argument position.
* Name binding in patterns follows the same rule as name binding for implicits
  in types: names which begin with lower case letters, not applied to any
  arguments, are treated as bound pattern variables.
* Added %deprecate directive, which gives a warning and a message when a
  deprecated name is referenced.

Library updates
---------------

* The 'Neg' class now represents numeric types which can be negative. As
  such, the (-) operator and 'abs' have been moved there from 'Num'.
* A special version of (-) on 'Nat' requires that the second argument is
  smaller than or equal to the first. 'minus' retains the old behaviour,
  returning Z if there is an underflow.
* The (+), (-), and (*) operations on Fin have been removed.
* New Logging Effects have been added to facilitate logging of effectful
  programmes.
* Elaborator reflection is now a part of the prelude. It is no longer
  necessary to import Language.Reflection.Elab.
* The `PERF` effect allows for simple performance metrics to be collected
  from Effectful programs.
* Some constructors that never actually occurred have been removed from
  the TT and Raw reflection datatypes in Language.Reflection.
* File IO operations (for example openFile/fread/fwrite) now return
  'Either FileError ty' where the return type was previously 'ty' to indicate
  that they may fail.

Tool updates
------------
* Records are now shown as records in :doc, rather than as the underlying
  datatype
* iPKG files have a new option `pkgs` which takes a comma-separated list
  of package names that the idris project depends on. This reduces bloat
  in the `opts` option with multiple package declarations.
* iPKG files now allow `executable = "your filename here"` in addition to
  the existing `executable = yourFilenameHere` style. While the unquoted
  version is limited to filenames that look like namespaced Idris identifiers
  (`your.filename.here`), the quoted version accepts any valid filename.
* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now
  adds missing clauses if there is already a definition.

Miscellaneous updates
---------------------
* Disable the deprecation warnings for %elim and old-style tactic scripts
  with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings
  flags.

0.9.19.1 patch release

Changes so far
==============

Language updates
----------------

* Improved unification by implementing a pattern unification rule
* The syntax `{{n}} quotes n without resolving it, allowing short syntax
  for defining new names. `{n} still quotes n to an existing name in scope.
* A new primitive operator prim__strSubstr for more efficient extraction of
  substrings. External code generators should implement this.
* Changed scoping rules for unbound implicits: any name which would be a
  valid unbound implicit is now *always* an unbound implicit. This is much
  more resilient to changes in inputs, but does require that function names
  be explicitly qualified when in argument position.

Library updates
---------------

* The 'Neg' class now represents numeric types which can be negative. As
such, the (-) operator and 'abs' have been moved there from 'Num'.
* A special version of (-) on 'Nat' requires that the second argument is
smaller than or equal to the first. 'minus' retains the old behaviour,
returning Z if there is an underflow.
* New Logging Effects have been added to facilitate logging of effectful
  programmes.

Tool updates
------------
* Records are now shown as records in :doc, rather than as the underlying
  datatype

New in 0.9.19:

--------------
* The Idris Reference manual has been fleshed out with content originally found
  on the GitHub wiki.
* The Show class has been moved into Prelude.Show and augmented with the method
  showPrec, which allows correct parenthesization of showed terms. This comes
  with the type Prec of precedences and a few helper functions.
* New REPL command :printerdepth that sets the pretty-printer to only descend to
  some particular depth when printing. The default is set to a high number to
  make it less dangerous to experiment with infinite structures. Infinite depth
  can be set by calling :printerdepth with no argument.
* Compiler output shows applications of >>= in do-notation
* fromInteger i where i is an integer constant is now shown just as i in
  compiler output
* An interactive shell, similar to the prover, for running reflected elaborator
  actions. Access it with :elab from the REPL.
* New command-line option --highlight that causes Idris to save highlighting
  information when successfully type checking. The information is in the same
  format sent by the IDE mode, and is saved in a file with the extension ".idh".
* Highlighting information is saved by the parser as well, allowing it to highlight
  keywords like "case", "of", "let", and "do"
* Use predicates instead of boolean equality proofs as preconditions
  on List functions
* More flexible 'case' construct, allowing each branch to target different
  types, provided that the case analysis does not affect the form of any
  variable used in the right hand side of the case.
* Some improvements in interactive editing, particularly in lifting out
  definitions and proof search.
* Moved System.Interactive, along with getArgs to the Prelude.
* Major improvements to reflected elaboration scripts, including the ability to run
  them in a declaration context and many bug fixes.
* "decl syntax" rules to allow syntax extensions at the declaration level
* Experimental Windows support for console colours

0.9.18.1 for fixing hackage dependencies

Version 0.9.18 change log:

* GHC 7.10 compatibility
* Add support for bundled toolchains.
* Strings are now UTF8 encoded in the default back end
* Idris source files are now assumed to be in UTF8, regardless of locale
  settings.
* Some reorganisation of primitives:
  + Buffer and BitVector primitives have been removed (they were not
    tested sufficiently, and lack a maintainer)
  + Float has been renamed 'Double' (Float is defined in the Prelude for
    compatibility)
  + Externally defined primitives and  operations now supported with
    '%extern' directive, allowing back ends to define their own special
    purpose primitives
  + Ptr and ManagedPtr have been removed and replaced with external primitives
* Add %hint function annotation, which allows functions to be used as
  hints in proof search for 'auto' arguments. Only functions which return
  an instance of a data or record type are allowed as hints.
* Syntax rules no longer perform variable capture. Users of effects will
  need to explicitly name results in dependent effect signatures instead
  of using the default name "result".
* Pattern-matching lambdas are allowed to be impossible. For example,
  Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
  requiring a separate lemma.
* Case alternatives are allowed to be impossible:
  case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
* The default Semigroup and Monoid instances for Maybe are now prioritised
  choice, keeping the first success as Alternative does. The version that
  collects successes is now a named instance.
* :exec REPL command now takes an optional expression to compile and run/show
* The return types of `Vect.findIndex`, `Vect.elemIndex` and
  `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`
* A new :browse command shows the contents of a namespace
* `{n} is syntax for a quotation of the reflected representation of the name
  "n". If "n" is lexically bound, then the resulting quotation will be for it,
  whereas if it is not, then it will succeed with a quotation of the unique
  global name that matches.
* New syntax for records that closely matches our other record-like structures:
  type classes. See the updated tutorial for details.
* Records can be coinductive. Define coinductive records with the "corecord"
  keyword.
* Type class constructors can be assigned user-accessible names. This is done
  using the same syntax as record constructors.
* if ... then ... else ... is now built-in syntax instead of being defined in
  a library. It is shown in REPL output and error messages, rather than its
  desugaring.
* The desugaring of if ... then ... else ... has been renamed to ifThenElse from
  boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
  to reflect that if-notation makes sense with non-Bool datatypes.
* Agda-style semantic highlighting is supported over the IDE protocol.
* Experimental support for elaborator reflection. Users can now script the
  elaborator, for use in code generation and proof automation. This feature is
  still under rapid development and is subject to change without notice. See
  Language.Reflection.Elab and the %runElab constructs

Fix interactive proof mode

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.