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