Release 2.13.0 · GaloisInc/cryptol

Language changes

Update the implementation of the Prelude function sortBy to use a merge sort instead of an insertion sort. This improves the both asymptotic and observed performance on sorting tasks.

"Type mismatch" errors now show a context giving more information about the location of the error. The context is shown when the part of the types match, but then some nested types do not. For example, when mathching { a : [8], b : [8] } with { a : [8], b : [16] } the error will be 8 does not match 16 and the context will be { b : [ERROR] _ } indicating that the error is in the length of the sequence of field b.

The What4 backend now properly supports Boolector 3.2.2 or later.
Make error message locations more precise in some cases (issue #1299).
Make :reload behave as expected after loading a module with :module (issue #1313).
Make include paths work as expected when nested within another include (issue #1321).
Fix a panic that occurred when loading dependencies before includes are resolved (issue #1330).
Closed issues #1098, #1280, and #1347.
Merged pull requests #1233, #1300, #1301, #1302, #1303, #1305, #1306, #1307, #1308, #1311, #1312, #1317, #1319, #1323, #1326, #1331, #1333, #1336, #1337, #1338, #1342, #1346, #1348, and #1349.