github FStarLang/FStar v2026.09.20
F* v2026.09.20

4 hours ago

What's Changed

  • tests/custard: CBOR boundary tests for the C and Rust columns by @gebner in #4482
  • tests/custard: put the header's directory on the mutant include path by @gebner in #4484
  • custard: refuse an unrepresentable float width at the value, not only at the type by @gebner in #4528
  • custard: binary16 and bfloat16 by @gebner in #4529
  • custard: emit the [custard_c_header] includes above the narrow-float support block by @gebner in #4530
  • custard: emit a [@@custard_extern] target verbatim, keywords included by @gebner in #4531
  • Pulse.Lib.Array.Core: allow changing permissions when the mask is empty by @mtzguido in #4543
  • Port LowStar.Comment to Pulse by @tahina-pro in #4546
  • Custard under the karamel: whole-program monomorphizing extraction by @gebner in #4395
  • Custard: migrate the test suites off the legacy extraction pipeline by @gebner in #4550
  • Simplify CI/devcontainer dependencies. by @gebner in #4549
  • FStar.Math.Pow: implement real exponentiation by @mtzguido in #4547
  • Support FStar.Attributes.rename_let in Pulse and Custard by @tahina-pro in #4552
  • Custard: realize Pulse.Lib.SpinLock, and migrate pulse/test/pool/pulse_task by @gebner in #4551
  • Custard: fold projections of a let-bound constructor by @gebner in #4553
  • Bump version to 2026.09.20 by @dzomo in #4555

Full Changelog: v2026.09.13...v2026.09.20

Don't miss a new FStar release

NewReleases is sending notifications on new releases.