Tags: jgreene/Idris-dev
Tags
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
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
Changes since previous version ------------------------------ * Agda-style equational reasoning (in Syntax.PreorderReasoning) * 'case' construct now abstracts over the scrutinee in its type * Added label type 'name (equivalent to the empty type). This is intended for field/effect disambiguation. "name" can be any valid identifier. Two labels are definitionally equal if they have the same name. * General improvements in error messages, especially %error_reverse annotation, which allows a hint as to how to display a term in error messages * --ideslave mode now transmits semantic information about many of the strings that it emits, which can be used by clients to implement semantic highlighting like that of the REPL. This has been implemented in the Emacs mode and the IRC bot, which can serve as examples. * New expression form: with NAME EXPR privileges the namespace NAME when disambiguating overloaded names. For example, it is possible to write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]", because the Vect constructors are defined in a namespace called Vect. * assert_smaller internal function, which marks an expression as smaller than a pattern for use in totality checking. e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be structurally smaller than "(x :: xs)" * assert_total internal function, which marks a subexpression as assumed to be total, e.g "assert_total (tail (x :: xs))". * Terminal width is automatically detected if Idris is compiled with curses support. If curses is not available, automatic mode assumes 80 columns. * Changed argument order for Prelude.Either.either. * Experimental 'neweffects' library, intended to replace 'effects' in the next release. Internal changes * Faster elaboration * Smaller .ibc files * Pretty-printer now used for all term output
Hackage release 0.9.10 Changes since previous release: * Type classes now implemented as dependent records, meaning that method types may now depend on earlier methods. * More flexible class instance resolution, so that function types and lambda expressions can be made instances of a type class. * Add !expr notation for implicit binding of intermediate results in monadic/do/etc expressions. * Extend Effects package to cope with possibly failing operations, using "if_valid", "if_error", etc. * At the REPL, "it" now refers to the previous expression. * Semantic colouring at the REPL. Turn this off with --nocolour. * Some prettifying of error messages. * The contents of ~/.idris/repl/init are run at REPL start-up. * The REPL stores a command history in ~/.idris/repl/history. * The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality checker and can thus be used in types. The [x..] syntax now returns an actually infinite stream. * Add '%reflection' option for functions, for compile-time operations on syntax. * Add expression form 'quoteGoal x by p in e' which applies p to the expected expression type and binds the result to x in the scope e. * Performance improvements in Strings library. * Library reorganisation, separated into prelude/ and base/. Internal changes * New module/dependency tree checking. * New parser implementation with more precise errors. * Improved type class resolution. * Compiling Nat via GMP integers. * Performance improvements in elaboration. * Improvements in termination checking. * Various REPL commands to support interactive editing, and a client/server mode to allow external invocation of REPL commands.