CakeML/cakeml v3304 on GitHub

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).

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.

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

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.

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.

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).

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).

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.

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.