This release introduces a new mode of incremental module loading and dependency analysis, see PR #4060. Briefly, dependencies are loaded and brought into scope as they are mentioned, instead of this loading happening only once at the start of the checking of a module or of an interactive session. The new behavior has to be explicitly asked for by passing --ext fly_deps. This will become the default by the next release.

What's Changed

• Carrying universes through to the SMT encoding by @nikswamy in #3699
• Bump checked file version by @mtzguido in #4020
• Tactics: make sure to not affect variable uniqs during unshadowing by @mtzguido in #4023
• Fix core gensym bug by @nikswamy in #4022
• Record ctor: find type candidate using all field names by @amosr-msft in #4016
• Fixing record resolution for {e with f=v} by @nikswamy in #4024
• Revise term hash and equality by @nikswamy in #4025
• Revised caching in core by @nikswamy in #4026
• main: load native tactics when computing deps by @amosr-msft in #4027
• Make with_error_bound exception-safe. by @gebner in #4028
• Some improvements to context pruning by @nikswamy in #4029
• weaken precondition on pigeonhole by @nikswamy in #4030
• parser: desugar record puns as Var instead of Name by @amosr-msft in #4031
• Avoid re-checking types in core just to find their universe by @nikswamy in #4032
• simplify guards to true in phase1 by @nikswamy in #4033
• nasty bug in subtyping of arrow types, producing ill-typed VCs by @nikswamy in #4034
• Misc improvements by @mtzguido in #4037
• Lex/Parse: Remove dead code related to F#-style type application by @mtzguido in #4038
• Typeclasses: members with names beginning with _ do not get methods by @mtzguido in #3945
• Introduce --dump_ast by @mtzguido in #4039
• Nit, record stats for encode_sig by @mtzguido in #4042
• SizeT: relax type of fits, prevents spurious queries about non-negati… by @mtzguido in #4043
• Misc by @mtzguido in #4046
• Misc by @mtzguido in #4047
• A proof-of-concept tactic for concretizing nats by @mtzguido in #4048
• dune: move away from deprecated package by @mtzguido in #4049
• Some printing nits by @mtzguido in #4050
• Fix build of stage1 (and stage2 without release mode) by @mtzguido in #4051
• Rel: do not simplify guards to true for tactics by @mtzguido in #4052
• Tactics: fix detection of equalities to account for metas by @mtzguido in #4053
• Core: fix a nasty capture bug in generated guards for pattern matches by @mtzguido in #4054
• Tweaking imprecise encoding of inner let recs by @mtzguido in #3995
• Update ide mode to delay dependence scanning until the first check of the full buffer by @nikswamy in #4055
• Tactics: make V2 the default by @mtzguido in #3924
• File extensions by @amosr-msft in #4036
• get_fstar_z3: add command-line options to specify arch and kernel by @amosr-msft in #4044
• Nits, testcases by @mtzguido in #4056
• Encoding/Syntax: more canonicalization of arrows/applications in orde… by @mtzguido in #4058
• Parser.Dep: avoid possibly expensive call during --dep by @mtzguido in #4061
• Fix #3771 by @mtzguido in #4062
• Fix #3757 by @mtzguido in #4063
• Remove special handling of the file name by @nikswamy in #4057
• CI: Moving Windows job to cloud runners by @mtzguido in #4064
• nightly CI: fix after GitHub change by @mtzguido in #4065
• Windows improvements: add system= in --version output, tidy up smoke test by @tahina-pro in #4066
• build-windows.yml: do not use an artifact for the smoke test by @mtzguido in #4067
• Parser/Resugar: introduce LitDoc node, and resugaring extension pass API by @mtzguido in #4068
• A few IDE error range fixes by @mtzguido in #4069
• Misc by @mtzguido in #4070
• Syntax.Util: term_eq: ignore return annotations in match, fix infinit… by @mtzguido in #4071
• Misc by @mtzguido in #4072
• Loading dependences on the fly by @nikswamy in #4060
• Make sure instances are total, even with --MLish by @mtzguido in #4073
• Bump stage0 by @mtzguido in #4074
• Bump version number by @mtzguido in #4075

Full Changelog: v2025.10.06...v2025.12.15

What's Changed

