Releases · CakeML/cakeml

Release list

CakeML v3400 Latest

Latest

xrchz released this 19 Jun 15:00

v3400

ccfc23c

Corresponding HOL commit: HOL-Theorem-Prover/HOL@d456022

Changes since release v3304:

Source language and front‑end

pat_bindings and pats_bindings no longer take an accumulator argument (progress on #662).

A first-order version of CakeML's PEG parser now exists (#1407).

Basis library

TextIO.inputAllFrom has been added to the basis library. The CF theorem for TextIO.inputAll has been corrected (#1375, #1366).

Compiler backend and runtime

perf-record --call-graph support (x64-only)

Passing --perf_callgraph=T to the CakeML compiler (x64-only) generates an unverified binary that can be profiled with perf record --call-graph fp.
The in-logic compiler uses the default config in x64_config.
Thus, to profile binaries such as checkers, the Dafny compiler, the Scheme compiler, etc., it is necessary to set perf_calls:=T in the configuration ultimately used by the compiler.

FlatLang

FlatLang has been simplified slightly (#1380).

DataLang

dataLang now supports multi-arg returns (#1416)

dataLang now avoid storing args in the cutsets unnecessarily (#1403)

WordLang

word_cse has been reworked to match more aggresively (#1410)

word_copy pass now additionally correctly propagates store-reg equality (#1385).

WordLang now supports Loop, Break, Continue (#1389).

Pancake

add_with_carry now available

It is now possible to use __add_with_carry__(left, right, carry_in)
in user code, which is compiled to wordLang's AddCarry.
Syntax example:

fun {1,1} f() {
  var a = 1;
  var b = 2;
  var c = 0;
  var {1,1} r = __add_with_carry__(a, b, c);
  r = __add_with_carry__(a, b, c);
  return r;
}

Permitted positions for __add_with_carry__ are declaration RHS and assignment RHS;
standalone, handler-attached, and tail-return calls are not supported.

LoopLang

LoopLang now supports multi-arg returns (#1391) and arbitrary depth Break/Continue (#1395).

LoopLang now compiles to WordLang Loops instead of tail calls, i.e., the old loop_remove pass is removed (#1391).

Garbage collector always disabled

The Pancake compiler now unconditionally compiles with GC set to none; any --gc=... flag passed alongside --pancake is silently ignored. This removes the unused GC runtime that Zhewen Shen's BSc thesis (p. 35) noted was being linked into every Pancake binary.

Candle

By optimizing the kernel Candle, we were able to achieve a 1.88x speedup on make_complex.ml (previously 56m49.502s, now 30m10.587s) (#1415).

A model of Little Theories (Farmer et al., 1992) has been added to Candle (#1405).

Examples

A new example for distributed SAT proof checking (#1384)

The FloVer example -- a Certificate Checker for Roundoff Error Bounds -- has been repaired and added back into the build-sequence (#1297, #1404).

Build infrastructure

examples/compilation/{ag32,x64} now make use of HOL's LOCAL_PARALLELISM_LIMIT instead of CLINE_OPTIONS = -j1, limiting parallelism only in that directory and not others (#1414).

Proof engineering and tooling

mlstring

str has been renamed to chr_to_str, freeing up str to be used for parameter names, for example. (#1307, #1372)
Added toString overload for chr_to_str (#1307, #1372).
Fused strlit and implode (#491, #1376).
- Incompatibilities
  - implode_def has been removed, so any references to it in tactics and automation need to be removed in user files.
  - A few proofs may break. In the cakeml repo the required fixes were relatively straightforward.
- Deprecations
  - strlit has been added as an inferior overload for backwards compatibility, but may be removed in the future. It is recommended to use implode instead.
  - strlit_tm, mk_strlit, dest_strlit and is_strlit are still available but may be removed in the future. It is recommended to use implode_tm, mk_implode, dest_implode and is_implode instead.

Assets 5

CakeML v3304

xrchz released this 25 Apr 18:59

v3304

f46cb7a

Corresponding HOL commit: HOL-Theorem-Prover/HOL@77fad20

Changes since release v3213:

Source language and front‑end

flatLang op wrapped in a Src ast$op constructor (#1337, issue #1336).
This unifies how source‑level operations are propagated into flatLang;
flat_elimProof and friends are updated.
OCaml front‑end (#1345, #1360). Desugaring from OCaml to the CakeML AST
is reworked, and the earlier handling of true/false in the OCaml parser
is reverted.
Verified string comparisons (#1331). Test gains semantics for string
comparisons, and a new MemOp StringCmp is implemented and verified through
the back‑end.
MOD fixity follow‑up. HOL changed MOD from Infixl 650 to
Infixl 600 (matching *). Explicit parentheses are added across the tree
so that a * b MOD c keeps its old meaning a * (b MOD c).

Basis library and runtime

TextIO.inputLine → TextIO.inputLineWith (#1340). The old name is
reused/renamed to better reflect the configurable line‑terminator behaviour;
callers throughout the tree are updated.
Runtime.customFFI added. New basis entry point with a matching C
helper, giving user programs a sanctioned way to invoke a custom FFI.

Configuration

inc_config removed (#1335, issue #1081). The incremental‑compilation
configuration record is retired in favour of the regular configuration.

Compiler backend

New Loop construct in stackLang (#1355). While is removed and
replaced by a more general Loop together with Break/Continue that can
jump out of (or continue) any enclosing loop. stack_alloc, word_to_stack,
stack_to_lab, and the cv translator are updated, and the new semantics is
proved correct (including removing all earlier cheats).
Variable‑length shifts (#1341). Support for variable shift amounts is
added in wordLang and all lower compiler phases.
32‑bit memory ops refactor (#1339). mem_load_32/mem_store_32 are
rewritten on top of the existing word_of_bytes/get_byte primitives.
Store read/write peephole optimisation in wordLang is the change that
shipped with v3213 (#1327) and forms the baseline for this range.

Register allocator

Four IRC register‑allocator bugs fixed (#1338).
Pancake entry points now save callee‑saved registers (#1332). Missing
RISC‑V, MIPS and ARMv8 callee‑saved register entries are added to the MEP
assembly stubs.

Pancake

Callee‑saved register fix above (#1332).
Pancake proofs migrated to the new suspend/Resume/Finalise style and
simplified by inlining theorem goals and removing ind_thm indirection
(#1356).

Candle / theorem prover

cv_if re‑defined in Candle (#1351).
mcandidate printer‑API fix (#1344). temp_remove_user_printer calls
are updated for the new HOL mcandidate API.
Candle and REPL evaluate proofs are ported to
suspend/Resume/Finalise (#1356).

Examples

Pseudo‑Boolean (PB) checker example refreshed (#1353).

Build infrastructure

Unverified sexp bootstrap reinstated in the build (#1358). The
unverified sexp bootstrap target is fixed up and added back to the standard
build sequence; a small error in types.txt is corrected on the way.

Proof engineering and tooling

suspend/Resume/Finalise rollout (#1356). A large clean‑up replaces
ad‑hoc proof bookkeeping in flat_to_closProof, bvl_to_bvi, word_cse,
word_to_stack, wordProps, the pancake proofs, and the Candle/REPL
evaluate proofs. Every use of get_goal is removed from the codebase.
No more parsing in library files (#1357, #1348). Library‑level
Definition/Theorem boilerplate is rewritten to use explicit Syntax
constructors instead of HOL term‑parser quotations, with assorted fix‑ups
(correct theories for type operators, missing imports of astSyntax before
astToSexprLib, regenerated READMEs, type‑variable / constant fixes).
type_vars ordering swap. type_vars and type_vars_in_term now
return their results in the reversed (HOL‑canonical) order in the local
Lib files; downstream code adjusted accordingly.
SmartOp2_thm sped up (#1361).
Two data_to_wordProof proofs sped up.
HOLSet addition no longer goes via List.rev.