v2023.09.03

What's Changed

• Unifying the range type into FStar.Range by @mtzguido in #2884
• Utilities on ranges exposed in reflection and tactics by @nikswamy in #2887
• Introducing an admit_termination attribute by @mtzguido in #2896
• Unifying the range type into FStar.Range by @mtzguido in #2892
• Adding FStar.Printable.fst with test by proof in tests/printable usin… by @briangmilnes in #2902
• Remove Steel from the F* code base by @tahina-pro in #2889
• Fix snapshot-diff detection for extraneous files by @mtzguido in #2911
• tests: ide: make test-incremental parallelizable by @mtzguido in #2898
• Support for custom syntax extensions by @nikswamy in #2909
• Some reflection/tactics updates by @mtzguido in #2918
• Use menhir by @mtzguido in #2910
• Nix: fix build by adding menhir dependency by @pnmadelaine in #2920
• Marking some symbols public in the menhir grammar by @nikswamy in #2921
• Some fixes to allow let recs on abbreviated types by @mtzguido in #2915
• Allow a syntax extension to provide qualifiers and attributes on a decl by @nikswamy in #2924
• fix ranges for extension syntax by @nikswamy in #2926
• Use named records in data constructors for some syntax classes by @aseemr in #2928
• A different fix for #2894 by @mtzguido in #2929
• Using a base image for CI jobs by @mtzguido in #2927
• Some tweaks to how delta depths are handled in the typechecker by @aseemr in #2934
• Exposing issues (warnings, errors, etc.) through the reflection API by @nikswamy in #2935
• Add missing case for LetOperator by @W95Psp in #2941
• Exposing a hook to read checked files, for use with separate tools built against fstar-lib by @nikswamy in #2942
• options/dep: introduce --output_deps_to by @mtzguido in #2932
• Making the handling of application nodes more uniform in the core checker by @nikswamy in #2944
• Nix: fix build (menhir dependency) + update lock file by @cmovcc in #2943
• Removing stale hints by @mtzguido in #2951
• Allow '@' on fatal errors in --warn_error by @TWal in #2950
• Simplifying subtype_of queries to avoid needless VCs related to proving that a term is a prop by @nikswamy in #2945
• Fixing order of --warn_error by @mtzguido in #2952
• Some build+test system tweaks by @mtzguido in #2956
• Revising checking arguments of an application in core by @nikswamy in #2959
• ci: use $(nproc) threads by @mtzguido in #2963
• Restoring the old error handler in Errors.catch_errors_aux by @nikswamy in #2965
• Exposing a few more productions for use in Pulse by @nikswamy in #2966
• Start a Tactics V2 by @mtzguido in #2960
• Some docs for tactics v2 and a CHANGES entry by @mtzguido in #2968
• colorizing the output of --query_stats by @mtzguido in #2972
• ulib: some proof taming by @mtzguido in #2973
• TermEq: expose universe comparisons by @mtzguido in #2975
• Support for negative literals in patterns by @aseemr in #2976
• Revising equality check in Core to emit a guard by @nikswamy in #2971
• ulib: introducing some standard classes by @mtzguido in #2977
• UInt128: proof taming by @mtzguido in #2979
• Unifier tweaks by @mtzguido in #2983
• Update part1_termination.rst by @arbipher in #2985
• Fixing the incremental parsing of syntax extension blobs by @nikswamy in #2987
• Simple lemma about appending permutations by @tdardinier in #2989
• Example: Leftist heap implementation by @tdardinier in #2982
• Support for close combinator for indexed effects by @aseemr in #2988
• Adding some comments to SMT log files by @mtzguido in #2992
• Initial support for matches in Reflection.Typing by @mtzguido in #2990
• Fix typo in OCaml code for extracting elements of a pair by @tdardinier in #2994
• Fixing the need to use --ide_id_info_off in Steel and Pulse by @nikswamy in #2996
• Fix hardcoded dependences of a file by @nikswamy in #2997
• Making AdmitWithoutDefinition (240) an error, by default by @nikswamy in #2925
• Introducing a minimal devcontainer (for codespaces) by @mtzguido in #2998
• Revising the way attributes are desugared by @nikswamy in #2940
• Misc changes by @mtzguido in #2999
• Tactic fixes by @mtzguido in #3001
• Introduce Z3 version switching by @mtzguido in #2995
• Misc tactics improvements by @mtzguido in #3003
• main.ml: only block signals on Posix systems by @mtzguido in #3006
• Makefile: remove -T on install usage by @mtzguido in #3008
• Misc fixes by @mtzguido in #3009
• A fix in query splitting by @mtzguido in #3010
• Tactics: allow Reflection.Typing primitives to raise guards by @mtzguido in #3011
• Fix extraction of character constants by @msprotz in #3007
• A fix in the core typechecker by @aseemr in #3004
• Fix in tactics, make sure to use optionstate by @mtzguido in #3013
• Exposing parsing_data in the unsafe_raw_read_checked_file by @nikswamy in #3018
• Changes for supporting ghost applications and ghost bind in Steel by @aseemr in #3012
• Fix typo in vec example proof by @2over12 in #3019
• Do not encode to SMT if admitting queries by @mtzguido in #3015
• ToSyntax: improve some ranges by @mtzguido in #3014
• Expose a utility to compute free vars of an AST term by @nikswamy in #3020
• Adding opens and abbrevs to sigelts by @nikswamy in #3022
• normalizer: avoid possible infinite loop on maybe_unfold_head by @mtzguido in #3021
• An --ext option by @nikswamy in #3023
• Restricting well-foundedness on inductives function-typed fields by @nikswamy in #2954
• deep_compress: remove some spurious warnings about Tm_names by @mtzguido in #3025
• A new noinline attributer for functions that should not be inlined by @msprotz in #3026
• Syntax of val binders by @nikswamy in #3029
• Add FStar.fst.config.json by @mtzguido in #3017
• Enable memtrace on F* by @mtzguido in #3016
• Hashconsed arrows/abstractions in the SMT encoding must be abstracted over their free variables by @mtzguido in #3028
• Revising the encoding of BoxBitVec_n by @nikswamy in #3033
• tactics: exposing ext_options/all_ext_options by @mtzguido in #3034
• Revising coercion mechanism to allow for implicit arguments by @mtzguido in #3032
• feat: Add 'bv_div_unsafe' to support 'bv / bv' expressions. by @bollu in #3030
• Making sure to invalidate a hint hash if Z3 version changes by @mtzguido in #3037
• Tactics: improving some ranges by @mtzguido in #3038
• Reduce dummy ranges in errors by @mtzguido in #3036
• Fix Nix build: add memtrace by @W95Psp in #3041
• Add (Github hosted) action for Nix by @W95Psp in #3042
• Misc improvements by @mtzguido in #3043
• Advance to 2023.09.03~dev by @dzomo in #3046

New Contributors

• @briangmilnes made their first contribution in #2902
• @arbipher made their first contribution in #2985
• @tdardinier made their first contribution in #2989
• @2over12 made their first contribution in #3019
• @bollu made their first contribution in #3030

Full Changelog: v2023.04.25...v2023.09.03