What's Changed
- SMT context pruning by @nikswamy in #3440
- fix: use more precise types for
move_requires_*by @TWal in #3449 - Misc by @mtzguido in #3451
- Improving internal error API by @mtzguido in #3453
- src: use fstar.include by @mtzguido in #3454
- A fix in tactics, do not set uvar_subtyping=false so eagerly by @mtzguido in #3446
- Extraction.Krml: properly detect mem type, it does not have an argument by @mtzguido in #3455
- Add normalization step for tactics. by @gebner in #3460
- Nits by @mtzguido in #3461
- Fix 3462 by @mtzguido in #3467
- Pretty-print ML extraction terms. by @gebner in #3468
- Extraction.Krml: pretty printing by @mtzguido in #3470
- Tweaks to default pretty instances. by @gebner in #3471
- Extraction.Krml: pp patterns by @mtzguido in #3472
- Fixing #3474: making sure module names match filenames in case by @mtzguido in #3478
- Moving prims.fst to Prims.fst by @mtzguido in #3479
- Warn on missing pop options by @mtzguido in #3480
- Adding #show-options to print current option flags by @mtzguido in #3481
- Extraction: print mllb_attrs by @mtzguido in #3482
- tactics: move concatMap to FStar.Tactics.Util by @mtzguido in #3483
- ulib: move hints to separate directory by @mtzguido in #3452
- Introduce doc/ref for development notes, document a bit about coercions by @mtzguido in #3484
- Resugar: make sure to compress before checking for machine integers by @mtzguido in #3486
- Errors: implementing error bound by @mtzguido in #3487
- Misc tactic improvements by @mtzguido in #3489
- dune tweaks: no cmt and no bytecode by @mtzguido in #3457
- Restore bytecode fstarlib by @msprotz in #3495
- A comment about bytecode version of fstar-lib by @mtzguido in #3497
- check-world: run hacl on github runners, avoid stupid uid issue by @mtzguido in #3499
- Arrow one by @mtzguido in #3500
- Some tactics and MkProjectors improvements by @mtzguido in #3501
- check-world: some documentation by @mtzguido in #3502
- Add message format cli option by @W95Psp in #3491
- Add extract_as attribute. by @gebner in #3466
- Bump dune version dependency. by @gebner in #3503
- Revise the SMT encoding of top-level prop definitions by @nikswamy in #3505
- Main: Add --list_plugins option by @mtzguido in #3506
- Improve publishing Nuget properties by @kant2002 in #3488
- Add a cast from size_t to uint64_t by @tahina-pro in #3507
- Main: adding --locate, --locate_lib, --locate_ocaml by @mtzguido in #3509
- Fix library finding in binary package by @mtzguido in #3512
- Util: fix mkdir for trailing slashes by @mtzguido in #3514
- A better error when z3 cannot be started by @mtzguido in #3517
- Reset gensym for predictable names and better query caching by @nikswamy in #3515
- Fixing mistaken erasure of effectful type applications by @nikswamy in #3518
- Represent implicits as a tree instead of a list to make conjoining them constant time by @nikswamy in #3521
- Desugaring: simplify desugaring for App, and respect textual order by @mtzguido in #3523
- Some nits by @mtzguido in #3524
- Some fixes in range module by @mtzguido in #3525
- Nits by @mtzguido in #3526
- Options: display short options in help, introduce
-dfor general debugging info by @mtzguido in #3527 - check-world: add mls-star by @mtzguido in #3513
- Fixing #3530 by @mtzguido in #3531
- Many fixes to resugaring by @mtzguido in #3532
- Autoload extension plugins by @mtzguido in #3533
- Options: --already_cached should not consider the current module by @mtzguido in #3529
- Makefile: fix clean rule by @mtzguido in #3535
- Some improvements wrt to plugins by @mtzguido in #3537
- Introducing a generic catenable list by @mtzguido in #3538
- Tc: make other components of guards also catenable lists by @mtzguido in #3539
- ulib: reducing some warnings by @mtzguido in #3540
- Improving a few errors by @mtzguido in #3541
- Extraction: not extracting tactics unless backend is Plugin by @mtzguido in #3542
- Do not print reveal or hide by default when resugaring by @nikswamy in #3544
- Update hints by @mtzguido in #3546
- Make the default effect in --MLish configurable by @mtzguido in #3548
- Parser.Dep: emitting a small header in the .depend by @mtzguido in #3550
- Tidying up a bit of FStar.All and FStar.Compiler.Effect by @mtzguido in #3551
- Make FStar.IO an interface by @mtzguido in #3552
- Revert "CI: point karamel to patched branch" by @mtzguido in #3554
- Preparing to use this F* as stage0 by @mtzguido in #3555
- ulib: move a type into stubs by @mtzguido in #3556
- Moving compiler sources into the FStarC namespace by @mtzguido in #3557
- Fix restricted open for constructors of type with indices by @W95Psp in #3558
- Restricted open: fix shadowing by @W95Psp in #3559
- fix(pp): char and string literals by @W95Psp in #3561
- Fix some missing branches for ShowOptions by @mtzguido in #3562
- Tactics: refactor a bit to avoid a cycle by @mtzguido in #3563
- Some refactoring about include paths, finding, locate, etc by @mtzguido in #3564
- Introduce --ocamlenv by @mtzguido in #3565
- Class.Show: remove dependency on Printable by @mtzguido in #3566
- Revert "Parser.Dep: remove wrong logic for FStar.Stubs" by @mtzguido in #3567
- Some library reorg by @mtzguido in #3569
- fix(check-world): only update F* for Comparse, DY* and MLS* by @TWal in #3568
- Loading plugins from the output dir too. by @mtzguido in #3570
- Small perf improvements, also fixing order dependency of qualifiers by @mtzguido in #3571
- Some nits by @mtzguido in #3573
- Fixing #3024 by @mtzguido in #3575
- Fix some quadratic name lookup behavior by @nikswamy in #3579
- tests: rework makefiles by @mtzguido in #3578
- tests: Makefile patch to make sure we disable hints for one file by @mtzguido in #3580
- Introducing --ocamlc and --ocamlc_plugin by @mtzguido in #3581
- Moving FStar.Pprint into the (normal, application) library by @mtzguido in #3582
- fstar: rename --ocamlc to --ocamlopt, add --ocamlc for bytecode by @mtzguido in #3583
- Tactics: fix V1.Logic by @mtzguido in #3584
- Delay snapshotting of desugaring environment by @nikswamy in #3585
- Optimize name resolution in desugaring by @nikswamy in #3586
- Use nanosecond timing from monotonic clock mtime for profiling by @nikswamy in #3587
- Passing -thread in --ocamlc/--ocamlopt by @mtzguido in #3588
- misc: Improving some errors by @mtzguido in #3590
- Remove duplicate lowercase hint files by @tahina-pro in #3591
- Simplifying Makefiles in test and examples by @mtzguido in #3594
- Main: fail when no files provided in batch by @mtzguido in #3593
- actions: adding a workflow to check for stale hints by @mtzguido in #3595
- Misc patches by @mtzguido in #3605
- test.mk: do not write checked files for output tests by @mtzguido in #3606
- Advance to 2024.11.07~dev by @dzomo in #3608
- Substitution must be fully applied in extraction by @nikswamy in #3607
- An induction principle for reflexive transitive closure by @nikswamy in #3609
- Fixing example in binary package by @mtzguido in #3610
- Fix nix build, add mk/ to src list by @mtzguido in #3611
- Advance to 2024.11.08~dev by @dzomo in #3612
- Extraction: add OCaml extension passes as for Krml by @mtzguido in #3614
- Adding everparse-cbor to check-world by @mtzguido in #3604
- CI: switch Dockerfiles back to Ubuntu 22.04 LTS by @tahina-pro in #3615
- Move away from deprecated batteries functions. by @gebner in #3423
- Fixes for binary package by @mtzguido in #3617
- Advance to 2024.12.03~dev by @dzomo in #3618
- test_package.sh: export FSTAR_ROOT to find makefiles by @mtzguido in #3619
- Fix #3616 by @mtzguido in #3621
- Fixes to make the windows binary build work by @mtzguido in #3620
- Makefiles: more conditional ocaml build, for package testing by @mtzguido in #3622
Full Changelog: v2024.09.05...v2024.12.03