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.shby @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-fileIDE request by @gebner in #3070 - examples: add a partial model for
sealedby @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 --laxsafer 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
existsandforallsimilar 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_typeguards by @mtzguido in #3155 - primops: use embedding class to remove a ton of boilerplate by @mtzguido in #3154
- Tidy-up testing
exampleswith 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