v2024.01.13

What's Changed

• Fixing a division by zero in modulus by @nikswamy in #3050
• Pretty printing error messages by @mtzguido in #3027
• Nix: fix make_fstar_version.sh by @pnmadelaine in #3052
• Fixing unfolding logic in coercions by @mtzguido in #3054
• devcontainer: install memtrace by @mtzguido in #3055
• Tutorial chapter sixteen: use consistent types by @chandradeepdey in #3056
• Extraction hooks to support custom extraction by extensions by @nikswamy in #3058
• Improving some error formats. by @mtzguido in #3059
• ToSyntax: tighten a range by @mtzguido in #3060
• Some more pretty printing, and a lemma about spinoff by @mtzguido in #3062
• Widen types if they are used in typeclass constraints by @nikswamy in #3061
• A new Extension enum value for codegen by @aseemr in #3071
• Fixed Z3 version check crash by @Johanmyst in #3067
• Add push-partial-checked-file IDE request by @gebner in #3070
• examples: add a partial model for sealed by @mtzguido in #3073
• Some small changes in support of Pulse by @nikswamy in #3075
• Remove fstar.opam Python 2 dependency by @cmovcc in #3069
• Introducing int_of_string / bool_of_string by @mtzguido in #3053
• Tc: fix sigelt pushing to be unique (and hence prevent clashes during splices) by @mtzguido in #3063
• Implementing map_seal and bind_seal primitive operators by @mtzguido in #3074
• Add a lemma about subset being reflexive for lists by @chandradeepdey in #3078
• Some misc changes by @mtzguido in #3079
• Normalizer: invalidate memoizations if cfg changes by @mtzguido in #3072
• misc: A fix and a new function by @mtzguido in #3080
• Reflection.Typing: introduce basic sigelt_typing, allow splice_t to return a list by @mtzguido in #3065
• Milnes first typos in by @briangmilnes in #2903
• Fixing #3081 by @mtzguido in #3083
• A couple of fixes to improve error localization, especially in extensions like Pulse by @nikswamy in #3084
• ToDocument: pretty-print lens access operators by @gebner in #3082
• Misc fixes by @mtzguido in #3086
• Do not unfold logical connectives in norm requests by @mtzguido in #3085
• Exposing more pretty-printing ops by @mtzguido in #3088
• fix(doc/book): typos by @mzacho in #3092
• Properties of List.Tot.no_repeats_p by @tahina-pro in #3094
• Fixing #3089, and some unifier fixes by @mtzguido in #3091
• Tactics: make prop_validity_token erased by @mtzguido in #3096
• pretty-printer: consistently print nested tuples with (,) syntax by @amosr in #3100
• Fix #3051 by @mtzguido in #3101
• Fixing the escape check to provide better errors by @mtzguido in #3105
• tactics: ctrl_rewrite: perform rewrite under arrows; fix rewrite under dependent binders by @amosr in #3104
• Using typeclasses in src/ by @mtzguido in #2969
• Restoring some vale tests (and moving to tests/) by @mtzguido in #3109
• src/tactics: more use of typeclasses by @mtzguido in #3110
• Tc: Making defensive checks into a single def_check_scoped function by @mtzguido in #3111
• Misc SMT improvements by @mtzguido in #3112
• --proof_recovery by @mtzguido in #3113
• Support for local state in meta programs by @aseemr in #2948
• Adding an deq class and using it for lazy_kind by @mtzguido in #3114
• Some bug fixes by @mtzguido in #3117
• Fixing #2949 by @mtzguido in #3119
• Make --MLish --lax safer by @mtzguido in #3123
• More typeclasses, some cleanup by @mtzguido in #3124
• Fix stale hints script's return code, and run it by @mtzguido in #3125
• Some typeclass performance improvements by @mtzguido in #3126
• A very modest typeclass caching by @mtzguido in #3127
• Solving type constructors implicits before data constructor implicits by @mtzguido in #3132
• Fix typeclass arguments for types by @mtzguido in #3133
• Fixes for typeclasses by @mtzguido in #3134
• Misc improvements for SMT debugging by @mtzguido in #3136
• Pretty-printing options by @mtzguido in #3137
• More preparation for solver upgrade by @mtzguido in #3138
• Options: restore settable __temp_fast_implicits until uses are removed by @mtzguido in #3139
• Use a typeclass for ord and sets in the compiler by @mtzguido in #3141
• Reduce use of Set.elems, make notes where it remains by @mtzguido in #3143
• --MLish and extraction by @mtzguido in #3142
• Slight refactor in discharge_guard pipeline by @mtzguido in #3146
• Generalize univ annotations in effects by @mtzguido in #3121
• Cleaning up FStar/examples so that they all build cleanly into .checked files by @nikswamy in #3147
• Allow overloading exists and forall similar to let operators by @nikswamy in #3149
• A typechecker fix, and adding a monad class by @mtzguido in #3148
• Making pipe operators primitive by @mtzguido in #3122
• Tactics: use a monad typeclass internally by @mtzguido in #3150
• A type class for embedding by @mtzguido in #3152
• Stricter --MLish: no subtyping via has_type guards by @mtzguido in #3155
• primops: use embedding class to remove a ton of boilerplate by @mtzguido in #3154
• Tidy-up testing examples with the F* binary package by @tahina-pro in #3156
• More primops simplification and modularization by @mtzguido in #3157
• More primops cleanup by @mtzguido in #3158
• Fix primops by @mtzguido in #3159
• Add record name in the MLE_Record node by @aseemr in #3161
• Fix a scoping bug by @mtzguido in #3162
• More cleanup, gone with a couple thousand lines of boilerplate by @mtzguido in #3160
• Misc debugging improvements by @mtzguido in #3163
• A monadic visitor by @mtzguido in #3164
• Tc: Allow for #_ to solve instances by @mtzguido in #3165
• Misc changes by @mtzguido in #3167
• Misc fixes by @mtzguido in #3170
• A tactic for projectors (and methods) by @mtzguido in #3168
• An option to log (only) failing queries by @mtzguido in #3172
• Allowing to splice vals, and define vals with splices by @mtzguido in #3177
• FStar.Pure.Break: add a utility to "break away" the VC of the continuation by @mtzguido in #3174
• Primops: MachineInts: fix OP_underspec by @mtzguido in #3179
• Machine int primops2 by @mtzguido in #3180
• FStar.BV: expose bvshl, bvshr and bvmod with bit vector rhs by @amosr in #3116
• Advance to 2024.01.13~dev by @dzomo in #3190

