Β« Changelog History


cryptol v2.12.0 Release Notes

  • Language changes

    • ⚑️ Updates to the layout rule. We simplified the specification and made some minor changes, in particular:

      • Paren blocks nested in a layout block need to respect the indentation if the layout block
      • We allow nested layout blocks to have the same indentation, which is convenient when writing private declarations as they don't need to be indented as long as they are at the end of the file.

    • πŸ†• New enumeration forms [x .. y by n], [x .. <y by n], [x .. y down by n] and [x .. >y down by n] have been implemented. These new forms let the user explicitly specify the stride for an enumeration, as opposed to the previous [x, y .. z] form (where the stride was computed from x and y).

    • Nested modules are now available (from pull request #1048). For example, the following is now valid Cryptol:

      module SubmodTest where

import submodule B as C

submodule A where
  propA = C::y > 5

submodule B where
  y : Integer
  y = 42

    πŸ†• New features

    • What4 prover backends now feature an improved multi-SAT procedure which is significantly faster than the old algorithm. Thanks to Levent Erkök for the suggestion.

    • There is a new w4-abc solver option, which communicates to ABC as an external process via What4.

    • πŸ‘ Expanded support for declaration forms in the REPL. You can now define infix operators, type synonyms and mutually-recursive functions, and state signatures and fixity declarations. Multiple declarations can be combined into a single line by separating them with ;, which is necessary for stating a signature together with a definition, etc.

    • There is a new :set path REPL option that provides an alternative to CRYPTOLPATH for controlling where to search for imported modules (issue #631).

    • πŸ‘ The cryptol-remote-api server now natively supports HTTPS (issue

      1008), newtype values (issue #1033), and safety checking (issue

      1166).

    • πŸš€ Releases optionally include solvers (issue #1111). See the *-with-solvers* files in the assets list for this release.

    πŸ› Bug fixes

    • Closed issues #422, #436, #619, #631, #633, #640, #680, #734, #735,

      759, #760, #764, #849, #996, #1000, #1008, #1019, #1032, #1033,

      1034, #1043, #1047, #1060, #1064, #1083, #1084, #1087, #1102, #1111,

      1113, #1117, #1125, #1133, #1142, #1144, #1145, #1146, #1157, #1160,

      1163, #1166, #1169, #1175, #1179, #1182, #1190, #1191, #1196, #1197,

      1204, #1209, #1210, #1213, #1216, #1223, #1226, #1238, #1239, #1240,

      1241, #1250, #1256, #1259, #1261, #1266, #1274, #1275, #1283, and

      1291.

    • πŸ”€ Merged pull requests #1048, #1128, #1129, #1130, #1131, #1135, #1136,

      1137, #1139, #1148, #1149, #1150, #1152, #1154, #1156, #1158, #1159,

      1161, #1164, #1165, #1168, #1170, #1171, #1172, #1173, #1174, #1176,

      1181, #1183, #1186, #1188, #1192, #1193, #1194, #1195, #1199, #1200,

      1202, #1203, #1205, #1207, #1211, #1214, #1215, #1218, #1219, #1221,

      1224, #1225, #1227, #1228, #1230, #1231, #1232, #1234, #1242, #1243,

      1244, #1245, #1246, #1247, #1248, #1251, #1252, #1254, #1255, #1258,

      1263, #1265, #1268, #1269, #1270, #1271, #1272, #1273, #1276, #1281,

      1282, #1284, #1285, #1286, #1287, #1288, #1293, #1294, and #1295.