mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-19 09:17:29 +03:00
[doc] Add missing entries and refactor CHANGELOG.md
(#1566)
This commit is contained in:
parent
68c6fe222c
commit
657699a866
228
CHANGELOG.md
228
CHANGELOG.md
@ -1,71 +1,156 @@
|
|||||||
Changes since Idris 2 v0.3.0
|
# Changelog
|
||||||
============================
|
|
||||||
|
|
||||||
Library changes:
|
## Unreleased (idris2-next)
|
||||||
* Introduced `test` package.
|
|
||||||
|
|
||||||
- Moved `tests/Lib.idr` into new `test` package as `Test/Golden.idr`.
|
### Syntax changes
|
||||||
|
|
||||||
- Removed `contrib/Test/Golden.idr` which duplicated the test framework now in the `test` package.
|
|
||||||
* Added `System.Console.GetOpt`,a library for specifying and parsing
|
|
||||||
command line options, to `contrib`.
|
|
||||||
* Monad transformers in `Control.Monad` where restructured
|
|
||||||
and several new transformer types where added.
|
|
||||||
* `Data.Colist` and `Data.Colist1` were added to `base`.
|
|
||||||
* Add `Data.SnocList` to base and `data SnocList` to `Prelude.Types`.
|
|
||||||
* `Data.Bits`, an interface for bitwise operations, was added to `base`.
|
|
||||||
* Interfaces `Bifoldable` and `Bitraversable` were added to the `prelude`.
|
|
||||||
* Interface `Data.Contravariant` for contravariant functors was added
|
|
||||||
to base.
|
|
||||||
* `Control.Applicative.Const` was added to `base`.
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
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
|
* The syntax for parameter blocks has been updated. It now allows to declare
|
||||||
implicit parameters and give multiplicities for parameters. The old syntax
|
implicit parameters and give multiplicities for parameters. The old syntax is
|
||||||
is still available for compatibility purposes but will be removed in the
|
still available for compatibility purposes but will be removed in the future.
|
||||||
future.
|
* Add support for SnocList syntax: `[< 1, 2, 3]` desugars into `Lin :< 1 :< 2 :<
|
||||||
* Add support for SnocList syntax: `[< 1, 2, 3]` desugars into `Lin :< 1 :< 2 :< 3`
|
3` and their semantic highlighting.
|
||||||
and their semantic highlighting.
|
|
||||||
* Underscores can be used as visual separators for digit grouping purposes in
|
* Underscores can be used as visual separators for digit grouping purposes in
|
||||||
integer literals: `10_000_000` is equivalent to `10000000` and
|
integer literals: `10_000_000` is equivalent to `10000000` and
|
||||||
`0b1111_0101_0000` is equivalent to `0b111101010000`. This can aid
|
`0b1111_0101_0000` is equivalent to `0b111101010000`. This can aid readability
|
||||||
readability of long literals, or literals whose value should clearly
|
of long literals, or literals whose value should clearly separate into parts,
|
||||||
separate into parts, such as bytes or words in hexadecimal notation.
|
such as bytes or words in hexadecimal notation.
|
||||||
|
|
||||||
Compiler changes:
|
### Compiler changes
|
||||||
|
|
||||||
* Added more optimisations and transformations, particularly on case blocks,
|
* Added more optimisations and transformations, particularly on case blocks,
|
||||||
list-shaped types, and enumerations, so generated code will often be slightly
|
list-shaped types, and enumerations, so generated code will often be slightly
|
||||||
faster.
|
faster.
|
||||||
* Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in
|
|
||||||
order to not block the Racket runtime when `sleep` is called.
|
|
||||||
* Added `--profile` flag, which generates profile data if supported by a back
|
* Added `--profile` flag, which generates profile data if supported by a back
|
||||||
end. Currently supported by the Chez and Racket back ends.
|
end. Currently supported by the Chez and Racket back ends.
|
||||||
* Javascript codegens now use `Number` to represent up to 32 bit precision
|
* New `%builtin` pragma for compiling user defined natural numbers to primitive
|
||||||
signed and unsigned integers. `Int32` still goes via `BigInt` for
|
`Integer`s (see the
|
||||||
multiplication to avoid precision issues when getting results larger
|
[docs](https://idris2.readthedocs.io/en/latest/reference/builtins.html))
|
||||||
than `Number.MAX_SAFE_INTEGER`. `Bits32` goes via `BigInt` for
|
* The `version` field in `.ipkg` files is now used. Packages are installed into
|
||||||
multiplication for the same reason as well as for all bitops, since `Number`
|
a directory which includes its version number, and dependencies can have
|
||||||
uses signed 32 bit integers for those.
|
version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version
|
||||||
* New code generator: `chez-sep`. This code generator produces many Chez Scheme
|
constraints. Version numbers must be in the form of integers, separated by
|
||||||
files and compiles them separately instead of producing one huge Scheme
|
dots (e.g. `1.0`, `0.3.0`, `3.1.4.1.5` etc)
|
||||||
program. This significantly reduces the amount of memory needed to build
|
* Idris now looks in the current working directory, under a subdirectory
|
||||||
large programs. Since this backend will skip calling the Chez compiler on
|
`depends` for local installations of packages before looking globally.
|
||||||
modules that haven't changed, it also leads to shorter compilation times in
|
* Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to
|
||||||
large codebases where only some files have changed -- for example when
|
look for packages.
|
||||||
developing Idris2 code generators. The codegen has a large parallelisation
|
* Added compiler warnings flags (`-W` prefix):
|
||||||
potential but at the moment, it is significantly slower for a full rebuild of
|
- `-Wno-shadowing`: disable shadowing warnings.
|
||||||
a large code base (the code generation stage takes about 3x longer).
|
- `-Werror`: treat warnings as errors.
|
||||||
* New `%builtin` pragma for compiling user defined natural numbers to
|
* Experimental flag (`-Xcheck-hashes`) to check hashes instead of filesystem
|
||||||
primitive `Integer`s (see the [docs](https://idris2.readthedocs.io/en/latest/reference/builtins.html))
|
times to determine if files should be recompiled. Should help with CI/CD
|
||||||
|
caching.
|
||||||
|
|
||||||
API changes:
|
### 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
|
||||||
|
|
||||||
|
### Library Changes
|
||||||
|
|
||||||
|
#### Prelude
|
||||||
|
|
||||||
|
Added
|
||||||
|
|
||||||
|
- `Bifoldable` and `Bitraversable` interfaces.
|
||||||
|
- `Foldable` add `foldlM`, `foldMap`, and `toList`.
|
||||||
|
- `Monad` interface `>=>`, `<=<` (Kleisli Arrows), and flipped bind (`=<<`).
|
||||||
|
- `Pair` Applicative and Monad implementations.
|
||||||
|
- `SnocList` datatype (fliped cons of a linked list).
|
||||||
|
- `(.:)` function "blackbird operator" (Composition of a two-argument function
|
||||||
|
with a single-argument one.)
|
||||||
|
- `on` function (Eg, ```((+) `on` f) x y = f x + f y```)
|
||||||
|
|
||||||
|
Changed
|
||||||
|
|
||||||
|
- `===`, `~=~`, and `<+>` operator precedence
|
||||||
|
- Exctracted `Cast` interface and implementations from `Prelude.Types` to
|
||||||
|
`Prelude.Cast`
|
||||||
|
- Renamed `Data.Strings` to `Data.String`
|
||||||
|
|
||||||
|
Hidden
|
||||||
|
|
||||||
|
- `countFrom`
|
||||||
|
|
||||||
|
#### Base
|
||||||
|
|
||||||
|
Added
|
||||||
|
|
||||||
|
- `Control.Applicative.Const`.
|
||||||
|
- New `Control.Monad` Monad Transformers types.
|
||||||
|
- `Data.Bits`, an interface for bitwise operations.
|
||||||
|
- `Data.Colist` and `Data.Colist1`.
|
||||||
|
- `Data.Contravariant` interface for contravariant functors.
|
||||||
|
- `Data.List` `unzip` function.
|
||||||
|
- `Data.List1` `zip*` and `unzip*` functions.
|
||||||
|
- `Data.SnocList`.
|
||||||
|
- `Data.Stream` `unzipWith` and `unzipWith3` fuctions.
|
||||||
|
- `Data.Vect` `unzipWith` and `unzipWith3` functions.
|
||||||
|
- `System.File` `withFile` and total read functions.
|
||||||
|
|
||||||
|
Changed:
|
||||||
|
|
||||||
|
- Restructured Monad Transformers in `Control.Monad`
|
||||||
|
- `zip` precedence
|
||||||
|
|
||||||
|
#### Contrib
|
||||||
|
|
||||||
|
Added
|
||||||
|
|
||||||
|
- `Control.Validation`, a library for dependent types input validation.
|
||||||
|
- `System.Console.GetOpt`, a library for specifying and parsing command line
|
||||||
|
options.
|
||||||
|
|
||||||
|
#### New test package
|
||||||
|
|
||||||
|
- Moved `tests/Lib.idr` to package as `Test/Golden.idr`.
|
||||||
|
- Removed `contrib/Test/Golden.idr` which duplicated the test framework now in
|
||||||
|
the `test` package.
|
||||||
|
|
||||||
|
### Codegen changes
|
||||||
|
|
||||||
|
#### Racket
|
||||||
|
|
||||||
|
* Now always uses `blodwen-sleep` instead of `idris2_sleep` in order to not
|
||||||
|
block the Racket runtime when `sleep` is called.
|
||||||
|
* Redid condition variables in the Racket codegen based on page 5 of the
|
||||||
|
Microsoft [Implementing CVs paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2004/12/ImplementingCVs.pdf).
|
||||||
|
Previously, they were based on an implementation using semaphores and
|
||||||
|
asynchronous channels, which worked apart from `broadcast`. The rework fixes
|
||||||
|
`broadcast` at the cost of losing `wait-timeout` due to increased complexity
|
||||||
|
of their internals and interactions between their associated functions.
|
||||||
|
|
||||||
|
#### Javascript
|
||||||
|
|
||||||
|
* Now use `Number` to represent up to 32 bit precision signed and unsigned
|
||||||
|
integers. `Int32` still goes via `BigInt` for multiplication to avoid
|
||||||
|
precision issues when getting results larger than `Number.MAX_SAFE_INTEGER`.
|
||||||
|
`Bits32` goes via `BigInt` for multiplication for the same reason as well as
|
||||||
|
for all bitops, since `Number` uses signed 32 bit integers for those.
|
||||||
|
* Now use `Number` instead of `BigInt` to represent up to 32 bit fixed precision
|
||||||
|
signed and unsigned integers. This should make interop with the FFI more
|
||||||
|
straight forward, and might also improve performance.
|
||||||
|
|
||||||
|
#### New chez-sep
|
||||||
|
|
||||||
|
* This code generator produces many Chez Scheme files and compiles them
|
||||||
|
separately instead of producing one huge Scheme program. This significantly
|
||||||
|
reduces the amount of memory needed to build large programs. Since this
|
||||||
|
backend will skip calling the Chez compiler on modules that haven't changed,
|
||||||
|
it also leads to shorter compilation times in large codebases where only some
|
||||||
|
files have changed -- for example when developing Idris2 code generators. The
|
||||||
|
codegen has a large parallelisation potential but at the moment, it is
|
||||||
|
significantly slower for a full rebuild of a large code base (the code
|
||||||
|
generation stage takes about 3x longer).
|
||||||
|
|
||||||
|
### API changes
|
||||||
|
|
||||||
* The API now exposes `Compiler.Separate.getCompilationUnits`, which
|
* The API now exposes `Compiler.Separate.getCompilationUnits`, which
|
||||||
can be used for separate code generation by any backend.
|
can be used for separate code generation by any backend.
|
||||||
@ -78,36 +163,14 @@ API changes:
|
|||||||
* A new pragma `%doubleLit` to support overloaded floating point literals
|
* A new pragma `%doubleLit` to support overloaded floating point literals
|
||||||
was added.
|
was added.
|
||||||
|
|
||||||
Library changes:
|
### Other changes
|
||||||
|
|
||||||
* Redid condition variables in the Racket codegen based on page 5 of the
|
|
||||||
Microsoft [Implementing CVs paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2004/12/ImplementingCVs.pdf).
|
|
||||||
Previously, they were based on an implementation using semaphores and
|
|
||||||
asynchronous channels, which worked apart from `broadcast`. The rework fixes
|
|
||||||
`broadcast` at the cost of losing `wait-timeout` due to increased complexity
|
|
||||||
of their internals and interactions between their associated functions.
|
|
||||||
* The JS backends now use `Number` instead of `BigInt` to represent up to 32 bit fixed
|
|
||||||
precision signed and unsigned integers. This should make interop
|
|
||||||
with the FFI more straight forward, and might also improve performance.
|
|
||||||
|
|
||||||
Other changes:
|
|
||||||
|
|
||||||
* 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.
|
|
||||||
* Support for auto-completion in bash-like shells was added.
|
* Support for auto-completion in bash-like shells was added.
|
||||||
* Fixed case-splitting to respect any indentation there may be in the term being
|
* Fixed case-splitting to respect any indentation there may be in the term being
|
||||||
case-split and the surrounding symbols, instead of filtering out the
|
case-split and the surrounding symbols, instead of filtering out the
|
||||||
whitespace and putting it back as indentation.
|
whitespace and putting it back as indentation.
|
||||||
|
|
||||||
Changes since Idris 2 v0.2.1
|
## v0.3.0
|
||||||
----------------------------
|
|
||||||
|
|
||||||
Library changes:
|
Library changes:
|
||||||
|
|
||||||
@ -216,8 +279,7 @@ REPL/IDE mode changes:
|
|||||||
* Added `:consolewidth (auto|n)` option for printing margins. Mirrors the
|
* Added `:consolewidth (auto|n)` option for printing margins. Mirrors the
|
||||||
command line option.
|
command line option.
|
||||||
|
|
||||||
Changes since Idris 2 v0.2.0
|
## v0.2.1
|
||||||
----------------------------
|
|
||||||
|
|
||||||
Language changes:
|
Language changes:
|
||||||
|
|
||||||
@ -293,8 +355,7 @@ REPL/IDE mode changes:
|
|||||||
* Improved program search to allow deconstructing intermediate values, and in
|
* Improved program search to allow deconstructing intermediate values, and in
|
||||||
simple cases, the result of recursive calls.
|
simple cases, the result of recursive calls.
|
||||||
|
|
||||||
Changes since Idris 2 v0.1.0
|
## v0.2.0
|
||||||
----------------------------
|
|
||||||
|
|
||||||
The implementation is now self-hosted. To initialise the build, either use
|
The implementation is now self-hosted. To initialise the build, either use
|
||||||
the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot)
|
the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot)
|
||||||
@ -351,8 +412,7 @@ Other improvements:
|
|||||||
* Extend Idris2's literate mode to support reading Markdown and OrgMode files.
|
* Extend Idris2's literate mode to support reading Markdown and OrgMode files.
|
||||||
For more details see: ["literate" in the user manual](https://idris2.readthedocs.io/en/latest/reference/literate.html).
|
For more details see: ["literate" in the user manual](https://idris2.readthedocs.io/en/latest/reference/literate.html).
|
||||||
|
|
||||||
Changes since Idris 1
|
## Changes since Idris 1
|
||||||
---------------------
|
|
||||||
|
|
||||||
Everything :). For full details, see:
|
Everything :). For full details, see:
|
||||||
[updates](https://idris2.readthedocs.io/en/latest/updates/updates.html)
|
[updates](https://idris2.readthedocs.io/en/latest/updates/updates.html)
|
||||||
|
Loading…
Reference in New Issue
Block a user