New Contributors

• @chandradeepdey made their first contribution in #3056
• @Johanmyst made their first contribution in https:...

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 https://github.com/FStarLang/FStar/...

v2023.04.25

Steel is being split out to its own repository at https://github.com/FStarLang/steel . So, this F* release is the last one with Steel still being part of F*'s standard library.

What's Changed

• GitHub Actions workflows: releases, MacOS, Windows by @tahina-pro in #2880
• Excluding some fixpoint reductions in typechecker by @mtzguido in #2881
• Fixing inconsistencies in inspect_ln by @aseemr in #2882
• A synchronous mode for SMT queries (+ tactic), plus a change to --split_queries by @mtzguido in #2776
• Reducing some dependencies from the compiler into ulib by @mtzguido in #2883
• Misc memory fixes by @mtzguido in #2885
• Advance to 2023.04.25~dev by @dzomo in #2888

Full Changelog: v2023.04.08...v2023.04.25

v2023.04.08

What's Changed

• Release v2023.03.22 by @dzomo in #2860
• Do not install fstar_tests.exe by default by @tahina-pro in #2863
• Sealing pretty-printing names in the reflection API by @nikswamy in #2835
• syntax: dsenv: reimplement shorten_lid by trimming of prefixes by @mtzguido in #2707
• Makefile fixes to get bootstrap working with cygwin by @aseemr in #2864
• Reducing the amount of Tm_names in checked files by @mtzguido in #2845
• Supporting incremental parsing and additional features in the IDE protocol in support of fstar-vscode-assistant by @nikswamy in #2853
• Removing with_type (and vcgen.optimize_bind_as_seq) by @aseemr in #2871
• actions: unconditionally remove container after build by @mtzguido in #2875
• Require OCaml >= 4.10 by @tahina-pro in #2865
• Compiler.Util: do not capture stderr on start_process by @mtzguido in #2870
• Meta DSL framework by @aseemr in #2857
• A few more improvements to the strict positivity checker by @nikswamy in #2873
• Advance to 2023.04.08~dev by @dzomo in #2878

New Contributors

• @dzomo made their first contribution in #2860

Full Changelog: v2023.03.22...v2023.04.08

v2023.03.22

NOTE: This release mistakenly works only for Ubuntu 22.04. Other (including later) releases should also work on Ubuntu 20.04, unless explicitly stated otherwise.

What's Changed

• Build F* with dune instead of ocamlbuild by @tahina-pro in #2815
• Update README.md by @nikswamy in #2841
• Some assorted fixes by @mtzguido in #2839
• Use leftmost head when checking for equatable symbols in the core typechecker by @aseemr in #2846
• Normalizer fix for mutually recursive functions (#2849) by @mtzguido in #2850
• ImmutableArray: add positivity, hasEq, decreases, new qualifier by @mtzguido in #2855
• Support for limited extraction of indexed effects by @aseemr in #2851
• Preserving names in patterns during NBE by @mtzguido in #2858

Full Changelog: v2023.02.21...v2023.03.22

v2023.02.21

Release v2023.02.21

This is the last state before merging #2815 .

v2023.02.01

Release v2023.02.01

This is the last state before merging #2817 .

v2022.11.19

Release v2022.11.19

v2022.11.07

Release v2022.11.07

v2022.10.07

Release v2022.10.07