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 #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