• Fix bad error by @mtzguido in #3997
• source packages: do not use GNU-specific cp -T by @tahina-pro in #3998
• Set new EVERPARSE_USE_* variables for new EverParse build by @tahina-pro in #4002
• Pass tactic proof state using references by @gebner in #3999
• Bump stage0 by @mtzguido in #4006
• A few makefile fixes by @mtzguido in #4007
• bitvectors: SMT native bvnot; lemma for bv_uext by @amosr-msft in #4005
• Remove leftover z3version override. by @gebner in #4008
• Print uvars without space. by @gebner in #4009
• SMT: fix setting of random seed by @mtzguido in #4010
• Core: fix nasty guard closing bug by @mtzguido in #4012
• nix: bump to 5.3 by @gebner in #4014
• Bump version number by @mtzguido in #4015
• Prettier top-level lets in ML. by @gebner in #4013
• Work around OCaml printer issue, re-enable 4.14.2 CI by @mtzguido in #4017
• Some improvements to typeclass resolution performance by @mtzguido in #4018
• Prepare for release by @mtzguido in #4019

New Contributors

• @amosr-msft made their first contribution in #4005

Full Changelog: v2025.09.04...v2025.10.06

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

What's Changed

• Allow using .. to match any number of constructor arguments by @mtzguido in #3877
• Exposing the expansion of .., to use from Pulse by @mtzguido in #3878
• CI: restore Nix cache & Nix builds by @mtzguido in #3879
• SMT: printing used rlimit by @mtzguido in #3745
• chore: update nixpkgs, revert sedlex override by @TWal in #3881
• fix(nix): make z3_4_8_5 nix build compatible with darwin plateforms by @W95Psp in #3882
• Core: fixup use ranges after cache hit by @mtzguido in #3885
• Syntax: allow writing TC constraints as groups by @mtzguido in #3886
• Parser: simplify, remove always-false boolean by @mtzguido in #3887
• Parser/Lexer: remove unneded argument for some more tokens by @mtzguido in #3888
• Parser: allowing refinements on multibinders by @mtzguido in #3889
• No batching of warning/errors by @mtzguido in #3810
• lib: add a red-black tree implementation of sets and maps by @mtzguido in #3890
• check-world: remove CBOR job by @mtzguido in #3891
• Tc: make 'new' and 'inline_for_extraction'/'noextract' compatible by @mtzguido in #3892
• Separate the --warn_error parser, fix crash on ill-formed options by @mtzguido in #3894
• Normalize: tweak warning about unfolding plugins by @mtzguido in #3895
• Some cleanup on machine integers by @mtzguido in #3896
• generic.mk: nit by @mtzguido in #3898
• FStarC.Range: add a 't' alias by @mtzguido in #3899
• Parser: move a warning away, into the desugaring phase by @mtzguido in #3901
• CI: update dev-base to OCaml 5.3.0 by @mtzguido in #3902
• Support universe-polymorphic splices. by @gebner in #3900
• dev-base: install domainslib by @mtzguido in #3904
• Add a bitvector test by @mtzguido in #3905
• All: simplify fuel settings by @mtzguido in #3906
• Misc by @mtzguido in #3907
• FStarC.Main: make sure to kill background Z3 processes before exiting by @mtzguido in #3908
• Some cleanups by @mtzguido in #3911
• Extraction: add pp instances for ML syntax by @mtzguido in #3912
• Misc error improvements by @mtzguido in #3913
• check-world: update everparse jobs by @mtzguido in #3914
• Make sure to kill Z3 when exiting by @mtzguido in #3915
• Tc: allow typeclass arguments in constructors by @mtzguido in #3916
• Fix pattern matching on typeclass arguments of constructors by @mtzguido in #3917
• Patching NBE unembeddings for machine ints by @nikswamy in #3918
• Misc cleanups by @mtzguido in #3920
• Introduce --expand_include by @mtzguido in #3921
• Fixes to check-friends for EverParse by @tahina-pro in #3922
• *: Remove uses of string_of_int/string_of_bool and use show by @mtzguido in #3923
• CI: add a pulse plugin build check, not enforced by @mtzguido in #3926
• FStarC.Util: Split some functions into FStarC.Time by @mtzguido in #3925
• Remove FStarC.Bytes by @mtzguido in #3927
• Remove FStarC.BigInt by @mtzguido in #3928
• Remove FStarC.StringBuilder, use StringBuffer by @mtzguido in #3929
• FStarC.Util: split away format functions into FStarC.Format by @mtzguido in #3930
• FStarC.Util Cleanup by @mtzguido in #3931
• Bump stage0 by @mtzguido in #3933
• machine integers: inline away the operators, remove them from .ml by @mtzguido in #3932
• Regenerate machine int files by @mtzguido in #3934
• FStar.Tactics.LaxTermEq: adding a laxer term_eq by @mtzguido in #3936
• LaxTermEq: fix, cannot use named view by @mtzguido in #3939
• check-world: no diff checking for everparse by @mtzguido in #3940
• Support unsaved files in the IDE. by @gebner in #3941
• Remove term_eq_old by @mtzguido in #3935
• Nits by @mtzguido in #3942
• Fixing #3943 by @mtzguido in #3944
• Typeclasses: solving refined, unit, and squash goals too by @mtzguido in #3946
• ToSyntax: refactor ticked variable handling by @mtzguido in #3947
• nit, usng an RBset by @mtzguido in #3949
• check-friends: add SecRef* by @mtzguido in #3950

