3* Add support for bundled toolchains.
4* Strings are now UTF8 encoded in the default back end
5* Idris source files are now assumed to be in UTF8, regardless of locale
7* Some reorganisation of primitives:
8 + Buffer and BitVector primitives have been removed (they were not
9 tested sufficiently, and lack a maintainer)
10 + Float has been renamed 'Double' (Float is defined in the Prelude for
12 + Externally defined primitives and operations now supported with
13 '%extern' directive, allowing back ends to define their own special
15 + Ptr and ManagedPtr have been removed and replaced with external primitives
16* Add %hint function annotation, which allows functions to be used as
17 hints in proof search for 'auto' arguments. Only functions which return
18 an instance of a data or record type are allowed as hints.
19* Syntax rules no longer perform variable capture. Users of effects will
20 need to explicitly name results in dependent effect signatures instead
21 of using the default name "result".
22* Pattern-matching lambdas are allowed to be impossible. For example,
23 Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
24 requiring a separate lemma.
25* Case alternatives are allowed to be impossible:
26 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
27* The default Semigroup and Monoid instances for Maybe are now prioritised
28 choice, keeping the first success as Alternative does. The version that
29 collects successes is now a named instance.
30* :exec REPL command now takes an optional expression to compile and run/show
34* The --ideslave command line option has been replaced with a --ide-mode
35 command line option with the same semantics.
36* A new tactic "claim N TY" that introduces a new hole named N with type TY
37* A new tactic "unfocus" that moves the current hole to the bottom of the
39* Quasiquotation supports the generation of Language.Reflection.Raw terms
40 in addition to Language.Reflection.TT. Types are used for disambiguation,
41 defaulting to TT at the REPL.
42* Language.Reflection.Quotable now takes an extra type parameter which
43 determines the type to be quoted to. Instances are provided to quote
44 common types to both TT and Raw.
45* Library operators have been renamed for consistency with Haskell. In
46 particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
47 now an alias for Functor.map. Correspondingly, ($>) and (<$) have
48 been renamed to (<*) and (*>). The cascading effects of this rename
49 are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
50 Matrix.(<.>) is now Matrix.(<:>).
51* Binding forms in DSL notation are now given an extra argument: a
52 reflected representation of the name that the user chose.
53 Specifically, the rewritten lambda, pi, and let binders will now get
54 an extra argument of type TTName. This allows more understandable
55 dynamic errors in DSL code and more readable code generation results.
56* DSL notation can now be applied with $
57* Added FFI_Export type which allows Idris functions to be exportoed and
58 called from foreign code
59* Instances can now have documentation strings.
60* Type providers can have documentation strings.
61* Unification errors now (where possible) contain information about provenance
63* New REPL command ":core TM" that shows the elaborated form of TM along with
64 its elaborated type using the syntax of TT. IDE mode has a corresponding
65 command :elaborate-term for serialized terms.
66* Effectful and IO function names for sending data to STDOUT have been
67 aligned, semantically.
68 + `print` is now for putting showable things to STDOUT.
69 + `printLn` is for putting showable things to STDOUT with a new line
70 + `putCharLn` for putting a single character to STDOUT, with a new line.
71* Classes can now be annotated with 'determining parameters' to say which
72 must be available before resolving instances. Only determining parameters
73 are checked when checking for overlapping instances.
74* New package 'contrib' containing things that are less mature or less used
75 than the contents of 'base'. 'contrib' is not available by default, so you
76 may need to add '-p contrib' to your .ipkg file or Idris command line.
77* Arguments to class instances are now checked for injectivity.
78 Unification assumes this, so we need to check when instances are defined.
82* Inductive-inductive definitions are now supported (i.e. simultaneously
83 defined types where one is indexed by the other.)
84* Implicits and type class constraints can now appear in scopes other than
86* Importing a module no longer means it is automatically reexported. A new
87 "public" modifier has been added to import statements, which will reexport
88 the names exported from that module.
89* Implemented @-patterns. A pattern of the form x@p on the left hand side
90 matches p, with x in scope on the right hand side with value p.
91* A new tactic sourceLocation that fills the current hole with the current
92 source code span, if this information is available. If not, it raises an
94* Better Unicode support for the JavaScript/Node codegen
95* ':search' and ':apropos' commands can now be given optional package lists
97* Vect, Fin and So moved out of prelude into base, in modules Data.Vect,
98 Data.Fin and Data.So respectively.
99* Several long-standing issues resolved, particularly with pattern matching
100 and coverage checking.
101* Modules can now have API documentation strings.
105* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
106 as an argument and produces it as an error.
107* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
108 of ErrorReportParts as an argument, like error handlers produce, allowing
109 access to the pretty-printer.
110* Stop showing irrelevant and inaccessible internal names in the interactive
112* The proof arguments in the List library functions are now implicit and
113 solved automatically.
114* More efficient representation of proof state, leading to faster elaboration
115 of large expressions.
116* EXPERIMENTAL Implementation of uniqueness types
117* Unary negation now desugars to "negate", which is a method of the Neg type class.
118 This allows instances of Num that can't be negative, like Nat, and it makes correct
119 IEEE Float operations easier to encode. Additionally, unary negation is now available
121* The Java and LLVM backends have been factored out for separate maintenance. Now, the
122 compiler distribution only ships with the C and JavaScript backends.
123* New REPL command :printdef displays the internal definition of a name
124* New REPL command :pprint pretty-prints a definition or term with LaTeX or
126* Naming of data and type constructors is made consistent across the standard
128* Terms in `code blocks` inside of documentation strings are now parsed and
129 type checked. If this succeeds, they are rendered in full color in
130 documentation lookups, and with semantic highlighting for IDEs.
131* Fenced code blocks in docs defined with the "example" attribute are rendered
133* Fenced code blocks declared to be Idris code that fail to parse or type check now
134 provide error messages to IDE clients.
135* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
140* Tactic for case analysis in proofs
141* Induction and case tactic now work on expressions
142* Support for running tests for a package with the tests section of .ipkg files and the
143 --testpkg command-line option
144* Clearly distinguish between type providers and postulate providers at the use site
145* Allow dependent function syntax to be overridden in dsl blocks, similarly to
146 functions and let. The keyword for this is "pi".
147* Updated 'effects' library, with simplified API
148* All new JavaScript backend (avoids callstack overflows)
149* Add support for %lib directive for NodeJS
150* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
151 `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
152 version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
153 terms to splice in, while on the LHS they are patterns.
154 A quasiquote expression can be given a goal type for the elaborator, which helps with
155 disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)
156 quotes the unit type.
157 Both goal types and quasiquote are typechecked in the global environment.
158* Better inference of unbound implicits
162* IDE support for retrieving structured information about metavariables
163* Experimental Bits support for JavaScript
164* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
165* Command line option -e (or --eval) to evaluate expressions without loading the
166 REPL. This is useful for writing more portable tests.
167* Many more of the basic functions and datatypes are documented.
168* Primitive types such as Int and String are documented
169* Removed javascript lib in favor of idris-hackers/iQuery
170* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
171* Remove :info REPL command, subsume and enhance its functionality in the :doc command
172* New (first class) nested record update/access syntax:
173 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
174 record { a->b->c } x -- accesses field, equivalent to c (b (a x))
175* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
176* :apropos now accepts space-delimited lists of query items, and searches for the conjunction
177 of its inputs. It also accepts binder syntax as search strings - for instance, -> finds
179* Totality errors are now treated as warnings until code generation time, when they become
180 errors again. This allows users to use the interactive editing features to fix totality
181 issues, but no programs that violate the stated assumptions will actually run.
182* Added :makelemma command, which adds a new top level definition to solve
184* Extend :addclause to add instance bodies as well as definitions
185* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
186* Move foldl into Foldable so it can be overridden.
187* Experimental :search REPL command for finding functions by type
191* New implementation of erasure
196* Proof search now works for metavariables in types, giving some interactive
198* New 'Lazy' type, replacing laziness annotations.
199* JavaScript and Node codegen now understand the %include directive.
200* Concept of 'null' is now understood in the JavaScript and Node codegen.
201* Lots of performance patches for generated JavaScript.
202* New commands :eval (:e) and :type (:t) in the prover, which either normalise
203 or show the type of expressions.
204* Allow type providers to return postulates in addition to terms.
205* Syntax for dealing with match failure in <- and pattern matching let.
206* New syntax for inline documentation. Documentation starts with |||, and
207 arguments are documented by preceding their name with @. Example:
208 ||| Add two natural numbers
209 ||| @ n the first number (examined by the function)
210 ||| @ m the second number (not examined)
211 plus (n, m : Nat) -> Nat
212* Allow the auto-solve behaviour in the prover to be disabled, for easier
213 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
214* Updated 'effects' library
215* New :apropos command at REPL to search documentation, names, and types
216* Unification errors are now slightly more informative
217* Support mixed induction/coinduction with 'Inf' type
218* Add 'covering' function option, which checks whether a function and all
219 descendants cover all possible inputs
224* Agda-style equational reasoning (in Syntax.PreorderReasoning)
225* 'case' construct now abstracts over the scrutinee in its type
226* Added label type 'name (equivalent to the empty type).
227 This is intended for field/effect disambiguation. "name" can be any
228 valid identifier. Two labels are definitionally equal if they have the
230* General improvements in error messages, especially %error_reverse
231 annotation, which allows a hint as to how to display a term in error
233* --ideslave mode now transmits semantic information about many of the
234 strings that it emits, which can be used by clients to implement
235 semantic highlighting like that of the REPL. This has been implemented
236 in the Emacs mode and the IRC bot, which can serve as examples.
237* New expression form: with NAME EXPR privileges the namespace NAME
238 when disambiguating overloaded names. For example, it is possible to
239 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
240 because the Vect constructors are defined in a namespace called Vect.
241* assert_smaller internal function, which marks an expression as smaller than
242 a pattern for use in totality checking.
243 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
244 structurally smaller than "(x :: xs)"
245* assert_total internal function, which marks a subexpression as assumed to
246 be total, e.g "assert_total (tail (x :: xs))".
247* Terminal width is automatically detected if Idris is compiled with curses
248 support. If curses is not available, automatic mode assumes 80 columns.
249* Changed argument order for Prelude.Either.either.
250* Experimental 'neweffects' library, intended to replace 'effects' in the
257* Pretty-printer now used for all term output
263* Type classes now implemented as dependent records, meaning that method
264 types may now depend on earlier methods.
265* More flexible class instance resolution, so that function types and lambda
266 expressions can be made instances of a type class.
267* Add !expr notation for implicit binding of intermediate results in
268 monadic/do/etc expressions.
269* Extend Effects package to cope with possibly failing operations, using
270 "if_valid", "if_error", etc.
271* At the REPL, "it" now refers to the previous expression.
272* Semantic colouring at the REPL. Turn this off with --nocolour.
273* Some prettifying of error messages.
274* The contents of ~/.idris/repl/init are run at REPL start-up.
275* The REPL stores a command history in ~/.idris/repl/history.
276* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
277 checker and can thus be used in types. The [x..] syntax now returns an
278 actually infinite stream.
279* Add '%reflection' option for functions, for compile-time operations on
281* Add expression form 'quoteGoal x by p in e' which applies p to the expected
282 expression type and binds the result to x in the scope e.
283* Performance improvements in Strings library.
284* Library reorganisation, separated into prelude/ and base/.
288* New module/dependency tree checking.
289* New parser implementation with more precise errors.
290* Improved type class resolution.
291* Compiling Nat via GMP integers.
292* Performance improvements in elaboration.
293* Improvements in termination checking.
294* Various REPL commands to support interactive editing, and a client/server
295 mode to allow external invocation of REPL commands.
300* Apply functions by return type, rather than with arguments:
301 "t <== f" means "apply f with arguments such that it returns a value
303* Allow the result type of a rewrite to be specified
304* Allow names to be attached to provisional definitions
305 lhs ?= {name} rhs -- generates a lemma called 'name' which makes the
306 types of the lhs and rhs match. {name} is optional - a unique name is
307 generated if it is absent.
308* Experimental LLVM backend
309* Added Data.HVect module
310* Fix fromInteger to take an Integer, rather than an Int
311* Integer literals for Fin
312* Renamed O to Z, and fO to fZ
313* Swapped Vect arguments, now Vect : Nat -> Type -> Type
314* Added DecEq instances
315* Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal
319* Add annotation for unification traces
320* Add 'mrefine' tactic for refining by matching against a type
321* Type class resolution fixes
322* Much faster coverage checking
329* Added "rewrite ... in ..." construct
330* Allow type class constraints in 'using' clauses
331* Renamed EFF to EFFECT in Effect package
332* Experimental Java backend
333* Tab completion in REPL
334* Dynamic loading of C libraries in the interpreter
335* Testing IO actions at the REPL with :x command
336* Improve rendering of :t
337* Fixed some INTERNAL ERROR messages
341* Fix non-linear pattern checking
342* Improved name disambiguation
343* More flexible unification and elaboration of lambdas
344* Various unification and totality checking bug fixes
351* 'implicit' keyword, for implicit type conversion
352* Added Effects package
353* Primitives for 8,16,32 and 64 bit integers
357* Change unification so that it keeps track of failed constraints in case
358 later information helps to resolve them
359* Distinguishing parameters and indices in data types
360* Faster termination/coverage checking
361* Split 'javascript' target into 'javascript' and 'node'
368* The type of types is now 'Type' rather than 'Set'
369* Forward declarations of data allowed
370 - supporting induction recursion and mutually recursive data
371* Type inference of definitions in 'where' clauses
372 - Provided that the type can be completely determined from the first
373 application of the function (in the top level definition)
374* 'mutual' blocks added
375 - effect is to elaborate all types of declarations in the block before
376 elaborating their definitions
377 - allows inductive-recursive definitions
378* Expression inspected by 'with' clause now abstracted from the goal
380* Implicit arguments will be added automatically only if their initial
381 letter is lower case, or they are in a using declaration
382* Added documentation comments (Haddock style) and ':doc' REPL command
383* Pattern matching on strings, big integers and characters
384* Added System.Concurrency modules
385* Added 'postulate' declarations
386* Allow type annotations on 'let' tactic
387* EXPERIMENTAL JavaScript generation, with '--target javascript' option
391* Separate inlining methods at compile-time and run-time
392* Fixed nested parameters blocks
393* Improve efficiency of elaborator by:
394 - only normalising when necessary
395 - reducing backtracking with resolving ambiguities
396* Better compilation of case trees
404 - as data declarations, but constructor arguments are evaluated lazily
405 - functions which return a codata type do not reduce at compile time
406* Added 'parameters' blocks
407* Allow local data definitions in where blocks
408* Added '%default' directive to declare total-by-default or partial-by-default
409 for functions, and a corresponding "partial" reserved words to mark functions
410 as allowed to be partial. Also "--total" and "--partial" added as command
412* Command line option "--warnpartial" for flagging all undeclared
413 partial functions, without error.
414* New termination checker supporting mutually recursive definitions.
415* Added ':load' command to REPL, for loading a new file
416* Added ':module' command to REPL, for adding modules
417* Renamed library modules (now have initial capital)
421* Several improvements and fixes to unification
422* Added collapsing optimisation and more aggressive erasure
429* Simple packaging system
430* Added --dumpc flag for displaying generated code
434* Improve overloading resolution (especially where this is a type error)
435* Various important bug fixes with evaluation and compilation
436* More aggressive compile-time evaluation
443* Added binding forms to syntax rules
444* Named class instances
445* Added ':set' command, with options 'errorcontext' for displaying local
446 variables in scope when a unification error occurs, and 'showimplicits'
447 for displaying elaborated terms in full
448* Added '--errorcontext' command line switch
449* Added ':proofs' and ':rmproofs' commands
450* Various minor REPL improvements and fixes
454* Completely new run time system (not based on Epic or relying on Boehm GC)
455* Normalise before forcing to catch more forceable arguments
456* Types no longer exported in normal form
457* Try to resolve overloading by inspecting types, rather than full type
465* backtick notation added: x `foo` y ==> foo x y
466* case expressions allowed in type signatures
467* Library extensions in prelude.vect and prelude.algebra
468* malloc/trace_malloc added to builtins.idr
472* Some type class resolution fixes
473* Several minor bug fixes
474* Performance improvements in resolving overloading and type classes
481* DSL notation, for overloading lambda and let bindings
482* Dependent records, with projection and update
483* Totality checking and 'total' keyword
484* Auto implicits and default argument values {auto n : T}, {default val n : T}
485* Overlapping type class instances disallowed
486* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
488* New libraries: control.monad.identity, control.monad.state
489* Small improvements in error reporting
493* Faster compilation (only compiling names which are used)
494* Better type class resolution
495* Lots of minor bug fixes
499Complete rewrite. User visible changes:
501* New proof/tactics syntax
502* New syntax for pairs/dependent pairs
503* Indentation-significant syntax
506* Added case expressions, pattern matching let and lambda
507* Added monad comprehensions
508* Added cumulativity and universe checking
509* Ad-hoc name overloading
510 - Resolved by type or explicit namespace
511* Modules (Haskell-style)
512* public, abstract and private access to functions and types
513* Separate type-checking
514* Improved interactive environment
515* Replaced 'do using' with Monad class
516* Extended syntax macros
521* All definitions (functions, classes and instances) are elaborated to top
522 level, fully explicit, data declarations and pattern matching definitions,
523 which are verified by a minimal type checker.
525This is the first release of a complete reimplementation. There will be bugs.
526If you find any, please do not hesitate to contact Edwin Brady
527(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