v2025.01.07

This F* release supports using Z3 4.13.3 (though this is opt-in and the default is Z3 4.8.5 still). Both Z3 versions are packaged and ready to use.

What's Changed

• Merge F* branch used by EverParse Windows releases (empty PR) by @tahina-pro in #3623
• FStar.Seq.Permutation: stabilize proof by @mtzguido in #3625
• Some normalizer cleanups by @mtzguido in #3624
• --ocamlenv: fix for Windows, cannot use exec by @mtzguido in #3627
• ci: install z3 4.13.3 as well by @mtzguido in #3629
• Disable Div test on Windows by @tahina-pro in #3630
• Added FILELINE and it's test file by @briangmilnes in #3597
• SMT: lazy z3 start, do not start process until we need to ask a query by @mtzguido in #3634
• SMT: fix suggestions about Z3 install by @mtzguido in #3635
• Added missing bij_comp to FStar.Functions.fst* by @briangmilnes in #3633
• Upgrade F* to use Z3 4.13.3 by @nikswamy in #3631
• Add an interface to FStarC.Common by @mtzguido in #3639
• Print a suggestion for a common Windows footgun by @mtzguido in #3640
• Remove squash axioms. by @gebner in #3638
• Adapt CI to the new official Windows opam 2.3 by @tahina-pro in #3641
• Support get_fstar_z3.sh on macos by @gebner in #3646
• Options: print the option's help when arguments are wrong by @mtzguido in #3649
• Introduce --locate_file to ask F* for the location of modules or checked files by @mtzguido in #3650
• Dep: a few tweaks by @mtzguido in #3651
• Dep: revert sorting by @mtzguido in #3654
• Fixes to check-world, and a nightly build by @mtzguido in #3653
• SMTEncoding: prevent hash inconsistencies due to filepaths by @mtzguido in #3652
• Advance to 2025.01.06~dev by @dzomo in #3656
• Fixes for release by @mtzguido in #3657
• nix: enable more systems (e.g. MacOS) by @W95Psp in #3658

Full Changelog: v2024.12.03...v2025.01.07