Tags: atlv24/Idris-dev
Tags
New in 1.2.0:
* Language updates
+ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
of any definitions in `where` clauses, provided the left-hand side of the
definition does not shadow it.
+ The `LinearTypes` language extension has been revised. It implements the
rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative
Type Theory" and now works with holes and case expressions.
+ Backticked operators can appear in sections, e.g. ``(`LTE` 42)`` or
``(1 `plus`)``.
+ Backticked operators can have their precendence and associativity set like
other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with
undeclared fixity are treated as non-associative with precedence lower
than all declared operators.
+ Allow non-injective implementations if explicitly named, e.g.,
```idris
LTB : Nat -> Type
LTB b = DPair Nat (\ n => LT n b)
implementation [uninhabltb] Uninhabited (LTB Z) where
uninhabited (MkDPair n prf) = absurd prf
```
It is possible to use `using implementation uninhabltb` to add the
implementation to the automated resolution, but if it fails to find the
instance due to non-injectivity, one must pass it explicitly to target
function, i.e. `absurd @{uninhabltb}`.
+ Verbatim strings now support trailing quote characters. All quote characters
until the final three are considered part of the string. Now a string such as
`""""hello""""` will parse, and is equivalent to `"\"hello\""`.
+ C FFI now supports pasting in any expression by prefixing it with '#', e.g.
```idris
intMax : IO Int
intMax = foreign FFI_C "#INT_MAX" (IO Int)
```
+ The deprecated keywords `%assert_total`, `abstract`, and `[static]` have
been removed as well as the use of "public" instead of "public export" to
expose a symbol.
+ The syntax for pattern-match alternatives now works for `let` statements in
`do` blocks in addition to `let` expressions and `<-` statements, e.g.
```idris
do …
let Just x = expr | Nothing => empty
…
```
This means that a `with`-application (using `|`) cannot be used in that
position anymore.
* Library Updates
+ Removed `oldeffects` library from `libs` folder, use `effects` or `Control.ST` instead.
+ Added `Text.Literate`, a module for working with literate source files.
+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
+ Added `discriminate` and `construct` tactics to Pruviloj.
+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
+ Added `Data.IOArray`, containing primitives for mutable arrays.
+ Added `Language.JSON`, for total serialization/deserialization of JSON data.
+ Reworked operator fixity for many operators.
* Changed `&&` and `||` to be right-associative. Increased precedence of `&&`
to be higher than that of `||`.
* Removed associativity from Boolean comparison operators `==`, `/=`, `<`, `<=`,
`>`, and `>=`. Increased precedence of `/=` and `==` to match the others.
* Made `<|>`, `<$>`, and `.` right-associative.
* Swapped precedence of `<|>` and `<*>` (and its related operators, `<*` and
`*>`). Now `<|>` has a lower precedence.
* Lowered the precedence of `>>=` to be below that of `<|>`.
+ Added some useful string manipulation functions to `Data.String.Extra`.
+ Added `Control.Delayed`, a module for conditionally making a type `Inf` or `Lazy`.
+ Added `Data.Fuel`, which implements the `Fuel` data type and the partial `forever` function.
+ Added `Data.Bool.Extra`, a module with properties of boolean operations.
+ Moved core of `Text.Lexer` to `Text.Lexer.Core`. Added several new combinators
and lexers to `Text.Lexer`.
+ Moved core of `Text.Parser` to `Text.Parser.Core`. Added several new combinators
to `Text.Parser`. Made the following changes.
* Flipped argument order of `parse`.
* Renamed `optional` to `option` and flip argument order.
* Renamed `maybe` to `optional`.
* Generalised many combinators to use an unknown `commit` flag where possible.
+ `Prelude.Doubles.atan2` is now implemented as a primitive instead of
being coded in Idris.
+ Added `Test.Unit` to `contrib` for simple unit testing.
+ Removed several deprecated items from the libraries shipped with Idris.
+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
implements `Abs` with `abs = id`.
+ Added `Control.ST.File`, an ST based implementation of the same behaviour
implemented by `Effect.File` in the effects package.
* Tool Updates
+ Private functions are no longer visible in the REPL except for modules
that are explicitly loaded.
+ The --interface option now creates CommonJS modules on the node backend.
+ The C backend now pass arguments to the C compiler in the same order
as they were given in the source files.
+ Backslash, braces and percent symbols are now correctly pretty printed
in LaTeX.
+ Errors and warnings now consistently have the following format:
```idris
reg068.idr:1:6-8:
|
1 | data nat : Type where --error
| ~~~
Main.nat has a name which may be implicitly bound.
This is likely to lead to problems!
```
The code is highlighted when highlighting information is available. How
much highlighting information is available depends on where the error
occurred.
+ The parser provider has been switched from Trifecta to Megaparsec. This
could possibly cause some subtle deviations in parsing from previous
versions of Idris.
+ Many more errors now report beginning *and* ending position (which may be
on different lines), instead of just a single point. The format is
`Foo.idr:9:7-15:` if ending column is on the same line or
`Foo.idr:9:7-10:15:` if the ending column is on a different line.
+ Error messages were changed so that the last column is inclusive, e.g.
`Foo.idr:9:7-15:` includes column 15. Previously the error would have read
`Foo.idr:9:7-16:`.
* Packaging Updates
+ Package names now only accept a restrictive charset of letters, numbers and the `-_` characters.
Package names are also case insensitive.
+ When building makefiles for the FFI, the environment variables
`IDRIS_INCLUDES` and `IDRIS_LDFLAGS` are now set with the correct C
flags.
New in 1.1.0
Library Updates:
+ Added `Text.PrettyPrint.WL` an implementation of the Wadler-Leijen
Pretty-Print algorithm. Useful for those wishing to pretty print
things.
+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
for implementing total lexical analysers and parsers.
+ New instances:
+ Added `Catchable` for `ReaderT`, `WriterT`, and `RWST`.
+ Added `MonadTrans` for `RWST`.
+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
mapping from `a` to `Nat`. For example, there is an implementation for lists,
where `size = length`.
The function `sizeAccessible` then proves well-foundedness of the relation
`Smaller x y = LT (size x) (size y)`, which allows us to use strong
induction conveniently with any type that implements `Sized`.
In practice, this allows us to write functions that recurse not only on
direct subterms of their arguments but on any value
with a (strictly) smaller `size`.
A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
+ Added utility lemma `decEqSelfIsYes : decEq x x = Yes Refl` to
`Decidable.Equality`. This is primarily useful for proving properties of
functions defined with the help of `decEq`.
Tool Updates:
+ New JavaScript code generator that uses an higher level intermediate
representation.
+ Various optimizations of the new JavaScript code generator.
+ Names are now annotated with their representations over the IDE
protocol, which allows IDEs to provide commands that work on special
names that don't have syntax, such as case block names.
New in 1.0.1:
=============
Library Updates
---------------
+ Added `Text.PrettyPrint.WL` an implementation of the Wadler-Leijen
Pretty-Print algorithm. Useful for those wishing to pretty print
things.
+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
for implementing total lexical analysers and parsers.
+ New instances:
+ Added `Catchable` for `ReaderT`, `WriterT`, and `RWST`.
+ Added `MonadTrans` for `RWST`.
+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
mapping from `a` to `Nat`. For example, there is an implementation for lists,
where `size = length`.
The function `sizeAccessible` then proves well-foundedness of the relation
`Smaller x y = LT (size x) (size y)`, which allows us to use strong
induction conveniently with any type that implements `Sized`.
In practice, this allows us to write functions that recurse not only on
direct subterms of their arguments but on any value
with a (strictly) smaller `size`.
A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
+ Added utility lemma `decEqSelfIsYes : decEq x x = Yes Refl` to
`Decidable.Equality`. This is primarily useful for proving properties of
functions defined with the help of `decEq`.
Tool Updates
------------
+ New JavaScript code generator that uses an higher level intermediate
representation.
+ Various optimizations of the new JavaScript code generator.
+ Names are now annotated with their representations over the IDE
protocol, which allows IDEs to provide commands that work on special
names that don't have syntax, such as case block names.
New in 0.99.2 Library Updates + Added `Data.Buffer` to `base`. This allows basic manipulation of mutable buffers of `Bits8`, including reading from and writing to files. Tool Updates + Idris now checks the list of packages specified at the command line against those installed. If there is a mismatch Idris will complain. Miscellaneous Updates + Documentation updates for the new `Control.ST` library + Various stability/efficiency fixes
New in 0.99.1:
Language updates
* Language pragmas now required for the less stable existing features, in
addition to the existing `TypeProviders` and `ErrorReflection`:
+ `ElabReflection`, which must be enabled to use `%runElab`
+ `UniquenessTypes`, which must be enabled to use `UniqueType`
+ `DSLNotation`, which must be enabled to define a `dsl` block
+ `FirstClassReflection`, which must be enabled to define a `%reflection`
function
* New language extension `LinearTypes`:
+ This allows adding a /multiplicity/ to a binder which says how often it
is allowed to be used; either 0 or 1 (if unstated, multiplicity is "many")
+ The typing rules follow Conor McBride's paper "I Got Plenty o' Nuttin'"
+ This is highly experimental, unfinished, not at all polished. and there
are still lots of details to sort out. Some features don't quite work
properly yet. But it is there to play with for the brave!
Tool Updates
+ Idris' output has been updated to more accurately reflect its
progress through the compiler i.e. Type Checking; Totality Checking;
IBC Generation; Compiling; and Code Generation. To control the
loudness of the reporting three verbosity levels are introduced:
`--V0`, `--V1`, and `--V2`. The old aliases of `-V` and `--verbose`
persist.
+ New REPL command `:!` that runs an external shell command.
+ The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS)
on Windows, which previously did not occur due to a bug.
+ Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many
Unicode-rendering issues on Windows (e.g., error messages stating
`commitBuffer: invalid argument (invalid character)`).
+ Idris now has a `--warnipkg` flag to enable auditing of Idris
packages during build time. Currently auditing check's the list of
modules specified in the `iPKG` file with those presented in the
package directory.
Library Updates
+ Terminating programs has been improved with more appropriate
functions (`exitWith`, `exitFailure`, and `exitSuccess`) and a data
structure (`ExitCode`) to capture a program's return code.
+ Casting a `String` to an `Int`, `Integer` or a `Double` now ignores leading
and trailing whitespace. Previously only leading whitespace was ignored.
+ RTS functions `openFile`, `do_popen`, and `ARGV` are now properly encoded using UTF-8 on Windows.
* `record` syntax now allows updating fields, including nested fields,
by applying a function using the `$=` operator. For example:
```idris
record Score where
constructor MkScore
correct : Nat
attempted : Nat
record GameState where
constructor MkGameState
score : Score
difficulty : Nat
correct : GameState -> GameState
correct st = record { score->correct $= (+1),
score->attempted $= (+1) } st
```
* Implicit parameter to interfaces are now allowed. For example:
```idris
interface Shows (ts : Vect k Type) where
shows : HVect ts -> Vect k String
```
In this interface, `k` is an implicit parameter, but previously needed to
be explicit
* The File Effect has been updated to take into account changes in
`Prelude.File` and to provide a 'better' API.
* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.
* `divBN` and `modBN` now can only be used for unsigned numbers.
* `return`, which has been an alias for `pure` for many releases, is now deprecated.
* Replace instance with implementation:
+ `InstanceN` is deprecated, use `ImplementationN` instead.
+ `InstanceCtorN` is deprecated, use `ImplementationCtorN` instead.
+ `addInstance` is deprecated, use `addImplementation` instead.
+ `%instance` keyword is deprecated, use `%implementation` instead.
* Idris packages are now installed within a sub-directory `libs` of Idris' data directory, before they were installed in the directory's root.
* Idris' documentation system now displays the documentation for auto
implicits in the output of `:doc`. This is tested for in `docs005`.
* New command line flag `--info` that displays information about the installation.
* New command line flag `--sourcepath <dir>` that allows adding directories to the source search path.
* Allow 'installation' of a package's IdrisDoc documentation into a central location. The default location is the subdirectory `docs` of Idris' data directory.
* New flag `--installdoc <ipkg>` provided to install documentation
* New flag `--docdir` provided to show default documentation installation location.
* New environment variable `IDRIS_DOC_PATH` to allow specification of an alternative installation path for documentation.
* Semantic meaning behind several environment variables has been clarified in documentation and code. See compilation section of the reference manual for more details.
* Interface parameter constraints are now printed in the output of `:doc`. This
is tested for in `docs006`.
* New, faster, better, implementation of the coverage checker
* The test suite now uses [tasty-golden](https://hackage.haskell.org/package/tasty-golden). New tests must be registered in `test/TestData.hs`, as explained in the relevant `README.md`.
* Added OSX and Windows continous integration with Travis and Appveyor.
* The :e command can now handle an $EDITOR with arguments in it, like "emacs -nw"
PreviousNext