F* v2025.09.04

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