FStarLang/FStar v2024.01.13 on GitHub

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 #3067
@gebner made their first contribution in #3070
@mzacho made their first contribution in #3092
@amosr made their first contribution in #3100

Full Changelog: v2023.09.03...v2024.01.13