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_terminationattribute 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
LetOperatorby @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_errorby @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
memtraceby @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