Full Changelog: v2025.06.20...v2025.08.07

This release is very minor change over 2025.06.13, to get a working OPAM build.

What's Changed

• Add [@@no_inline_let] annotation by @amosr in #3169
• Normalizer: simplify identities for real ops (e.g. 1.0R *. x ~> x) by @mtzguido in #3871
• Makefile: support busybox fin, which does not have -false by @mtzguido in #3873

Full Changelog: v2025.06.13...v2025.06.20

What's Changed

• Introduce FStar.Exception.string_of_exn to the library by @mtzguido in #3814
• Some typeclasses improvements by @mtzguido in #3815
• Typo suggestions by @mtzguido in #3816
• Core: use structured errors by @mtzguido in #3817
• Bump stage 0 by @mtzguido in #3818
• Misc by @mtzguido in #3819
• Windows: replace winwrap.sh with cygpath by @tahina-pro in #3802
• Fix crash by @mtzguido in #3820
• fstar.opam: add upper bound for ppxlib by @mtzguido in #3823
• Tweak some record errors by @mtzguido in #3822
• Resugar: preserve order of datacons when printing by @mtzguido in #3825
• Fix fstar.opam, and test it by @mtzguido in #3826
• Parser: make more lists right-flexible, allowing trailing comma or se… by @mtzguido in #3824
• Tactics: allow access to qualifiers and attributes during splice by @mtzguido in #3827
• Some fixes for FV qualifiers by @mtzguido in #3828
• FindZ3: fix caching by @mtzguido in #3829
• Improve error range for non-linear patterns by @mtzguido in #3830
• Misc patches by @mtzguido in #3831
• Tactics: introduce PrettifyType by @mtzguido in #3832
• nix: Pin the python version used by z3 by @Nadrieril in #3834
• Fix an order of arguments bug in NBE by @nikswamy in #3835
• nix: Update nixpkgs by @Nadrieril in #3836
• CI: remove ubuntu-20 runner by @mtzguido in #3837
• Misc fixes by @mtzguido in #3838
• Update ppxlib by @mtzguido in #3840
• Normalizer: rework norm requests by @mtzguido in #3841
• Fix Nix build by @mtzguido in #3842
• Introduce --stats by @mtzguido in #3839
• Data types a la carte by @nikswamy in #3845
• SMT: use rlimit and seed as part of query hash by @mtzguido in #3847
• Solver: do not use a hint if its fuels are no longer valid by @mtzguido in #3848
• Makefile: auto-rebuild stage0 when it changes by @mtzguido in #3851
• Remove eqtype_as_type from layered effect samples by @nikswamy in #3852
• An implementation of a naive and a hash-based string matcher by @nikswamy in #3854
• Annotated example for book chapter by @nikswamy in #3855
• an example of a lift in a la carte by @nikswamy in #3857
• feat(ulib): add list predicate for_allP by @TWal in #3853
• Introduce --ext extraction_inline_all by @mtzguido in #3858
• PrettifyType: some tweaks by @mtzguido in #3859
• Avoid inline let-bound terms in VCs by @nikswamy in #3861
• Fix sedlex rules by @hhugo in #3860
• nix: override sedlex locally to fix version mismatch by @Nadrieril in #3864
• Some nits by @mtzguido in #3866
• Allow native extraction of reifiable effects. by @mtzguido in #3867
• extraction: attempt to extract all type arguments by @mtzguido in #3869
• Bump version number by @mtzguido in #3870

New Contributors

• @Nadrieril made their first contribution in #3834
• @hhugo made their first contribution in #3860

Full Changelog: v2025.03.25...v2025.06.13

What's Changed

