# Changelog ## [Next version] ### Language changes * Missing methods in implementations now give a compile time error. This was always the intended behaviour, but until now had not been implemented! * Records now work in `parameters` blocks and `where` clauses. * Implementations of interfaces now work in `parameters` blocks and `where` clauses * The syntax for Name reflection has changed, and now requires a single brace instead of a double brace, e.g. `` `{x} `` * Raw string literals allows to write string while customising the escape sequence. Start a string with `#"` in order to change the escape characters to `\#`, close the string with `"#`. Remains compatible with multiline string literals. * Interpolated strings allows to insert expressions within string literals and avoid writing concatenation explicitly. Escape a left curly brace `\{` to start an interpolation slice and close it with a right curly brace `}` to resume writing the string literal. The enclosed expression must be of type `String`. Interpolated strings are compatible with raw strings (the slices need to be escaped with `\#{` instead) and multiline strings. * We now support ellipses (written `_`) on the left hand side of a `with` clause. Ellipses are substituted for by the left hand side of the parent clause i.e. ```idris filter : (p : a -> Bool) -> List a -> List a filter p [] = [] filter p (x :: xs) with (p x) _ | True = x :: filter p xs _ | False = filter p xs ``` means ```idris filter : (p : a -> Bool) -> List a -> List a filter p [] = [] filter p (x :: xs) with (p x) filter p (x :: xs) | True = x :: filter p xs filter p (x :: xs) | False = filter p xs ``` ### Compiler changes * Added incremental compilation, using either the `--inc` flag or the `IDRIS2_INC_CGS` environment variable, which compiles modules incrementally. In incremental mode, the final build step is much faster than in whole program mode (the default), at the cost of runtime performance being about half as good. The `--whole-program` flag overrides incremental compilation, and reverts to whole program compilation. Incremental compilation is currently supported only by the Chez Scheme back end. This is currently supported only on Unix-like platforms (not yet Windows) - Note that you must set `IDRIS2_INC_CGS` when building and installing all libraries you plan to link with an incremental build. - Note also that this is experimental and not yet well tested! * The type checker now tries a lot harder to avoid reducing expressions where it is not needed. This gives a huge performance improvement in programs that potentially do a lot of compile time evaluation. However, sometimes reducing expressions can help in totality and quantity checking, so this may cause some programs not to type check which previously did - in these cases, you will need to give the reduced expressions explicitly. ### REPL/CLI/IDE mode changes * Added `--list-packages` CLI option. * Added `--total` CLI option. ### Library changes #### Prelude Changed - Removed `Data.Strings`. Use `Data.String` instead. #### System.Concurrency * Reimplement the `Channels` primitive in the Chez-Scheme backend since it had some non-deterministic properties (see issue [#1552](https://github.com/idris-lang/idris2/issues/1552)). NOTE: Due to complications with race-conditions, Chez not having channels built in, etc, the reimplementation changes the semantics slightly: `channelPut` no longer blocks until the value has been received under the `chez` backend, but instead only blocks if there is already a value in the channel that has not been received. With thanks to Alain Zscheile (@zseri) for help with understanding condition variables, and figuring out where the problems were and how to solve them. #### Control.Relation, Control.Order * The old system of interfaces for defining order relations (to say, for instance, that LTE is a partial order) is replaced with a new system of interfaces. These interfaces defines properties of binary relations (functions of type `ty -> ty -> Type`), and orders are defined simply as bundles of these properties. ### Installation changes * Added a new makefile target to install Idris 2 library documentation. After `make install`, type `make install-libdocs` to install it. After that, the index file can be found here: ``idris2 --libdir`/docs/index.html`.`` ## v0.4.0 ### Syntax changes * Desugar non-binding sequencing in do blocks to (`>>`) ([#1095](https://github.com/idris-lang/idris2/pull/1095)) * Multiline Strings with `"""` as delimiters ([#1097](https://github.com/idris-lang/idris2/pull/1097)) * Force strict indentation after usage of `with` keyword ([#1107](https://github.com/idris-lang/idris2/pull/1107)) * The syntax for parameter blocks has been updated. It now allows to declare implicit parameters and give multiplicities for parameters. The old syntax is still available for compatibility purposes but will be removed in the future. * Add support for SnocList syntax: `[< 1, 2, 3]` desugars into `Lin :< 1 :< 2 :< 3` and their semantic highlighting. * Underscores can be used as visual separators for digit grouping purposes in integer literals: `10_000_000` is equivalent to `10000000` and `0b1111_0101_0000` is equivalent to `0b111101010000`. This can aid readability of long literals, or literals whose value should clearly separate into parts, such as bytes or words in hexadecimal notation. ### Compiler changes * Added more optimisations and transformations, particularly on case blocks, list-shaped types, and enumerations, so generated code will often be slightly faster. * Added `--profile` flag, which generates profile data if supported by a back end. Currently supported by the Chez and Racket back ends. * New `%builtin` pragma for compiling user defined natural numbers to primitive `Integer`s (see the [docs](https://idris2.readthedocs.io/en/latest/reference/builtins.html)) * The `version` field in `.ipkg` files is now used. Packages are installed into a directory which includes its version number, and dependencies can have version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version constraints. Version numbers must be in the form of integers, separated by dots (e.g. `1.0`, `0.3.0`, `3.1.4.1.5` etc) * Idris now looks in the current working directory, under a subdirectory `depends` for local installations of packages before looking globally. * Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to look for packages. * Added compiler warnings flags (`-W` prefix): - `-Wno-shadowing`: disable shadowing warnings. - `-Werror`: treat warnings as errors. * Experimental flag (`-Xcheck-hashes`) to check hashes instead of filesystem times to determine if files should be recompiled. Should help with CI/CD caching. ### REPL/IDE mode changes * Added `:search` command, which searches for functions by type * `:load`/`:l` and `:cd` commands now only accept paths surrounded by double quotes * Added a timeout to "generate definition" and "proof search" commands, defaulting to 1 second (1000 milliseconds) and configurable with `%search_timeout