What's Changed
- F* v2025.08.07 by @mtzguido in #3951
- Add SCIO* to check-friends workflow by @andricicezar in #3953
- Misc by @mtzguido in #3955
- No surface projector definitions by @mtzguido in #3954
- ToSyntax: remove generation of projector/discriminator decls by @mtzguido in #3956
- Introduce bare-tests by @mtzguido in #3957
- More informative tactic error messages by @gebner in #3952
- Makefile: fix stage0 rebuilding by @mtzguido in #3958
- Cleanups by @mtzguido in #3959
- Exit on SIGTERM. by @gebner in #3960
- Cleanups, fixes by @mtzguido in #3961
- Nits by @mtzguido in #3962
- Fix lax_term_eq by @mtzguido in #3963
- Default to Z3 4.13.3 by @mtzguido in #3880
- Extraction: reduce krml output unless -d/--debug by @mtzguido in #3528
- Syntax: no need to add a range to
var, a lident already has one by @mtzguido in #3964 - Typeclass goodies by @mtzguido in #3965
- Nits by @mtzguido in #3967
- Nits by @mtzguido in #3968
- Syntax.Hash: add many missing default cases by @mtzguido in #3969
- Misc by @mtzguido in #3971
- Errors: print expected failures as diags by @mtzguido in #3972
- Improving error location for failed meta args by @mtzguido in #3973
- Tactics: introduce stats_record by @mtzguido in #3974
- FStar.SizeT: add missing (/^) operator, also mark them inline by @mtzguido in #3975
- Misc fixes by @mtzguido in #3976
- Options: make --already_cached ReverseAccumulated by @mtzguido in #3977
- Restore internal (OCaml) unit tests by @mtzguido in #3978
- Reduce excessive debug by @mtzguido in #3979
- Tactics.PrettifyTypes: some improvements on generated types by @tahina-pro in #3981
- Introduce #check pragma by @mtzguido in #3982
- Tc: fix context push/pop in #check by @mtzguido in #3983
- Lexer: make
**actually right-associative, but keep its precedence by @mtzguido in #3984 - Remove traces of old 'DefaultEffect' qualifier by @mtzguido in #3948
- Do not peek past interfaces in dependence analysis for ide mode by @nikswamy in #3872
- Avoid some needless norm calls by @nikswamy in #3985
- NamedView: compress universes too by @mtzguido in #3987
- Flatten arrows before instantiating implicits by @nikswamy in #3988
- Misc cleanup by @mtzguido in #3989
- Reflection: support character constants by @mtzguido in #3992
- Options: allow to ignore warning for non-existing include by @mtzguido in #3994
New Contributors
- @andricicezar made their first contribution in #3953
Full Changelog: v2025.08.07...v2025.09.04