v2024.12.03

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 -d for 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