Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prepare for 3.0.0 release #1531

Merged
merged 8 commits into from
Jun 26, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 45 additions & 1 deletion CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,25 @@
# next
# 3.0.0 -- 2023-06-26

## Language changes

* Cryptol now includes a redesigned module system that is significantly more
expressive than in previous releases. The new module system includes the
following features:

* Nested modules: Modules may now be defined within other modules.

* Named interfaces: An interface specifies the parameters to a module.
Separating the interface from the parameter declarations makes it possible
to have different parameters that use the same interface.

* Top-level module constraints: These are useful to specify constraints
between different module parameters (i.e., ones that come from different
interfaces or multiple copies of the same interface).

See the
[manual section](https://galoisinc.github.io/cryptol/master/Modules.html#instantiation-by-parametrizing-declarations)
for more information.

* Declarations may now use *numeric constraint guards*. This is a feature
that allows a function to behave differently depending on its numeric
type parameters. See the [manual section](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards))
Expand All @@ -19,6 +37,11 @@
* Infix operators are now allowed in import lists: `import M ((<+>))` will
import only the operator `<+>` from module `M`.

* `lib/Array.cry` now contains an `arrayEq` primitive. Like the other
array-related primitives, this has no computational interpretation (and
therefore cannot be used in the Cryptol interpreter), but it is useful for
stating specifications that are used in SAW.

## New features

* Add a `:time` command to benchmark the evaluation time of expressions.
Expand Down Expand Up @@ -52,8 +75,29 @@
* Fix a bug that caused finite bitvector enumerations to panic when used in
combination with `(#)` (e.g., `[0..1] # 0`).

* Cryptol's markdown parser is slightly more permissive and will now parse code
blocks with whitespace in between the backticks and `cryptol`. This sort of
whitespace is often inserted by markdown generation tools such as `pandoc`.

* Improve documentation for `fromInteger` (#1465)

* Closed issues #812, #977, #1090, #1140, #1147, #1253, #1322, #1324, #1329,
#1344, #1347, #1351, #1354, #1355, #1359, #1366, #1368, #1370, #1371, #1372,
#1373, #1378, #1383, #1385, #1386, #1391, #1394, #1395, #1396, #1398, #1399,
#1404, #1415, #1423, #1435, #1439, #1440, #1441, #1442, #1444, #1445, #1448,
#1449, #1450, #1451, #1452, #1456, #1457, #1458, #1462, #1465, #1466, #1470,
#1475, #1480, #1483, #1484, #1485, #1487, #1488, #1491, #1496, #1497, #1501,
#1503, #1510, #1511, #1513, and #1514.

* Merged pull requests #1184, #1205, #1279, #1356, #1357, #1358, #1361, #1363,
#1365, #1367, #1376, #1379, #1380, #1384, #1387, #1388, #1393, #1401, #1402,
#1403, #1406, #1408, #1409, #1410, #1411, #1412, #1413, #1414, #1416, #1417,
#1418, #1419, #1420, #1422, #1424, #1429, #1430, #1431, #1432, #1436, #1438,
#1443, #1447, #1453, #1454, #1459, #1460, #1461, #1463, #1464, #1467, #1468,
#1472, #1473, #1474, #1476, #1477, #1478, #1481, #1493, #1499, #1502, #1504,
#1506, #1509, #1512, #1516, #1518, #1519, #1520, #1521, #1523, #1527, and
#1528.

# 2.13.0

## Language changes
Expand Down
4 changes: 3 additions & 1 deletion cryptol-remote-api/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
# Revision history for `cryptol-remote-api` and `cryptol-eval-server`

## NEXT -- YYYY-MM-DD
## 3.0.0 -- 2023-06-26

* The v3.0.0 release is made in tandem with the Cryptol 3.0.0 release. See the
Cryptol 3.0.0 release notes for relevant Cryptol changes.
* Add more fields (such as `pragmas`, `parameter`, `module`, and `infix`) to
the response to the RPC `visible names` method.
* Do not error if `visible names` is called when a parameterized module is
Expand Down
2 changes: 1 addition & 1 deletion cryptol-remote-api/cryptol-remote-api.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 2.4
name: cryptol-remote-api
version: 2.13.1
version: 3.0.0.99
license: BSD-3-Clause
license-file: LICENSE
author: Galois, Inc.
Expand Down
4 changes: 3 additions & 1 deletion cryptol-remote-api/python/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
# Revision history for `cryptol` Python package

## NEXT -- YYYY-MM-DD
## 3.0.0 -- 2023-06-26

* The v3.0.0 release is made in tandem with the Cryptol 3.0.0 release. See the
Cryptol 3.0.0 release notes for relevant Cryptol changes.
* Add `property_names` and `parameter_names` commands, used to get only those
loaded names which are properties or module parameters, respectively.
* Add more fields (such as `pragmas`, `parameter`, `module`, and `infix`) to
Expand Down
2 changes: 1 addition & 1 deletion cryptol-remote-api/python/pyproject.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[tool.poetry]
name = "cryptol"
version = "2.13.1"
version = "3.0.0.99"
readme = "README.md"
keywords = ["cryptography", "verification"]
description = "Cryptol client for the Cryptol 2.13 RPC server"
Expand Down
2 changes: 1 addition & 1 deletion cryptol.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Cabal-version: 2.4
Name: cryptol
Version: 2.13.0.99
Version: 3.0.0.99
Synopsis: Cryptol: The Language of Cryptography
Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
License: BSD-3-Clause
Expand Down