FStar Versions Save

A Proof-oriented Programming Language

v2024.01.13

3 months ago

What's Changed

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

New Contributors

@chandradeepdey made their first contribution in https://github.com/FStarLang/FStar/pull/3056
@Johanmyst made their first contribution in https://github.com/FStarLang/FStar/pull/3067
@gebner made their first contribution in https://github.com/FStarLang/FStar/pull/3070
@mzacho made their first contribution in https://github.com/FStarLang/FStar/pull/3092
@amosr made their first contribution in https://github.com/FStarLang/FStar/pull/3100

Full Changelog: https://github.com/FStarLang/FStar/compare/v2023.09.03...v2024.01.13

v2023.09.03

8 months ago

What's Changed

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

New Contributors

@briangmilnes made their first contribution in https://github.com/FStarLang/FStar/pull/2902
@arbipher made their first contribution in https://github.com/FStarLang/FStar/pull/2985
@tdardinier made their first contribution in https://github.com/FStarLang/FStar/pull/2989
@2over12 made their first contribution in https://github.com/FStarLang/FStar/pull/3019
@bollu made their first contribution in https://github.com/FStarLang/FStar/pull/3030

Full Changelog: https://github.com/FStarLang/FStar/compare/v2023.04.25...v2023.09.03

v2023.04.25

1 year ago

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 https://github.com/FStarLang/FStar/pull/2880
Excluding some fixpoint reductions in typechecker by @mtzguido in https://github.com/FStarLang/FStar/pull/2881
Fixing inconsistencies in inspect_ln by @aseemr in https://github.com/FStarLang/FStar/pull/2882
A synchronous mode for SMT queries (+ tactic), plus a change to --split_queries by @mtzguido in https://github.com/FStarLang/FStar/pull/2776
Reducing some dependencies from the compiler into ulib by @mtzguido in https://github.com/FStarLang/FStar/pull/2883
Misc memory fixes by @mtzguido in https://github.com/FStarLang/FStar/pull/2885
Advance to 2023.04.25~dev by @dzomo in https://github.com/FStarLang/FStar/pull/2888

Full Changelog: https://github.com/FStarLang/FStar/compare/v2023.04.08...v2023.04.25

v2023.04.08

1 year ago

What's Changed

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

New Contributors

@dzomo made their first contribution in https://github.com/FStarLang/FStar/pull/2860

Full Changelog: https://github.com/FStarLang/FStar/compare/v2023.03.22...v2023.04.08

v2023.03.22

1 year ago

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 https://github.com/FStarLang/FStar/pull/2815
Update README.md by @nikswamy in https://github.com/FStarLang/FStar/pull/2841
Some assorted fixes by @mtzguido in https://github.com/FStarLang/FStar/pull/2839
Use leftmost head when checking for equatable symbols in the core typechecker by @aseemr in https://github.com/FStarLang/FStar/pull/2846
Normalizer fix for mutually recursive functions (#2849) by @mtzguido in https://github.com/FStarLang/FStar/pull/2850
ImmutableArray: add positivity, hasEq, decreases, new qualifier by @mtzguido in https://github.com/FStarLang/FStar/pull/2855
Support for limited extraction of indexed effects by @aseemr in https://github.com/FStarLang/FStar/pull/2851
Preserving names in patterns during NBE by @mtzguido in https://github.com/FStarLang/FStar/pull/2858

Full Changelog: https://github.com/FStarLang/FStar/compare/v2023.02.21...v2023.03.22

v2023.02.21

1 year ago

Release v2023.02.21

This is the last state before merging #2815 .

v2023.02.01

1 year ago

Release v2023.02.01

This is the last state before merging #2817 .

v2022.11.19

1 year ago

Release v2022.11.19

v2022.11.07

1 year ago

Release v2022.11.07

v2022.10.07

1 year ago

Release v2022.10.07