@@ -1,776 +0,0 @@
1−New in 0.12:
2−============
3−
4−* Improved startup performance by reducing the processing of an already imported
5− module that has changed accessibility.
6−
7−* A limited set of command line options can be used to override
8− package declared options. Overridable options are currently,
9− logging level and categories, default totality check, warn reach,
10− IBC output folder, and idris path.
11−
12−* Remove deprecated options `--ideslave` and `--ideslave-socket`. These options
13− were replaced with `--ide-mode` and `--ide-mode-socket` in 0.9.17
14−
15−New in 0.11:
16−============
17−
18−Updated export rules
19−--------------------
20−
21−* The export rules are:
22− - 'private' means that the definition is not exported at all
23− - 'export' means that the top level type is exported, but not the
24− definition. In the case of 'data', this means the type constructor is
25− exported but not the data constructors.
26− - 'public export' means that the entire definition is exported.
27−* By default, names are 'private'. This can be altered with an %access
28− directive as before.
29−* Exported types can only refer to other exported names
30−* Publicly exported definitions can only refer to publicly exported names
31−
32−Improved C FFI
33−--------------
34−
35−* Idris functions can now be passed as callbacks to C functions or wrapped
36−in a C function pointer.
37−* C function pointers can be called.
38−* Idris can access pointers to C globals.
39−
40−Effects
41−-------
42−
43−* Effects can now be given in any order in effect lists (there is no need
44−for the ordering to be preserved in sub lists of effects)
45−
46−Elaborator reflection updates
47−-----------------------------
48−
49−* Datatypes can now be defined from elaborator reflection:
50− - declareDatatype adds the type constructor declaration to the context
51− - defineDatatype adds the constructors to the datatype
52− - To declare an inductive-recursive family, declare the types of the
53− function and the type constructor before defining the pattern-match
54− cases and constructors.
55−
56−Minor language changes
57−----------------------
58−
59−* The '[static]' annotation is changed to '%static' to be consistent with the
60− other annotations.
61−* Added '%auto_implicits' directive. The default is '%auto_implicits on'.
62− Placing '%auto_implicits off' in a source file means that after that
63− point, any implicit arguments must be bound, e.g.:
64− append : {n,m,a:_} -> Vect n a -> Vect m a -> Vect (n + m) a
65−
66− Only names which are used explicitly in the type need to be bound, e.g.:
67− Here : {x, xs : _} -> Elem x (x :: xs)
68−
69− In 'Here', there is no need to bind any of the variables in the type of
70− 'xs' (it could be e.g. List a or Vect n a; 'a' and 'n' will still be
71− implicitly bound).
72−
73− You can still implicitly bind with 'using':
74−
75− using (xs : Vect _ _)
76− data Elem : {a, n : _} -> a -> Vect n a -> Type where
77− Here : {x : _} -> Elem x (x :: xs)
78− There : {x, y : _} -> Elem x xs -> Elem x (y :: xs)
79−
80− However, note that *only* names which appear in *both* the using block
81− *and* the type being defined will be implicitly bound. The following will
82− therefore fail because 'n' isn't implicitly bound:
83−
84− using (xs : Vect n a)
85− bad : Elem x xs -> Elem x (y :: xs)
86−* `Sigma` has been renamed to `DPair`.
87−* Accessor functions for dependent pairs have been renamed to bring them into
88− line with standard accessor functions for pairs. The function `getWitness`
89− is now `fst`, and `getProof` is `snd`.
90−* File Modes expanded: Append, ReadWriteTruncate, and ReadAppend added,
91− Write is deprecated and renamed to WriteTruncate.
92−* C11 Extended Mode variations added to File Modes.
93−* More flexible holes.
94− Holes can now depend on other holes in a term (such as implicit arguments
95− which may be inferred from the definition of the hole).
96−* Programs with holes can now be compiled.
97− Attempting to evaluate an expression with a hole results in a run time error.
98−* Dependent pairs now can be specified using a telescope-style syntax, without
99− requirement of nesting, e.g. it is possible to now write the following:
100− (a : Type ** n : Nat ** Vect n a)
101−* Idris will give a warning if an implicit is bound automatically, but would
102− otherwise be a valid expressio if the name was used as a global
103−
104−External Dependencies
105−---------------------
106−
107−* Curses has been removed as an external dependancy.
108−
109−New in 0.10:
110−============
111−
112−* 'class' and 'instance' are now deprecated keywords. They have been
113− replaced by 'interface' and 'implementation' respectively. This is to
114− properly reflect their purpose.
115−* (/) operator moved into new Fractional interface.
116−* Idris' logging infrastructure has been categorised. Command line and repl
117− are available. For command line the option `--logging-categories CATS`
118− is used to pass in the categories. Here `CATS` is a colon separated quoted
119− string containing the categories to log. The REPL command is `logcats CATS`.
120− Where `CATS` is a whitespace separated list of categoriese. Default is for
121− all categories to be logged.
122−* New flag `--listlogcats` to list logging categories.`
123−
124−New in 0.9.20:
125−==============
126−
127−Language updates
128−----------------
129−
130−* Improved unification by implementing a pattern unification rule
131−* The syntax `{{n}} quotes n without resolving it, allowing short syntax
132− for defining new names. `{n} still quotes n to an existing name in scope.
133−* A new primitive operator prim__strSubstr for more efficient extraction of
134− substrings. External code generators should implement this.
135−* The previous syntax for tactic proofs and the previous interactive prover
136− are now deprecated in favour of reflected elaboration. They will be removed
137− at some point in the future.
138−* Changed scoping rules for unbound implicits: any name which would be a
139− valid unbound implicit is now *always* an unbound implicit. This is much
140− more resilient to changes in inputs, but does require that function names
141− be explicitly qualified when in argument position.
142−* Name binding in patterns follows the same rule as name binding for implicits
143− in types: names which begin with lower case letters, not applied to any
144− arguments, are treated as bound pattern variables.
145−* Added %deprecate directive, which gives a warning and a message when a
146− deprecated name is referenced.
147−
148−Library updates
149−---------------
150−
151−* The 'Neg' class now represents numeric types which can be negative. As
152− such, the (-) operator and 'abs' have been moved there from 'Num'.
153−* A special version of (-) on 'Nat' requires that the second argument is
154− smaller than or equal to the first. 'minus' retains the old behaviour,
155− returning Z if there is an underflow.
156−* The (+), (-), and (*) operations on Fin have been removed.
157−* New Logging Effects have been added to facilitate logging of effectful
158− programmes.
159−* Elaborator reflection is now a part of the prelude. It is no longer
160− necessary to import Language.Reflection.Elab.
161−* The `PERF` effect allows for simple performance metrics to be collected
162− from Effectful programs.
163−* Some constructors that never actually occurred have been removed from
164− the TT and Raw reflection datatypes in Language.Reflection.
165−* File IO operations (for example openFile/fread/fwrite) now return
166− 'Either FileError ty' where the return type was previously 'ty' to indicate
167− that they may fail.
168−
169−Tool updates
170−------------
171−* Records are now shown as records in :doc, rather than as the underlying
172− datatype
173−* iPKG files have a new option `pkgs` which takes a comma-separated list
174− of package names that the idris project depends on. This reduces bloat
175− in the `opts` option with multiple package declarations.
176−* iPKG files now allow `executable = "your filename here"` in addition to
177− the existing `executable = yourFilenameHere` style. While the unquoted
178− version is limited to filenames that look like namespaced Idris identifiers
179− (`your.filename.here`), the quoted version accepts any valid filename.
180−* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now
181− adds missing clauses if there is already a definition.
182−
183−Miscellaneous updates
184−---------------------
185−* Disable the deprecation warnings for %elim and old-style tactic scripts
186− with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings
187− flags.
188−
189−
190−New in 0.9.19:
191−--------------
192−* The Idris Reference manual has been fleshed out with content originally found
193− on the GitHub wiki.
194−* The Show class has been moved into Prelude.Show and augmented with the method
195− showPrec, which allows correct parenthesization of showed terms. This comes
196− with the type Prec of precedences and a few helper functions.
197−* New REPL command :printerdepth that sets the pretty-printer to only descend to
198− some particular depth when printing. The default is set to a high number to
199− make it less dangerous to experiment with infinite structures. Infinite depth
200− can be set by calling :printerdepth with no argument.
201−* Compiler output shows applications of >>= in do-notation
202−* fromInteger i where i is an integer constant is now shown just as i in
203− compiler output
204−* An interactive shell, similar to the prover, for running reflected elaborator
205− actions. Access it with :elab from the REPL.
206−* New command-line option --highlight that causes Idris to save highlighting
207− information when successfully type checking. The information is in the same
208− format sent by the IDE mode, and is saved in a file with the extension ".idh".
209−* Highlighting information is saved by the parser as well, allowing it to highlight
210− keywords like "case", "of", "let", and "do"
211−* Use predicates instead of boolean equality proofs as preconditions
212− on List functions
213−* More flexible 'case' construct, allowing each branch to target different
214− types, provided that the case analysis does not affect the form of any
215− variable used in the right hand side of the case.
216−* Some improvements in interactive editing, particularly in lifting out
217− definitions and proof search.
218−* Moved System.Interactive, along with getArgs to the Prelude.
219−* Major improvements to reflected elaboration scripts, including the ability to run
220− them in a declaration context and many bug fixes.
221−* "decl syntax" rules to allow syntax extensions at the declaration level
222−* Experimental Windows support for console colours
223−
224−New in 0.9.18:
225−--------------
226−* GHC 7.10 compatibility
227−* Add support for bundled toolchains.
228−* Strings are now UTF8 encoded in the default back end
229−* Idris source files are now assumed to be in UTF8, regardless of locale
230− settings.
231−* Some reorganisation of primitives:
232− + Buffer and BitVector primitives have been removed (they were not
233− tested sufficiently, and lack a maintainer)
234− + Float has been renamed 'Double' (Float is defined in the Prelude for
235− compatibility)
236− + Externally defined primitives and operations now supported with
237− '%extern' directive, allowing back ends to define their own special
238− purpose primitives
239− + Ptr and ManagedPtr have been removed and replaced with external primitives
240−* Add %hint function annotation, which allows functions to be used as
241− hints in proof search for 'auto' arguments. Only functions which return
242− an instance of a data or record type are allowed as hints.
243−* Syntax rules no longer perform variable capture. Users of effects will
244− need to explicitly name results in dependent effect signatures instead
245− of using the default name "result".
246−* Pattern-matching lambdas are allowed to be impossible. For example,
247− Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
248− requiring a separate lemma.
249−* Case alternatives are allowed to be impossible:
250− case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
251−* The default Semigroup and Monoid instances for Maybe are now prioritised
252− choice, keeping the first success as Alternative does. The version that
253− collects successes is now a named instance.
254−* :exec REPL command now takes an optional expression to compile and run/show
255−* The return types of `Vect.findIndex`, `Vect.elemIndex` and
256− `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`
257−* A new :browse command shows the contents of a namespace
258−* `{n} is syntax for a quotation of the reflected representation of the name
259− "n". If "n" is lexically bound, then the resulting quotation will be for it,
260− whereas if it is not, then it will succeed with a quotation of the unique
261− global name that matches.
262−* New syntax for records that closely matches our other record-like structures:
263− type classes. See the updated tutorial for details.
264−* Records can be coinductive. Define coinductive records with the "corecord"
265− keyword.
266−* Type class constructors can be assigned user-accessible names. This is done
267− using the same syntax as record constructors.
268−* if ... then ... else ... is now built-in syntax instead of being defined in
269− a library. It is shown in REPL output and error messages, rather than its
270− desugaring.
271−* The desugaring of if ... then ... else ... has been renamed to ifThenElse from
272− boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
273− to reflect that if-notation makes sense with non-Bool datatypes.
274−* Agda-style semantic highlighting is supported over the IDE protocol.
275−* Experimental support for elaborator reflection. Users can now script the
276− elaborator, for use in code generation and proof automation. This feature is
277− still under rapid development and is subject to change without notice. See
278− Language.Reflection.Elab and the %runElab constructs
279−
280−
281−New in 0.9.17:
282−--------------
283−* The --ideslave command line option has been replaced with a --ide-mode
284− command line option with the same semantics.
285−* A new tactic "claim N TY" that introduces a new hole named N with type TY
286−* A new tactic "unfocus" that moves the current hole to the bottom of the
287− hole stack
288−* Quasiquotation supports the generation of Language.Reflection.Raw terms
289− in addition to Language.Reflection.TT. Types are used for disambiguation,
290− defaulting to TT at the REPL.
291−* Language.Reflection.Quotable now takes an extra type parameter which
292− determines the type to be quoted to. Instances are provided to quote
293− common types to both TT and Raw.
294−* Library operators have been renamed for consistency with Haskell. In
295− particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
296− now an alias for Functor.map. Correspondingly, ($>) and (<$) have
297− been renamed to (<*) and (*>). The cascading effects of this rename
298− are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
299− Matrix.(<.>) is now Matrix.(<:>).
300−* Binding forms in DSL notation are now given an extra argument: a
301− reflected representation of the name that the user chose.
302− Specifically, the rewritten lambda, pi, and let binders will now get
303− an extra argument of type TTName. This allows more understandable
304− dynamic errors in DSL code and more readable code generation results.
305−* DSL notation can now be applied with $
306−* Added FFI_Export type which allows Idris functions to be exportoed and
307− called from foreign code
308−* Instances can now have documentation strings.
309−* Type providers can have documentation strings.
310−* Unification errors now (where possible) contain information about provenance
311− of a type
312−* New REPL command ":core TM" that shows the elaborated form of TM along with
313− its elaborated type using the syntax of TT. IDE mode has a corresponding
314− command :elaborate-term for serialized terms.
315−* Effectful and IO function names for sending data to STDOUT have been
316− aligned, semantically.
317− + `print` is now for putting showable things to STDOUT.
318− + `printLn` is for putting showable things to STDOUT with a new line
319− + `putCharLn` for putting a single character to STDOUT, with a new line.
320−* Classes can now be annotated with 'determining parameters' to say which
321− must be available before resolving instances. Only determining parameters
322− are checked when checking for overlapping instances.
323−* New package 'contrib' containing things that are less mature or less used
324− than the contents of 'base'. 'contrib' is not available by default, so you
325− may need to add '-p contrib' to your .ipkg file or Idris command line.
326−* Arguments to class instances are now checked for injectivity.
327− Unification assumes this, so we need to check when instances are defined.
328−
329−New in 0.9.16:
330−--------------
331−* Inductive-inductive definitions are now supported (i.e. simultaneously
332− defined types where one is indexed by the other.)
333−* Implicits and type class constraints can now appear in scopes other than
334− the top level.
335−* Importing a module no longer means it is automatically reexported. A new
336− "public" modifier has been added to import statements, which will reexport
337− the names exported from that module.
338−* Implemented @-patterns. A pattern of the form x@p on the left hand side
339− matches p, with x in scope on the right hand side with value p.
340−* A new tactic sourceLocation that fills the current hole with the current
341− source code span, if this information is available. If not, it raises an
342− error.
343−* Better Unicode support for the JavaScript/Node codegen
344−* ':search' and ':apropos' commands can now be given optional package lists
345− to search.
346−* Vect, Fin and So moved out of prelude into base, in modules Data.Vect,
347− Data.Fin and Data.So respectively.
348−* Several long-standing issues resolved, particularly with pattern matching
349− and coverage checking.
350−* Modules can now have API documentation strings.
351−
352−New in 0.9.15:
353−--------------
354−* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
355− as an argument and produces it as an error.
356−* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
357− of ErrorReportParts as an argument, like error handlers produce, allowing
358− access to the pretty-printer.
359−* Stop showing irrelevant and inaccessible internal names in the interactive
360− prover.
361−* The proof arguments in the List library functions are now implicit and
362− solved automatically.
363−* More efficient representation of proof state, leading to faster elaboration
364− of large expressions.
365−* EXPERIMENTAL Implementation of uniqueness types
366−* Unary negation now desugars to "negate", which is a method of the Neg type class.
367− This allows instances of Num that can't be negative, like Nat, and it makes correct
368− IEEE Float operations easier to encode. Additionally, unary negation is now available
369− to DSL authors.
370−* The Java and LLVM backends have been factored out for separate maintenance. Now, the
371− compiler distribution only ships with the C and JavaScript backends.
372−* New REPL command :printdef displays the internal definition of a name
373−* New REPL command :pprint pretty-prints a definition or term with LaTeX or
374− HTML highlighting
375−* Naming of data and type constructors is made consistent across the standard
376− library (see #1516)
377−* Terms in `code blocks` inside of documentation strings are now parsed and
378− type checked. If this succeeds, they are rendered in full color in
379− documentation lookups, and with semantic highlighting for IDEs.
380−* Fenced code blocks in docs defined with the "example" attribute are rendered
381− as code examples.
382−* Fenced code blocks declared to be Idris code that fail to parse or type check now
383− provide error messages to IDE clients.
384−* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
385− Engine style)
386−
387−New in 0.9.14:
388−--------------
389−* Tactic for case analysis in proofs
390−* Induction and case tactic now work on expressions
391−* Support for running tests for a package with the tests section of .ipkg files and the
392− --testpkg command-line option
393−* Clearly distinguish between type providers and postulate providers at the use site
394−* Allow dependent function syntax to be overridden in dsl blocks, similarly to
395− functions and let. The keyword for this is "pi".
396−* Updated 'effects' library, with simplified API
397−* All new JavaScript backend (avoids callstack overflows)
398−* Add support for %lib directive for NodeJS
399−* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
400− `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
401− version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
402− terms to splice in, while on the LHS they are patterns.
403− A quasiquote expression can be given a goal type for the elaborator, which helps with
404− disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)
405− quotes the unit type.
406− Both goal types and quasiquote are typechecked in the global environment.
407−* Better inference of unbound implicits
408−
409−New in 0.9.13:
410−--------------
411−* IDE support for retrieving structured information about metavariables
412−* Experimental Bits support for JavaScript
413−* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
414−* Command line option -e (or --eval) to evaluate expressions without loading the
415− REPL. This is useful for writing more portable tests.
416−* Many more of the basic functions and datatypes are documented.
417−* Primitive types such as Int and String are documented
418−* Removed javascript lib in favor of idris-hackers/iQuery
419−* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
420−* Remove :info REPL command, subsume and enhance its functionality in the :doc command
421−* New (first class) nested record update/access syntax:
422− record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
423− record { a->b->c } x -- accesses field, equivalent to c (b (a x))
424−* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
425−* :apropos now accepts space-delimited lists of query items, and searches for the conjunction
426− of its inputs. It also accepts binder syntax as search strings - for instance, -> finds
427− functions.
428−* Totality errors are now treated as warnings until code generation time, when they become
429− errors again. This allows users to use the interactive editing features to fix totality
430− issues, but no programs that violate the stated assumptions will actually run.
431−* Added :makelemma command, which adds a new top level definition to solve
432− a metavariable.
433−* Extend :addclause to add instance bodies as well as definitions
434−* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
435−* Move foldl into Foldable so it can be overridden.
436−* Experimental :search REPL command for finding functions by type
437−
438−Internal changes
439−
440−* New implementation of erasure
441−
442−New in 0.9.12:
443−--------------
444−
445−* Proof search now works for metavariables in types, giving some interactive
446− type inference.
447−* New 'Lazy' type, replacing laziness annotations.
448−* JavaScript and Node codegen now understand the %include directive.
449−* Concept of 'null' is now understood in the JavaScript and Node codegen.
450−* Lots of performance patches for generated JavaScript.
451−* New commands :eval (:e) and :type (:t) in the prover, which either normalise
452− or show the type of expressions.
453−* Allow type providers to return postulates in addition to terms.
454−* Syntax for dealing with match failure in <- and pattern matching let.
455−* New syntax for inline documentation. Documentation starts with |||, and
456− arguments are documented by preceding their name with @. Example:
457− ||| Add two natural numbers
458− ||| @ n the first number (examined by the function)
459− ||| @ m the second number (not examined)
460− plus (n, m : Nat) -> Nat
461−* Allow the auto-solve behaviour in the prover to be disabled, for easier
462− debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
463−* Updated 'effects' library
464−* New :apropos command at REPL to search documentation, names, and types
465−* Unification errors are now slightly more informative
466−* Support mixed induction/coinduction with 'Inf' type
467−* Add 'covering' function option, which checks whether a function and all
468− descendants cover all possible inputs
469−
470−New in 0.9.11:
471−--------------
472−
473−* Agda-style equational reasoning (in Syntax.PreorderReasoning)
474−* 'case' construct now abstracts over the scrutinee in its type
475−* Added label type 'name (equivalent to the empty type).
476− This is intended for field/effect disambiguation. "name" can be any
477− valid identifier. Two labels are definitionally equal if they have the
478− same name.
479−* General improvements in error messages, especially %error_reverse
480− annotation, which allows a hint as to how to display a term in error
481− messages
482−* --ideslave mode now transmits semantic information about many of the
483− strings that it emits, which can be used by clients to implement
484− semantic highlighting like that of the REPL. This has been implemented
485− in the Emacs mode and the IRC bot, which can serve as examples.
486−* New expression form: with NAME EXPR privileges the namespace NAME
487− when disambiguating overloaded names. For example, it is possible to
488− write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
489− because the Vect constructors are defined in a namespace called Vect.
490−* assert_smaller internal function, which marks an expression as smaller than
491− a pattern for use in totality checking.
492− e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
493− structurally smaller than "(x :: xs)"
494−* assert_total internal function, which marks a subexpression as assumed to
495− be total, e.g "assert_total (tail (x :: xs))".
496−* Terminal width is automatically detected if Idris is compiled with curses
497− support. If curses is not available, automatic mode assumes 80 columns.
498−* Changed argument order for Prelude.Either.either.
499−* Experimental 'neweffects' library, intended to replace 'effects' in the
500− next release.
501−
502−Internal changes
503−
504−* Faster elaboration
505−* Smaller .ibc files
506−* Pretty-printer now used for all term output
507−
508−
509−New in 0.9.10:
510−--------------
511−
512−* Type classes now implemented as dependent records, meaning that method
513− types may now depend on earlier methods.
514−* More flexible class instance resolution, so that function types and lambda
515− expressions can be made instances of a type class.
516−* Add !expr notation for implicit binding of intermediate results in
517− monadic/do/etc expressions.
518−* Extend Effects package to cope with possibly failing operations, using
519− "if_valid", "if_error", etc.
520−* At the REPL, "it" now refers to the previous expression.
521−* Semantic colouring at the REPL. Turn this off with --nocolour.
522−* Some prettifying of error messages.
523−* The contents of ~/.idris/repl/init are run at REPL start-up.
524−* The REPL stores a command history in ~/.idris/repl/history.
525−* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
526− checker and can thus be used in types. The [x..] syntax now returns an
527− actually infinite stream.
528−* Add '%reflection' option for functions, for compile-time operations on
529− syntax.
530−* Add expression form 'quoteGoal x by p in e' which applies p to the expected
531− expression type and binds the result to x in the scope e.
532−* Performance improvements in Strings library.
533−* Library reorganisation, separated into prelude/ and base/.
534−
535−Internal changes
536−
537−* New module/dependency tree checking.
538−* New parser implementation with more precise errors.
539−* Improved type class resolution.
540−* Compiling Nat via GMP integers.
541−* Performance improvements in elaboration.
542−* Improvements in termination checking.
543−* Various REPL commands to support interactive editing, and a client/server
544− mode to allow external invocation of REPL commands.
545−
546−New in 0.9.9:
547−-------------
548−
549−* Apply functions by return type, rather than with arguments:
550− "t <== f" means "apply f with arguments such that it returns a value
551− of type t"
552−* Allow the result type of a rewrite to be specified
553−* Allow names to be attached to provisional definitions
554− lhs ?= {name} rhs -- generates a lemma called 'name' which makes the
555− types of the lhs and rhs match. {name} is optional - a unique name is
556− generated if it is absent.
557−* Experimental LLVM backend
558−* Added Data.HVect module
559−* Fix fromInteger to take an Integer, rather than an Int
560−* Integer literals for Fin
561−* Renamed O to Z, and fO to fZ
562−* Swapped Vect arguments, now Vect : Nat -> Type -> Type
563−* Added DecEq instances
564−* Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal
565−
566−Internal changes
567−
568−* Add annotation for unification traces
569−* Add 'mrefine' tactic for refining by matching against a type
570−* Type class resolution fixes
571−* Much faster coverage checking
572−
573−New in 0.9.8:
574−-------------
575−
576−User visible changes:
577−
578−* Added "rewrite ... in ..." construct
579−* Allow type class constraints in 'using' clauses
580−* Renamed EFF to EFFECT in Effect package
581−* Experimental Java backend
582−* Tab completion in REPL
583−* Dynamic loading of C libraries in the interpreter
584−* Testing IO actions at the REPL with :x command
585−* Improve rendering of :t
586−* Fixed some INTERNAL ERROR messages
587−
588−Internal changes:
589−
590−* Fix non-linear pattern checking
591−* Improved name disambiguation
592−* More flexible unification and elaboration of lambdas
593−* Various unification and totality checking bug fixes
594−
595−New in 0.9.7:
596−-------------
597−
598−User visible changes:
599−
600−* 'implicit' keyword, for implicit type conversion
601−* Added Effects package
602−* Primitives for 8,16,32 and 64 bit integers
603−
604−Internal changes:
605−
606−* Change unification so that it keeps track of failed constraints in case
607− later information helps to resolve them
608−* Distinguishing parameters and indices in data types
609−* Faster termination/coverage checking
610−* Split 'javascript' target into 'javascript' and 'node'
611−
612−New in 0.9.6:
613−-------------
614−
615−User visible changes:
616−
617−* The type of types is now 'Type' rather than 'Set'
618−* Forward declarations of data allowed
619− - supporting induction recursion and mutually recursive data
620−* Type inference of definitions in 'where' clauses
621− - Provided that the type can be completely determined from the first
622− application of the function (in the top level definition)
623−* 'mutual' blocks added
624− - effect is to elaborate all types of declarations in the block before
625− elaborating their definitions
626− - allows inductive-recursive definitions
627−* Expression inspected by 'with' clause now abstracted from the goal
628− - i.e. "magic" with
629−* Implicit arguments will be added automatically only if their initial
630− letter is lower case, or they are in a using declaration
631−* Added documentation comments (Haddock style) and ':doc' REPL command
632−* Pattern matching on strings, big integers and characters
633−* Added System.Concurrency modules
634−* Added 'postulate' declarations
635−* Allow type annotations on 'let' tactic
636−* EXPERIMENTAL JavaScript generation, with '--target javascript' option
637−
638−Internal changes:
639−
640−* Separate inlining methods at compile-time and run-time
641−* Fixed nested parameters blocks
642−* Improve efficiency of elaborator by:
643− - only normalising when necessary
644− - reducing backtracking with resolving ambiguities
645−* Better compilation of case trees
646−
647−New in 0.9.5:
648−-------------
649−
650−User visible changes:
651−
652−* Added codata
653− - as data declarations, but constructor arguments are evaluated lazily
654− - functions which return a codata type do not reduce at compile time
655−* Added 'parameters' blocks
656−* Allow local data definitions in where blocks
657−* Added '%default' directive to declare total-by-default or partial-by-default
658− for functions, and a corresponding "partial" reserved words to mark functions
659− as allowed to be partial. Also "--total" and "--partial" added as command
660− line options.
661−* Command line option "--warnpartial" for flagging all undeclared
662− partial functions, without error.
663−* New termination checker supporting mutually recursive definitions.
664−* Added ':load' command to REPL, for loading a new file
665−* Added ':module' command to REPL, for adding modules
666−* Renamed library modules (now have initial capital)
667−
668−Internal changes:
669−
670−* Several improvements and fixes to unification
671−* Added collapsing optimisation and more aggressive erasure
672−
673−New in 0.9.4:
674−-------------
675−
676−User visible changes:
677−
678−* Simple packaging system
679−* Added --dumpc flag for displaying generated code
680−
681−Internal changes:
682−
683−* Improve overloading resolution (especially where this is a type error)
684−* Various important bug fixes with evaluation and compilation
685−* More aggressive compile-time evaluation
686−
687−New in 0.9.3:
688−-------------
689−
690−User visible changes:
691−
692−* Added binding forms to syntax rules
693−* Named class instances
694−* Added ':set' command, with options 'errorcontext' for displaying local
695− variables in scope when a unification error occurs, and 'showimplicits'
696− for displaying elaborated terms in full
697−* Added '--errorcontext' command line switch
698−* Added ':proofs' and ':rmproofs' commands
699−* Various minor REPL improvements and fixes
700−
701−Internal changes:
702−
703−* Completely new run time system (not based on Epic or relying on Boehm GC)
704−* Normalise before forcing to catch more forceable arguments
705−* Types no longer exported in normal form
706−* Try to resolve overloading by inspecting types, rather than full type
707− checking
708−
709−New in 0.9.2:
710−-------------
711−
712−User visible changes:
713−
714−* backtick notation added: x `foo` y ==> foo x y
715−* case expressions allowed in type signatures
716−* Library extensions in prelude.vect and prelude.algebra
717−* malloc/trace_malloc added to builtins.idr
718−
719−Internal changes:
720−
721−* Some type class resolution fixes
722−* Several minor bug fixes
723−* Performance improvements in resolving overloading and type classes
724−
725−New in 0.9.1:
726−-------------
727−
728−User visible changes:
729−
730−* DSL notation, for overloading lambda and let bindings
731−* Dependent records, with projection and update
732−* Totality checking and 'total' keyword
733−* Auto implicits and default argument values {auto n : T}, {default val n : T}
734−* Overlapping type class instances disallowed
735−* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
736− Dominic Mulligan)
737−* New libraries: control.monad.identity, control.monad.state
738−* Small improvements in error reporting
739−
740−Internal changes:
741−
742−* Faster compilation (only compiling names which are used)
743−* Better type class resolution
744−* Lots of minor bug fixes
745−
746−0.1.x to 0.9.0:
747−
748−Complete rewrite. User visible changes:
749−
750−* New proof/tactics syntax
751−* New syntax for pairs/dependent pairs
752−* Indentation-significant syntax
753−* Added type classes
754−* Added where clauses
755−* Added case expressions, pattern matching let and lambda
756−* Added monad comprehensions
757−* Added cumulativity and universe checking
758−* Ad-hoc name overloading
759− - Resolved by type or explicit namespace
760−* Modules (Haskell-style)
761−* public, abstract and private access to functions and types
762−* Separate type-checking
763−* Improved interactive environment
764−* Replaced 'do using' with Monad class
765−* Extended syntax macros
766−
767−Internal changes:
768−
769−* Everything :-)
770−* All definitions (functions, classes and instances) are elaborated to top
771− level, fully explicit, data declarations and pattern matching definitions,
772− which are verified by a minimal type checker.
773−
774−This is the first release of a complete reimplementation. There will be bugs.
775−If you find any, please do not hesitate to contact Edwin Brady
776−(ecb10@st-andrews.ac.uk).