• Respect extract_as for recursive definitions too by @mtzguido in #3776
• Perf fixes by @mtzguido in #3777
• Update fstar.opam to correspond to ocaml/opam-repository/packages/fstar by @chandradeepdey in #3779
• Fix a scoping bug for dependent matches in Tactics.check_match_complete by @mtzguido in #3780
• Tactics: return proper errors when guards fail for typing reflection by @mtzguido in #3781
• Tc: unconditionally restore options before encoding a module by @mtzguido in #3783
• Add missing apt-get update by @gebner in #3785
• Simplify reveal ?u =?= reveal t to ?u =?= hide (reveal t). by @gebner in #3784
• Parser: allow operators in restricted opens by @mtzguido in #3786
• Tc: proper ranges for spliced definitions by @mtzguido in #3787
• Prims.ml: remove mentions of lex_t/LexNil/LexCons by @mtzguido in #3788
• Tc: no need to refresh the solver when loading from cache by @mtzguido in #3789
• Tc: tweak error range for wrong universe instatiation by @mtzguido in #3790
• INSTALL.md: fix location of get_fstar_z3.sh by @mtzguido in #3791
• Revert a block and recheck it, if the push kind changes (i.e., allows… by @nikswamy in #3792
• Parser: fix parsing of (-) by @mtzguido in #3793
• Parser: mark lidentOrOperator as public by @mtzguido in #3794
• Tactics.NamedView: guaranteeing that pack does not change top-level ctor by @mtzguido in #3795
• Add a test by @mtzguido in #3796
• Extraction: nit, rename type to avoid pun with FStar.Syntax by @mtzguido in #3798
• add starmalloc to check-world by @mtzguido in #3799
• Reflection.Typing: add a knob for instantiate_implicits by @mtzguido in #3801
• Misc fixes by @mtzguido in #3803
• Error improvements, misc fixes by @mtzguido in #3805
• Improve error range for incoherent matches by @mtzguido in #3806
• Error nits by @mtzguido in #3807
• Misc improvements by @mtzguido in #3808
• Primops.Real: more simplifications by @mtzguido in #3809
• Bump version number by @mtzguido in #3811

Full Changelog: v2025.02.17...v2025.03.25

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

What's Changed

• Making sure tactic errors respect error range bound by @mtzguido in #3687
• FStar.Issue: exposing doc_of_issue by @mtzguido in #3688
• Some build nits by @mtzguido in #3695
• FStarC.Util: make sure executable_name and exec_dir point to concrete… by @mtzguido in #3697
• Misc patches for error reporting by @mtzguido in #3701
• Makefile: macos compatibility by @mtzguido in #3702
• Fixed Z3 version check again by @Johanmyst in #3700
• Allow use_hints even when context_pruning is set by @nikswamy in #3703
• build: simplify, coallescing src/ml/full into ulib/ml/plugin, move src/ml/bare -> src/ml by @mtzguido in #3708
• lib.mk: include most FStar.Class modules by @mtzguido in #3709
• Options.Ext: refactor, and allow turning off boolean extensions by se… by @mtzguido in #3710
• Nik remove admit by @nikswamy in #3711
• workflow: nix: disable soon-to-eol magic Nix cache by @mtzguido in #3707
• Allow recording partial hints, make --record_hints settable by @mtzguido in #3704
• nit in error message, use docs by @mtzguido in #3713
• Tactics.Print: fix namedv_to_string by @mtzguido in #3715
• Improving errors when checking qualifiers, respecting no_auto_projector_decls by @mtzguido in #3716
• Misc cleanups by @mtzguido in #3717
• Error message tweaks by @mtzguido in #3718
• Makefile/package fixes by @mtzguido in #3719
• Some fixes in support of Pulse errors by @mtzguido in #3720
• Bump version number by @mtzguido in #3721

Full Changelog: v2025.01.17...v2025.02.06

What's Changed

• Remove FStar.Ghost.Pull by @gebner in #3636
• Staged build, new CI, new packaging by @mtzguido in #3637
• nix: exposing ocamlPackages as before by @mtzguido in #3662
• Makefile/opam fixes by @mtzguido in #3663
• mk: removing extraneous .ml files after extracting by @mtzguido in #3664
• Build improvements by @mtzguido in #3667
• ci.yml: run for merge queue by @mtzguido in #3668
• Tc: prevent reset of -d across modules by @mtzguido in #3669
• check-friends: restoring main repos by @mtzguido in #3670
• Errors: Introducing '--message_format github', for github actions by @mtzguido in #3553
• src: Fix VS code config to match Makefile by @mtzguido in #3673
• Preparing for a native Windows build by @mtzguido in #3674
• Misc build improvements by @mtzguido in #3675
• Improvements to --dep graph by @mtzguido in #3411
• Refresh hints by @mtzguido in #3676
• Improving Cygwin support by @mtzguido in #3642
• Detecting GITHUB_ENV and autoprinting github messages by @mtzguido in #3671
• Add an UnfoldOnce/delta_once normalizer step by @mtzguido in #3626
• Building a Windows package by @mtzguido in #3677
• Disable windows build, it amazingly already failed by @mtzguido in #3678
• src: Renaming FStarC.Compiler.* -> FStarC.* by @mtzguido in #3666
• Removing hints from the repo by @nikswamy in #3680
• Core: debug nits by @mtzguido in #3683
• Windows build (with self-hosted runner) by @mtzguido in #3684
• Bump version to 2025.01.17 by @mtzguido in #3685

Full Changelog: v2025.01.07...v2025.01.17