F* v2025.02.17

What's Changed

• Some refactoring, and tidying up libraries during build by @mtzguido in #3722
• Normalizer: making delta attributes compose by @mtzguido in #3723
• test.mk: Make sure to be silent on error output tests by @mtzguido in #3724
• Nits by @mtzguido in #3726
• Tactics: introduce postprocess_type by @mtzguido in #3725
• Nits by @mtzguido in #3728
• src: move FStarC.Interactive.* into src/interactive by @mtzguido in #3729
• Misc by @mtzguido in #3730
• Pretty-print SMT queries by @gebner in #3679
• Misc dep improvements by @mtzguido in #3731
• release.yml: Use annotated tags by @mtzguido in #3733
• fix ulibfs to use FStar_Pervasives_Native.option by @nikswamy in #3735
• Introducing FStar.Prelude, removing special casing for Prims/Pervasives internally by @mtzguido in #3732
• Remove Prims.array by @mtzguido in #3734
• rlimit by @mtzguido in #3736
• FStar.Math.Euclid: stabilize proof by @mtzguido in #3737
• Fix #3738 by @mtzguido in #3739
• Nits by @mtzguido in #3742
• FStarC.Range: do no try to find files when printing ranges by @mtzguido in #3740
• nit: Use projector/discriminator syntax instead of internal names by @mtzguido in #3743
• Nits by @mtzguido in #3744
• Tc: do not disable admit for splice_t by @mtzguido in #3747
• Resugar: fix bug for infix ops with implicits by @mtzguido in #3748
• NormSteps: fix delta_qualifier definition, was completely wrong by @mtzguido in #3749
• Dep: do not look at .fs/.fsi files by @mtzguido in #3746
• Nits by @mtzguido in #3750
• Fix build, and fix branch protection by @mtzguido in #3754
• Context pruning is set by default by @nikswamy in #3752
• Simplifying command-line usage of F* by @mtzguido in #3753
• IntN: add a fits for every module by @mtzguido in #3751
• Add everquic-crypto to check-world by @mtzguido in #3756
• FStarC.Timing: split timing funs away from FStarC.Util by @mtzguido in #3759
• FStarC.Range: always use basenames by @mtzguido in #3758
• Tc: binder attributes should not trigger instantiations by @mtzguido in #3761
• Tc: fix implicit vs explicit check by @mtzguido in #3762
• Parser: tweak error_message type for extension parsers by @mtzguido in #3763
• Parser: tweak grammar to expose a rule useful to Pulse by @mtzguido in #3764
• Introduce -o option, subsuming --krmloutput and --output_deps_to, and also location for checked and extracted files by @mtzguido in #3766
• Options: fix doc in --cache_checked_modules by @mtzguido in #3767
• Adding attributes to projectors, discriminators, and methods by @mtzguido in #3760
• Makefile: only use dune --release on release builds by @mtzguido in #3768
• Warn on nonexisting --include by @mtzguido in #3769
• Nits by @mtzguido in #3770
• Introduce .scripts/remove_unused_opens.sh by @mtzguido in #3755
• Extraction: respect -o option, plus cleanups by @mtzguido in #3773
• Revert "Makefile: only use dune --release on release builds" by @mtzguido in #3774
• Bump version number by @mtzguido in #3775

Full Changelog: v2025.02.06...v2025.02.17