Skip to content

Commit ada3eb4

Browse files
authored
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.
1 parent 22c1204 commit ada3eb4

File tree

16 files changed

+10138
-8440
lines changed

16 files changed

+10138
-8440
lines changed

Diff for: CHANGELOG.md

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# Changelog
22

3-
## [Next version]
3+
## v0.5.0
44

55
### Language changes
66

@@ -11,11 +11,11 @@
1111
`where` clauses
1212
* The syntax for Name reflection has changed, and now requires a single brace
1313
instead of a double brace, e.g. `` `{x} ``
14-
* Raw string literals allows to write string while customising the escape
14+
* Raw string literals allows writing string while customising the escape
1515
sequence. Start a string with `#"` in order to change the escape characters
1616
to `\#`, close the string with `"#`. Remains compatible with multiline
1717
string literals.
18-
* Interpolated strings allows to insert expressions within string literals
18+
* Interpolated strings allows inserting expressions within string literals
1919
and avoid writing concatenation explicitly. Escape a left curly brace `\{`
2020
to start an interpolation slice and close it with a right curly brace `}` to
2121
resume writing the string literal. The enclosed expression must be of type
@@ -59,7 +59,7 @@ filter p (x :: xs) with (p x)
5959
all libraries you plan to link with an incremental build.
6060
- Note also that this is experimental and not yet well tested!
6161
* The type checker now tries a lot harder to avoid reducing expressions where
62-
it is not needed. This gives a huge performance improvement in programs
62+
it is not needed. This can give a huge performance improvement in programs
6363
that potentially do a lot of compile time evaluation. However, sometimes
6464
reducing expressions can help in totality and quantity checking, so this may
6565
cause some programs not to type check which previously did - in these cases,

Diff for: Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ TARGET = ${TARGETDIR}/${NAME}
1313
IDRIS2_CG ?= chez
1414

1515
MAJOR=0
16-
MINOR=4
16+
MINOR=5
1717
PATCH=0
1818

1919
GIT_SHA1=

Diff for: bootstrap/idris2_app/idris2.rkt

+5,071-4,220
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Diff for: bootstrap/idris2_app/idris2.ss

+5,049-4,202
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Diff for: docs/source/listing/idris-prompt-helloworld.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
$ idris2 hello.idr
22
____ __ _ ___
33
/ _/___/ /____(_)____ |__ \
4-
/ // __ / ___/ / ___/ __/ / Version 0.4.0
4+
/ // __ / ___/ / ___/ __/ / Version 0.5.0
55
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
66
/___/\__,_/_/ /_/____/ /____/ Type :? for help
77

Diff for: docs/source/listing/idris-prompt-interp.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
$ idris2 interp.idr
22
____ __ _ ___
33
/ _/___/ /____(_)____ |__ \
4-
/ // __ / ___/ / ___/ __/ / Version 0.4.0
4+
/ // __ / ___/ / ___/ __/ / Version 0.5.0
55
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
66
/___/\__,_/_/ /_/____/ /____/ Type :? for help
77

Diff for: docs/source/listing/idris-prompt-start.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
$ idris2
22
____ __ _ ___
33
/ _/___/ /____(_)____ |__ \
4-
/ // __ / ___/ / ___/ __/ / Version 0.4.0
4+
/ // __ / ___/ / ___/ __/ / Version 0.5.0
55
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
66
/___/\__,_/_/ /_/____/ /____/ Type :? for help
77

Diff for: flake.nix

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111

1212
outputs = { self, nixpkgs, nixpkgs-chez-racket, flake-utils, idris-emacs-src }:
1313
let
14-
idris2-version = "0.4.0";
14+
idris2-version = "0.5.0";
1515
lib = import ./nix/lib.nix;
1616
sys-agnostic = rec {
1717
templates.pkg = {

Diff for: idris2api.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package idris2
2-
version = 0.4.0
2+
version = 0.5.0
33

44
modules =
55
Algebra,

Diff for: libs/base/base.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package base
2-
version = 0.4.0
2+
version = 0.5.0
33

44
opts = "--ignore-missing-ipkg -Wno-shadowing"
55

Diff for: libs/contrib/contrib.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package contrib
2-
version = 0.4.0
2+
version = 0.5.0
33

44
opts = "--ignore-missing-ipkg -Wno-shadowing"
55

Diff for: libs/network/network.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package network
2-
version = 0.4.0
2+
version = 0.5.0
33

44
opts = "--ignore-missing-ipkg -p contrib"
55

Diff for: libs/prelude/prelude.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package prelude
2-
version = 0.4.0
2+
version = 0.5.0
33

44
opts = "--ignore-missing-ipkg --no-prelude"
55

Diff for: libs/test/test.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package test
2-
version = 0.4.0
2+
version = 0.5.0
33

44
depends = contrib
55

Diff for: src/Core/Context.idr

+1-1
Original file line numberDiff line numberDiff line change
@@ -2231,7 +2231,7 @@ recordWarning w
22312231
export
22322232
getTime : Core Integer
22332233
getTime
2234-
= do clock <- coreLift (clockTime Process)
2234+
= do clock <- coreLift (clockTime Monotonic)
22352235
pure (seconds clock * nano + nanoseconds clock)
22362236
where
22372237
nano : Integer

Diff for: tests/idris2/pkg010/expected.in

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
1/1: Building Main (Main.idr)
2-
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.4.0/testpkg-0
3-
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.4.0/testpkg-0
2+
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.5.0/testpkg-0
3+
Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.5.0/testpkg-0

0 commit comments

Comments
 (0)