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_5nix 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