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-postby @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
--includeby @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