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--versionoutput, 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