mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-26 04:29:53 +03:00
Update release notes for 2.11 (#1121)
This commit is contained in:
parent
e546dff60a
commit
b64e07526d
41
CHANGES.md
41
CHANGES.md
@ -1,4 +1,14 @@
|
|||||||
# NEXT
|
# 2.11.0
|
||||||
|
|
||||||
|
## Language changes
|
||||||
|
|
||||||
|
* The `newtype` construct, which has existed in the interpreter in an
|
||||||
|
incomplete and undocumented form for quite a while, is now fullly
|
||||||
|
supported. The construct is documented in section 1.22 of [Programming
|
||||||
|
Cryptol](https://cryptol.net/files/ProgrammingCryptol.pdf). Note,
|
||||||
|
however, that the `cryptol-remote-api` RPC server currently does not
|
||||||
|
include full support for referring to `newtype` names, though it can
|
||||||
|
work with implementations that use `newtype` internally.
|
||||||
|
|
||||||
## New features
|
## New features
|
||||||
|
|
||||||
@ -9,6 +19,35 @@
|
|||||||
runtime overhead, but may be disabled using the `--no-call-stacks`
|
runtime overhead, but may be disabled using the `--no-call-stacks`
|
||||||
command-line option.
|
command-line option.
|
||||||
|
|
||||||
|
* The `:exhaust` command now works for floating-point types and the
|
||||||
|
`:check` command now uses more representative sampling of
|
||||||
|
floating-point input values to test.
|
||||||
|
|
||||||
|
* The `cryptol-remote-api` RPC server now has methods corresponding to
|
||||||
|
the `:prove` and `:sat` commands in the REPL.
|
||||||
|
|
||||||
|
* The `cryptol-eval-server` executable is a new, stateless server
|
||||||
|
providing a subset of the functionality of `cryptol-remote-api`
|
||||||
|
dedicated entirely to invoking Cryptol functions on concrete inputs.
|
||||||
|
|
||||||
|
## Internal changes
|
||||||
|
|
||||||
|
* A single running instance of the SMT solver used for type checking
|
||||||
|
(Z3) is now used to check a larger number of type correctness queries.
|
||||||
|
This means that fewer solver instances are invoked, and type checking
|
||||||
|
should generally be faster.
|
||||||
|
|
||||||
|
* The Cryptol interpreter now builds against `libBF` version 0.6, which
|
||||||
|
fixes a few bugs in the evaluation of floating-point operations.
|
||||||
|
|
||||||
|
## Bug fixes
|
||||||
|
|
||||||
|
* Closed issues #118, #398, #426, #470, #491, #567, #594, #639, #656,
|
||||||
|
#698, #743, #810, #858, #870, #905, #915, #917, #962, #973, #975,
|
||||||
|
#980, #984, #986, #990, #996, #997, #1002, #1006, #1009, #1012, #1024,
|
||||||
|
#1030, #1035, #1036, #1039, #1040, #1044, #1045, #1049, #1050, #1051,
|
||||||
|
#1052, #1063, #1092, #1093, #1094, and #1100.
|
||||||
|
|
||||||
# 2.10.0
|
# 2.10.0
|
||||||
|
|
||||||
## Language changes
|
## Language changes
|
||||||
|
Loading…
Reference in New Issue
Block a user