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.

Miscellaneous

• Typo fixes (#1354) and several stray‑character / mismatched‑quote fixes.

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

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

Corresponding HOL is the Trindemossen-2 release, i.e., HOL commit
HOL-Theorem-Prover/HOL@bdc6917.

Corresponding HOL commit: HOL-Theorem-Prover/HOL@718b3aa

Corresponding HOL commit: HOL-Theorem-Prover/HOL@48a676c

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

Corresponding HOL commit: HOL-Theorem-Prover/HOL@2de6b3c

Corresponding HOL commit: HOL-Theorem-Prover/HOL@277f6ad

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