What's Changed
- Introduce FStar.Exception.string_of_exn to the library by @mtzguido in #3814
- Some typeclasses improvements by @mtzguido in #3815
- Typo suggestions by @mtzguido in #3816
- Core: use structured errors by @mtzguido in #3817
- Bump stage 0 by @mtzguido in #3818
- Misc by @mtzguido in #3819
- Windows: replace winwrap.sh with cygpath by @tahina-pro in #3802
- Fix crash by @mtzguido in #3820
- fstar.opam: add upper bound for ppxlib by @mtzguido in #3823
- Tweak some record errors by @mtzguido in #3822
- Resugar: preserve order of datacons when printing by @mtzguido in #3825
- Fix fstar.opam, and test it by @mtzguido in #3826
- Parser: make more lists right-flexible, allowing trailing comma or se… by @mtzguido in #3824
- Tactics: allow access to qualifiers and attributes during splice by @mtzguido in #3827
- Some fixes for FV qualifiers by @mtzguido in #3828
- FindZ3: fix caching by @mtzguido in #3829
- Improve error range for non-linear patterns by @mtzguido in #3830
- Misc patches by @mtzguido in #3831
- Tactics: introduce PrettifyType by @mtzguido in #3832
- nix: Pin the python version used by z3 by @Nadrieril in #3834
- Fix an order of arguments bug in NBE by @nikswamy in #3835
- nix: Update nixpkgs by @Nadrieril in #3836
- CI: remove ubuntu-20 runner by @mtzguido in #3837
- Misc fixes by @mtzguido in #3838
- Update ppxlib by @mtzguido in #3840
- Normalizer: rework norm requests by @mtzguido in #3841
- Fix Nix build by @mtzguido in #3842
- Introduce --stats by @mtzguido in #3839
- Data types a la carte by @nikswamy in #3845
- SMT: use rlimit and seed as part of query hash by @mtzguido in #3847
- Solver: do not use a hint if its fuels are no longer valid by @mtzguido in #3848
- Makefile: auto-rebuild stage0 when it changes by @mtzguido in #3851
- Remove eqtype_as_type from layered effect samples by @nikswamy in #3852
- An implementation of a naive and a hash-based string matcher by @nikswamy in #3854
- Annotated example for book chapter by @nikswamy in #3855
- an example of a lift in a la carte by @nikswamy in #3857
- feat(ulib): add list predicate
for_allPby @TWal in #3853 - Introduce
--ext extraction_inline_allby @mtzguido in #3858 - PrettifyType: some tweaks by @mtzguido in #3859
- Avoid inline let-bound terms in VCs by @nikswamy in #3861
- Fix sedlex rules by @hhugo in #3860
- nix: override sedlex locally to fix version mismatch by @Nadrieril in #3864
- Some nits by @mtzguido in #3866
- Allow native extraction of reifiable effects. by @mtzguido in #3867
- extraction: attempt to extract all type arguments by @mtzguido in #3869
- Bump version number by @mtzguido in #3870
New Contributors
- @Nadrieril made their first contribution in #3834
- @hhugo made their first contribution in #3860
Full Changelog: v2025.03.25...v2025.06.13