3* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
4 as an argument and produces it as an error.
5* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
6 of ErrorReportParts as an argument, like error handlers produce, allowing
7 access to the pretty-printer.
8* Stop showing irrelevant and inaccessible internal names in the interactive
10* The proof arguments in the List library functions are now implicit and
12* More efficient representation of proof state, leading to faster elaboration
14* EXPERIMENTAL Implementation of uniqueness types
15* Unary negation now desugars to "negate", which is a method of the Neg type class.
16 This allows instances of Num that can't be negative, like Nat, and it makes correct
17 IEEE Float operations easier to encode. Additionally, unary negation is now available
19* The Java and LLVM backends have been factored out for separate maintenance. Now, the
20 compiler distribution only ships with the C and JavaScript backends.
21* New REPL command :printdef displays the internal definition of a name
22* New REPL command :pprint pretty-prints a definition or term with LaTeX or
24* Naming of data and type constructors is made consistent across the standard
26* Terms in `code blocks` inside of documentation strings are now parsed and
27 type checked. If this succeeds, they are rendered in full color in
28 documentation lookups, and with semantic highlighting for IDEs.
29* Fenced code blocks in docs defined with the "example" attribute are rendered
31* Fenced code blocks declared to be Idris code that fail to parse or type check now
32 provide error messages to IDE clients.
33* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
38* Tactic for case analysis in proofs
39* Induction and case tactic now work on expressions
40* Support for running tests for a package with the tests section of .ipkg files and the
41 --testpkg command-line option
42* Clearly distinguish between type providers and postulate providers at the use site
43* Allow dependent function syntax to be overridden in dsl blocks, similarly to
44 functions and let. The keyword for this is "pi".
45* Updated 'effects' library, with simplified API
46* All new JavaScript backend (avoids callstack overflows)
47* Add support for %lib directive for NodeJS
48* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
49 `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
50 version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
51 terms to splice in, while on the LHS they are patterns.
52 A quasiquote expression can be given a goal type for the elaborator, which helps with
53 disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)
55 Both goal types and quasiquote are typechecked in the global environment.
56* Better inference of unbound implicits
60* IDE support for retrieving structured information about metavariables
61* Experimental Bits support for JavaScript
62* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
63* Command line option -e (or --eval) to evaluate expressions without loading the
64 REPL. This is useful for writing more portable tests.
65* Many more of the basic functions and datatypes are documented.
66* Primitive types such as Int and String are documented
67* Removed javascript lib in favor of idris-hackers/iQuery
68* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
69* Remove :info REPL command, subsume and enhance its functionality in the :doc command
70* New (first class) nested record update/access syntax:
71 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
72 record { a->b->c } x -- accesses field, equivalent to c (b (a x))
73* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
74* :apropos now accepts space-delimited lists of query items, and searches for the conjunction
75 of its inputs. It also accepts binder syntax as search strings - for instance, -> finds
77* Totality errors are now treated as warnings until code generation time, when they become
78 errors again. This allows users to use the interactive editing features to fix totality
79 issues, but no programs that violate the stated assumptions will actually run.
80* Added :makelemma command, which adds a new top level definition to solve
82* Extend :addclause to add instance bodies as well as definitions
83* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
84* Move foldl into Foldable so it can be overridden.
85* Experimental :search REPL command for finding functions by type
89* New implementation of erasure
94* Proof search now works for metavariables in types, giving some interactive
96* New 'Lazy' type, replacing laziness annotations.
97* JavaScript and Node codegen now understand the %include directive.
98* Concept of 'null' is now understood in the JavaScript and Node codegen.
99* Lots of performance patches for generated JavaScript.
100* New commands :eval (:e) and :type (:t) in the prover, which either normalise
101 or show the type of expressions.
102* Allow type providers to return postulates in addition to terms.
103* Syntax for dealing with match failure in <- and pattern matching let.
104* New syntax for inline documentation. Documentation starts with |||, and
105 arguments are documented by preceding their name with @. Example:
106 ||| Add two natural numbers
107 ||| @ n the first number (examined by the function)
108 ||| @ m the second number (not examined)
109 plus (n, m : Nat) -> Nat
110* Allow the auto-solve behaviour in the prover to be disabled, for easier
111 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
112* Updated 'effects' library
113* New :apropos command at REPL to search documentation, names, and types
114* Unification errors are now slightly more informative
115* Support mixed induction/coinduction with 'Inf' type
116* Add 'covering' function option, which checks whether a function and all
117 descendants cover all possible inputs
122* Agda-style equational reasoning (in Syntax.PreorderReasoning)
123* 'case' construct now abstracts over the scrutinee in its type
124* Added label type 'name (equivalent to the empty type).
125 This is intended for field/effect disambiguation. "name" can be any
126 valid identifier. Two labels are definitionally equal if they have the
128* General improvements in error messages, especially %error_reverse
129 annotation, which allows a hint as to how to display a term in error
131* --ideslave mode now transmits semantic information about many of the
132 strings that it emits, which can be used by clients to implement
133 semantic highlighting like that of the REPL. This has been implemented
134 in the Emacs mode and the IRC bot, which can serve as examples.
135* New expression form: with NAME EXPR privileges the namespace NAME
136 when disambiguating overloaded names. For example, it is possible to
137 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
138 because the Vect constructors are defined in a namespace called Vect.
139* assert_smaller internal function, which marks an expression as smaller than
140 a pattern for use in totality checking.
141 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
142 structurally smaller than "(x :: xs)"
143* assert_total internal function, which marks a subexpression as assumed to
144 be total, e.g "assert_total (tail (x :: xs))".
145* Terminal width is automatically detected if Idris is compiled with curses
146 support. If curses is not available, automatic mode assumes 80 columns.
147* Changed argument order for Prelude.Either.either.
148* Experimental 'neweffects' library, intended to replace 'effects' in the
155* Pretty-printer now used for all term output
161* Type classes now implemented as dependent records, meaning that method
162 types may now depend on earlier methods.
163* More flexible class instance resolution, so that function types and lambda
164 expressions can be made instances of a type class.
165* Add !expr notation for implicit binding of intermediate results in
166 monadic/do/etc expressions.
167* Extend Effects package to cope with possibly failing operations, using
168 "if_valid", "if_error", etc.
169* At the REPL, "it" now refers to the previous expression.
170* Semantic colouring at the REPL. Turn this off with --nocolour.
171* Some prettifying of error messages.
172* The contents of ~/.idris/repl/init are run at REPL start-up.
173* The REPL stores a command history in ~/.idris/repl/history.
174* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
175 checker and can thus be used in types. The [x..] syntax now returns an
176 actually infinite stream.
177* Add '%reflection' option for functions, for compile-time operations on
179* Add expression form 'quoteGoal x by p in e' which applies p to the expected
180 expression type and binds the result to x in the scope e.
181* Performance improvements in Strings library.
182* Library reorganisation, separated into prelude/ and base/.
186* New module/dependency tree checking.
187* New parser implementation with more precise errors.
188* Improved type class resolution.
189* Compiling Nat via GMP integers.
190* Performance improvements in elaboration.
191* Improvements in termination checking.
192* Various REPL commands to support interactive editing, and a client/server
193 mode to allow external invocation of REPL commands.
198* Apply functions by return type, rather than with arguments:
199 "t <== f" means "apply f with arguments such that it returns a value
201* Allow the result type of a rewrite to be specified
202* Allow names to be attached to provisional definitions
203 lhs ?= {name} rhs -- generates a lemma called 'name' which makes the
204 types of the lhs and rhs match. {name} is optional - a unique name is
205 generated if it is absent.
206* Experimental LLVM backend
207* Added Data.HVect module
208* Fix fromInteger to take an Integer, rather than an Int
209* Integer literals for Fin
210* Renamed O to Z, and fO to fZ
211* Swapped Vect arguments, now Vect : Nat -> Type -> Type
212* Added DecEq instances
213* Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal
217* Add annotation for unification traces
218* Add 'mrefine' tactic for refining by matching against a type
219* Type class resolution fixes
220* Much faster coverage checking
227* Added "rewrite ... in ..." construct
228* Allow type class constraints in 'using' clauses
229* Renamed EFF to EFFECT in Effect package
230* Experimental Java backend
231* Tab completion in REPL
232* Dynamic loading of C libraries in the interpreter
233* Testing IO actions at the REPL with :x command
234* Improve rendering of :t
235* Fixed some INTERNAL ERROR messages
239* Fix non-linear pattern checking
240* Improved name disambiguation
241* More flexible unification and elaboration of lambdas
242* Various unification and totality checking bug fixes
249* 'implicit' keyword, for implicit type conversion
250* Added Effects package
251* Primitives for 8,16,32 and 64 bit integers
255* Change unification so that it keeps track of failed constraints in case
256 later information helps to resolve them
257* Distinguishing parameters and indices in data types
258* Faster termination/coverage checking
259* Split 'javascript' target into 'javascript' and 'node'
266* The type of types is now 'Type' rather than 'Set'
267* Forward declarations of data allowed
268 - supporting induction recursion and mutually recursive data
269* Type inference of definitions in 'where' clauses
270 - Provided that the type can be completely determined from the first
271 application of the function (in the top level definition)
272* 'mutual' blocks added
273 - effect is to elaborate all types of declarations in the block before
274 elaborating their definitions
275 - allows inductive-recursive definitions
276* Expression inspected by 'with' clause now abstracted from the goal
278* Implicit arguments will be added automatically only if their initial
279 letter is lower case, or they are in a using declaration
280* Added documentation comments (Haddock style) and ':doc' REPL command
281* Pattern matching on strings, big integers and characters
282* Added System.Concurrency modules
283* Added 'postulate' declarations
284* Allow type annotations on 'let' tactic
285* EXPERIMENTAL JavaScript generation, with '--target javascript' option
289* Separate inlining methods at compile-time and run-time
290* Fixed nested parameters blocks
291* Improve efficiency of elaborator by:
292 - only normalising when necessary
293 - reducing backtracking with resolving ambiguities
294* Better compilation of case trees
302 - as data declarations, but constructor arguments are evaluated lazily
303 - functions which return a codata type do not reduce at compile time
304* Added 'parameters' blocks
305* Allow local data definitions in where blocks
306* Added '%default' directive to declare total-by-default or partial-by-default
307 for functions, and a corresponding "partial" reserved words to mark functions
308 as allowed to be partial. Also "--total" and "--partial" added as command
310* Command line option "--warnpartial" for flagging all undeclared
311 partial functions, without error.
312* New termination checker supporting mutually recursive definitions.
313* Added ':load' command to REPL, for loading a new file
314* Added ':module' command to REPL, for adding modules
315* Renamed library modules (now have initial capital)
319* Several improvements and fixes to unification
320* Added collapsing optimisation and more aggressive erasure
327* Simple packaging system
328* Added --dumpc flag for displaying generated code
332* Improve overloading resolution (especially where this is a type error)
333* Various important bug fixes with evaluation and compilation
334* More aggressive compile-time evaluation
341* Added binding forms to syntax rules
342* Named class instances
343* Added ':set' command, with options 'errorcontext' for displaying local
344 variables in scope when a unification error occurs, and 'showimplicits'
345 for displaying elaborated terms in full
346* Added '--errorcontext' command line switch
347* Added ':proofs' and ':rmproofs' commands
348* Various minor REPL improvements and fixes
352* Completely new run time system (not based on Epic or relying on Boehm GC)
353* Normalise before forcing to catch more forceable arguments
354* Types no longer exported in normal form
355* Try to resolve overloading by inspecting types, rather than full type
363* backtick notation added: x `foo` y ==> foo x y
364* case expressions allowed in type signatures
365* Library extensions in prelude.vect and prelude.algebra
366* malloc/trace_malloc added to builtins.idr
370* Some type class resolution fixes
371* Several minor bug fixes
372* Performance improvements in resolving overloading and type classes
379* DSL notation, for overloading lambda and let bindings
380* Dependent records, with projection and update
381* Totality checking and 'total' keyword
382* Auto implicits and default argument values {auto n : T}, {default val n : T}
383* Overlapping type class instances disallowed
384* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
386* New libraries: control.monad.identity, control.monad.state
387* Small improvements in error reporting
391* Faster compilation (only compiling names which are used)
392* Better type class resolution
393* Lots of minor bug fixes
397Complete rewrite. User visible changes:
399* New proof/tactics syntax
400* New syntax for pairs/dependent pairs
401* Indentation-significant syntax
404* Added case expressions, pattern matching let and lambda
405* Added monad comprehensions
406* Added cumulativity and universe checking
407* Ad-hoc name overloading
408 - Resolved by type or explicit namespace
409* Modules (Haskell-style)
410* public, abstract and private access to functions and types
411* Separate type-checking
412* Improved interactive environment
413* Replaced 'do using' with Monad class
414* Extended syntax macros
419* All definitions (functions, classes and instances) are elaborated to top
420 level, fully explicit, data declarations and pattern matching definitions,
421 which are verified by a minimal type checker.
423This is the first release of a complete reimplementation. There will be bugs.
424If you find any, please do not hesitate to contact Edwin Brady
425(ecb10@st-andrews.ac.uk).
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list