F* v2025.08.07

What's Changed

• Allow using .. to match any number of constructor arguments by @mtzguido in #3877
• Exposing the expansion of .., to use from Pulse by @mtzguido in #3878
• CI: restore Nix cache & Nix builds by @mtzguido in #3879
• SMT: printing used rlimit by @mtzguido in #3745
• chore: update nixpkgs, revert sedlex override by @TWal in #3881
• fix(nix): make z3_4_8_5 nix build compatible with darwin plateforms by @W95Psp in #3882
• Core: fixup use ranges after cache hit by @mtzguido in #3885
• Syntax: allow writing TC constraints as groups by @mtzguido in #3886
• Parser: simplify, remove always-false boolean by @mtzguido in #3887
• Parser/Lexer: remove unneded argument for some more tokens by @mtzguido in #3888
• Parser: allowing refinements on multibinders by @mtzguido in #3889
• No batching of warning/errors by @mtzguido in #3810
• lib: add a red-black tree implementation of sets and maps by @mtzguido in #3890
• check-world: remove CBOR job by @mtzguido in #3891
• Tc: make 'new' and 'inline_for_extraction'/'noextract' compatible by @mtzguido in #3892
• Separate the --warn_error parser, fix crash on ill-formed options by @mtzguido in #3894
• Normalize: tweak warning about unfolding plugins by @mtzguido in #3895
• Some cleanup on machine integers by @mtzguido in #3896
• generic.mk: nit by @mtzguido in #3898
• FStarC.Range: add a 't' alias by @mtzguido in #3899
• Parser: move a warning away, into the desugaring phase by @mtzguido in #3901
• CI: update dev-base to OCaml 5.3.0 by @mtzguido in #3902
• Support universe-polymorphic splices. by @gebner in #3900
• dev-base: install domainslib by @mtzguido in #3904
• Add a bitvector test by @mtzguido in #3905
• All: simplify fuel settings by @mtzguido in #3906
• Misc by @mtzguido in #3907
• FStarC.Main: make sure to kill background Z3 processes before exiting by @mtzguido in #3908
• Some cleanups by @mtzguido in #3911
• Extraction: add pp instances for ML syntax by @mtzguido in #3912
• Misc error improvements by @mtzguido in #3913
• check-world: update everparse jobs by @mtzguido in #3914
• Make sure to kill Z3 when exiting by @mtzguido in #3915
• Tc: allow typeclass arguments in constructors by @mtzguido in #3916
• Fix pattern matching on typeclass arguments of constructors by @mtzguido in #3917
• Patching NBE unembeddings for machine ints by @nikswamy in #3918
• Misc cleanups by @mtzguido in #3920
• Introduce --expand_include by @mtzguido in #3921
• Fixes to check-friends for EverParse by @tahina-pro in #3922
• *: Remove uses of string_of_int/string_of_bool and use show by @mtzguido in #3923
• CI: add a pulse plugin build check, not enforced by @mtzguido in #3926
• FStarC.Util: Split some functions into FStarC.Time by @mtzguido in #3925
• Remove FStarC.Bytes by @mtzguido in #3927
• Remove FStarC.BigInt by @mtzguido in #3928
• Remove FStarC.StringBuilder, use StringBuffer by @mtzguido in #3929
• FStarC.Util: split away format functions into FStarC.Format by @mtzguido in #3930
• FStarC.Util Cleanup by @mtzguido in #3931
• Bump stage0 by @mtzguido in #3933
• machine integers: inline away the operators, remove them from .ml by @mtzguido in #3932
• Regenerate machine int files by @mtzguido in #3934
• FStar.Tactics.LaxTermEq: adding a laxer term_eq by @mtzguido in #3936
• LaxTermEq: fix, cannot use named view by @mtzguido in #3939
• check-world: no diff checking for everparse by @mtzguido in #3940
• Support unsaved files in the IDE. by @gebner in #3941
• Remove term_eq_old by @mtzguido in #3935
• Nits by @mtzguido in #3942
• Fixing #3943 by @mtzguido in #3944
• Typeclasses: solving refined, unit, and squash goals too by @mtzguido in #3946
• ToSyntax: refactor ticked variable handling by @mtzguido in #3947
• nit, usng an RBset by @mtzguido in #3949
• check-friends: add SecRef* by @mtzguido in #3950

Full Changelog: v2025.06.20...v2025.08.07