v2024.09.05

What's Changed

• Extraction nits by @mtzguido in #3380
• Introduce --read_checked_file option by @mtzguido in #3381
• git protocol deprecated, use https instead by @LukeXuan in #3379
• Misc debugging nits by @mtzguido in #3383
• Debug: print stack dump on SIGINT when --trace_error by @mtzguido in #3384
• Misc nits by @mtzguido in #3386
• extraction: reexport mlexpr_to_string by @mtzguido in #3387
• Normalizer: ditch inline_closure_env, use a lazy substitution by @mtzguido in #3385
• prims: bump checked file version by @mtzguido in #3389
• Parser: introduce seq![1;2;3] for sequence literals by @mtzguido in #3390
• extraction: fix missing cases in mlpattern_to_string by @mtzguido in #3391
• AST: fix ast comparison, handle ListLiteral and SeqLiteral by @mtzguido in #3392
• Postpone checking of ModifiesGen by @mtzguido in #3393
• Fix Makefile by @mtzguido in #3394
• Tc: improving error for mistaking fields in a record by @mtzguido in #3395
• LowStar.Monotonic.Buffer: mark loc erasable by @mtzguido in #3396
• FStar.fst.config.json: make sure to use this fstar.exe by @mtzguido in #3398
• Normalizer: introduce DontUnfoldAttr, discard UnfoldTac by @mtzguido in #3399
• Tactics: remove canon tests from ulib/, place in new tests/ by @mtzguido in #3401
• Reflection: V2: support Equality qualifier for binders by @mtzguido in #3403
• actions/docker: reworking ci to just run make ci-post by @mtzguido in #3404
• Optimizing CI by @mtzguido in #3405
• Deps by @mtzguido in #3407
• normalizer: a fix for a plugin returned by a function by @mtzguido in #3409
• Revert "UInt128: break dependency on FStar.Int.Cast" by @mtzguido in #3410
• Misc improvements in library by @mtzguido in #3412
• Refactoring implicit instantiation by @mtzguido in #3413
• A bit more refactor by @mtzguido in #3414
• Using monoids for tc guards in TcTerm by @mtzguido in #3416
• Tc: rework attribute-tagged implicits to require defer_to by @mtzguido in #3415
• Main: introduce --read_krml_file mode by @mtzguido in #3419
• Some rework of the options module by @mtzguido in #3420
• Avoid wildcard expansion when making F# builds by @jonahbeckford in #3421
• Bump OCaml version to 4.14 by @gebner in #3397
• Some makefile fixes by @mtzguido in #3424
• extraction: krml: check for CInline attribute in letbindings, set an inlining flag in the binder by @mtzguido in #3418
• Introduce an attribute to unrefine type arguments by @mtzguido in #3406
• Refactoring printers by @mtzguido in #3425
• Fix encoding of primitive operators with refined domains by @nikswamy in #3427
• ulib: FStar.Range: allow inspecting the unsealed __range by @mtzguido in #3428
• Some fixes by @mtzguido in #3431
• feat(syntax): any terms in meta arguments by @W95Psp in #3430
• actions: check-world workflow by @mtzguido in #3433
• Parser.Dep: interpret inline_for_extraction on any decl, not just Vals by @mtzguido in #3432
• Misc fix by @mtzguido in #3435
• Do not require parentheses for fun/assume/assert by @gebner in #3378
• Fixing short circuting operators when --admit by @mtzguido in #3436
• parser: publish more symbols for Pulse by @mtzguido in #3437
• CI Tweaks by @mtzguido in #3438
• Adding Pulse bootstrapping test to check-world by @mtzguido in #3441
• checkworld tweaks by @mtzguido in #3442
• Reflection.Typing: add missing universe instantiation in elab_pat by @mtzguido in #3439
• Ide fixes by @mtzguido in #3443
• RFC: An fstar.include file to simplify --include by @mtzguido in #3345
• Advance to 2024.09.05~dev by @dzomo in #3444

New Contributors

• @LukeXuan made their first contribution in #3379
• @jonahbeckford made their first contribution in #3421

Full Changelog: v2024.08.14...v2024.09.05