mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 21:37:48 +03:00
Version 0.5.0 (#1931)
* Update version numbers and bootstrap scheme * Use wall clock time for search timeouts That was always the intention in any case, rather than the process time.
This commit is contained in:
Edwin Brady
GitHub
parent
22c12046df
commit
ada3eb4449
@ -1,6 +1,6 @@
|
|||||||
# Changelog
|
# Changelog
|
||||||
|
|
||||||
## [Next version]
|
## v0.5.0
|
||||||
|
|
||||||
### Language changes
|
### Language changes
|
||||||
|
|
||||||
@ -11,11 +11,11 @@
|
|||||||
`where` clauses
|
`where` clauses
|
||||||
* The syntax for Name reflection has changed, and now requires a single brace
|
* The syntax for Name reflection has changed, and now requires a single brace
|
||||||
instead of a double brace, e.g. `` `{x} ``
|
instead of a double brace, e.g. `` `{x} ``
|
||||||
* Raw string literals allows to write string while customising the escape
|
* Raw string literals allows writing string while customising the escape
|
||||||
sequence. Start a string with `#"` in order to change the escape characters
|
sequence. Start a string with `#"` in order to change the escape characters
|
||||||
to `\#`, close the string with `"#`. Remains compatible with multiline
|
to `\#`, close the string with `"#`. Remains compatible with multiline
|
||||||
string literals.
|
string literals.
|
||||||
* Interpolated strings allows to insert expressions within string literals
|
* Interpolated strings allows inserting expressions within string literals
|
||||||
and avoid writing concatenation explicitly. Escape a left curly brace `\{`
|
and avoid writing concatenation explicitly. Escape a left curly brace `\{`
|
||||||
to start an interpolation slice and close it with a right curly brace `}` to
|
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
|
resume writing the string literal. The enclosed expression must be of type
|
||||||
@ -59,7 +59,7 @@ filter p (x :: xs) with (p x)
|
|||||||
all libraries you plan to link with an incremental build.
|
all libraries you plan to link with an incremental build.
|
||||||
- Note also that this is experimental and not yet well tested!
|
- Note also that this is experimental and not yet well tested!
|
||||||
* The type checker now tries a lot harder to avoid reducing expressions where
|
* 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
|
it is not needed. This can give a huge performance improvement in programs
|
||||||
that potentially do a lot of compile time evaluation. However, sometimes
|
that potentially do a lot of compile time evaluation. However, sometimes
|
||||||
reducing expressions can help in totality and quantity checking, so this may
|
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,
|
cause some programs not to type check which previously did - in these cases,
|
||||||
|
|||||||
2
Makefile
2
Makefile
@ -13,7 +13,7 @@ TARGET = ${TARGETDIR}/${NAME}
|
|||||||
IDRIS2_CG ?= chez
|
IDRIS2_CG ?= chez
|
||||||
|
|
||||||
MAJOR=0
|
MAJOR=0
|
||||||
MINOR=4
|
MINOR=5
|
||||||
PATCH=0
|
PATCH=0
|
||||||
|
|
||||||
GIT_SHA1=
|
GIT_SHA1=
|
||||||
|
|||||||
9345
bootstrap/idris2_app/idris2.rkt
generated
9345
bootstrap/idris2_app/idris2.rkt
generated
File diff suppressed because one or more lines are too long
9301
bootstrap/idris2_app/idris2.ss
generated
9301
bootstrap/idris2_app/idris2.ss
generated
File diff suppressed because one or more lines are too long
@ -1,7 +1,7 @@
|
|||||||
$ idris2 hello.idr
|
$ idris2 hello.idr
|
||||||
____ __ _ ___
|
____ __ _ ___
|
||||||
/ _/___/ /____(_)____ |__ \
|
/ _/___/ /____(_)____ |__ \
|
||||||
/ // __ / ___/ / ___/ __/ / Version 0.4.0
|
/ // __ / ___/ / ___/ __/ / Version 0.5.0
|
||||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||||
|
|
||||||
|
|||||||
@ -1,7 +1,7 @@
|
|||||||
$ idris2 interp.idr
|
$ idris2 interp.idr
|
||||||
____ __ _ ___
|
____ __ _ ___
|
||||||
/ _/___/ /____(_)____ |__ \
|
/ _/___/ /____(_)____ |__ \
|
||||||
/ // __ / ___/ / ___/ __/ / Version 0.4.0
|
/ // __ / ___/ / ___/ __/ / Version 0.5.0
|
||||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||||
|
|
||||||
|
|||||||
@ -1,7 +1,7 @@
|
|||||||
$ idris2
|
$ idris2
|
||||||
____ __ _ ___
|
____ __ _ ___
|
||||||
/ _/___/ /____(_)____ |__ \
|
/ _/___/ /____(_)____ |__ \
|
||||||
/ // __ / ___/ / ___/ __/ / Version 0.4.0
|
/ // __ / ___/ / ___/ __/ / Version 0.5.0
|
||||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||||
|
|
||||||
|
|||||||
@ -11,7 +11,7 @@
|
|||||||
|
|
||||||
outputs = { self, nixpkgs, nixpkgs-chez-racket, flake-utils, idris-emacs-src }:
|
outputs = { self, nixpkgs, nixpkgs-chez-racket, flake-utils, idris-emacs-src }:
|
||||||
let
|
let
|
||||||
idris2-version = "0.4.0";
|
idris2-version = "0.5.0";
|
||||||
lib = import ./nix/lib.nix;
|
lib = import ./nix/lib.nix;
|
||||||
sys-agnostic = rec {
|
sys-agnostic = rec {
|
||||||
templates.pkg = {
|
templates.pkg = {
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
package idris2
|
package idris2
|
||||||
version = 0.4.0
|
version = 0.5.0
|
||||||
|
|
||||||
modules =
|
modules =
|
||||||
Algebra,
|
Algebra,
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
package base
|
package base
|
||||||
version = 0.4.0
|
version = 0.5.0
|
||||||
|
|
||||||
opts = "--ignore-missing-ipkg -Wno-shadowing"
|
opts = "--ignore-missing-ipkg -Wno-shadowing"
|
||||||
|
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
package contrib
|
package contrib
|
||||||
version = 0.4.0
|
version = 0.5.0
|
||||||
|
|
||||||
opts = "--ignore-missing-ipkg -Wno-shadowing"
|
opts = "--ignore-missing-ipkg -Wno-shadowing"
|
||||||
|
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
package network
|
package network
|
||||||
version = 0.4.0
|
version = 0.5.0
|
||||||
|
|
||||||
opts = "--ignore-missing-ipkg -p contrib"
|
opts = "--ignore-missing-ipkg -p contrib"
|
||||||
|
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
package prelude
|
package prelude
|
||||||
version = 0.4.0
|
version = 0.5.0
|
||||||
|
|
||||||
opts = "--ignore-missing-ipkg --no-prelude"
|
opts = "--ignore-missing-ipkg --no-prelude"
|
||||||
|
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
package test
|
package test
|
||||||
version = 0.4.0
|
version = 0.5.0
|
||||||
|
|
||||||
depends = contrib
|
depends = contrib
|
||||||
|
|
||||||
|
|||||||
@ -2231,7 +2231,7 @@ recordWarning w
|
|||||||
export
|
export
|
||||||
getTime : Core Integer
|
getTime : Core Integer
|
||||||
getTime
|
getTime
|
||||||
= do clock <- coreLift (clockTime Process)
|
= do clock <- coreLift (clockTime Monotonic)
|
||||||
pure (seconds clock * nano + nanoseconds clock)
|
pure (seconds clock * nano + nanoseconds clock)
|
||||||
where
|
where
|
||||||
nano : Integer
|
nano : Integer
|
||||||
|
|||||||
@ -1,3 +1,3 @@
|
|||||||
1/1: Building Main (Main.idr)
|
1/1: Building Main (Main.idr)
|
||||||
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.4.0/testpkg-0
|
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.5.0/testpkg-0
|
||||||
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.4.0/testpkg-0
|
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.5.0/testpkg-0
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user