What's Changed
- Allow --cache_dir to create parent directories by @mtzguido in #3194
- destruct_typ_as_formula: unascribe formula after unsquashing by @mtzguido in #3197
- NBE: mantain shape of primops to read them back them properly by @mtzguido in #3196
- Build fstarlib as bytecode too by @mtzguido in #3202
- Seq: reimplement seq_to_list and seq_of_list by casting by @mtzguido in #3203
- Adding attributes to the ML AST by @aseemr in #3205
- Tactics.Visit: visit computations in type ascriptions by @amosr in #3208
- FStar.Tactics.V2: embed Pat_Vars by sealing ppname by @amosr in #3211
- FStar.Compiler.Sealed: add an internal sealed type by @mtzguido in #3212
- Fix #3213 by @mtzguido in #3214
- Further fix for #3213 by @mtzguido in #3215
- Some fixes related to #3207 by @mtzguido in #3216
- Adding attributes to type parameters in ML AST by @aseemr in #3217
- Add a subset_mem lemma to make mem_subset more complete by @chandradeepdey in #3199
- Add missing case in lidents_of_term by @gebner in #3219
- Fixing a normalizer inefficiency by @mtzguido in #3222
- Tutorial chapter sixteen: Small fix in or introduction code by @chandradeepdey in #3223
- Make mem_filter stronger by @chandradeepdey in #3200
- Fixing #3224 by @mtzguido in #3225
- Tactics: add a primitive to spawn a subinvocation of the engine by @mtzguido in #3226
- Core typechecker fix for returns annotation by @aseemr in #3229
- Misc fixes by @mtzguido in #3235
- Fixing some scoping bugs by @mtzguido in #3237
- Fix #3238 by @mtzguido in #3239
- Using structured errors in tactics by @mtzguido in #3240
- Revert 3239 by @mtzguido in #3243
- A tweak to typeclass resolution: allow for "higher-order" resolution by @mtzguido in #3245
- Some misc cleanup changes to the normalizer by @mtzguido in #3247
- FStar.Tactics.Parametricity: move parametricity translation to ulib, as a plugin by @mtzguido in #3248
- Removing F* book sources from F* repo by @mtzguido in #3241
- Add a proof that the cardinality of Type(u+1) is greater than Type(u) by @mtzguido in #3244
- Misc fixes by @mtzguido in #3250
- Splitting qualifier/attribute checking in two phases by @mtzguido in #3254
- Small fix + cleanup in Core by @mtzguido in #3255
- Making Reals erasable, and providing a reflection API for real literals by @mtzguido in #3242
- Some fixes/improvements to the core typechecker by @mtzguido in #3256
- Misc changes by @mtzguido in #3257
- Some refactoring for typeclasses by @mtzguido in #3259
- Functional dependencies for typeclasses by @mtzguido in #3260
- Fix compat:open_metas option by @mtzguido in #3262
- Do not normalize domains of arrows with HNF. by @gebner in #3251
- Introduce and use a red-black tree implementation for sets by @mtzguido in #3261
- Fix by @mtzguido in #3267
- Tactics: make mapply a plugin by @mtzguido in #3268
- Misc changes by @mtzguido in #3269
- Removing the fv_delta field by @mtzguido in #3272
- Fixing CI by @mtzguido in #3273
- Misc by @mtzguido in #3276
- Syntax/SMT: Structure SMT errors (and Meta_labeled) by @mtzguido in #3277
- Some enhancements in support of interfaces in Pulse by @aseemr in #3270
- Making debug toggles more efficient by @mtzguido in #3274
- Small optimization in tcresolve, error message tweaks by @mtzguido in #3278
- Tactics.TypeRepr: add a tactic to translate inductives to a sums of products by @mtzguido in #3281
- Injectivity of inductive types revisited by @nikswamy in #3253
- Misc by @mtzguido in #3283
- Fix #3266 by @mtzguido in #3284
- Fixing #3264 by @mtzguido in #3287
- Misc error message fixes by @mtzguido in #3288
- SizeT: make SizeT.t a new type by @mtzguido in #3285
- Misc error message fixes by @mtzguido in #3289
- Tactics: if dump_on_failure is true, do not add Tactic failed prefix by @mtzguido in #3279
- Print: more pp instances by @mtzguido in #3290
- Color warnings yellow, diagnostics blue by @mtzguido in #3291
- Partial fix for 3292 by @mtzguido in #3293
- Misc fixes (typeclasses, printing) by @mtzguido in #3294
- Rel: make progress checking in head_matches_delta stricter by @mtzguido in #3297
- Debug/Options: make sure to restore debugging state after popping options by @mtzguido in #3298
- Introduce FStar.RefinementExtensionality by @mtzguido in #3299
- Misc tactics and debugging improvements by @mtzguido in #3300
- Syntax.Free: fix incomplete match by @mtzguido in #3301
- Misc fixes for error messages by @mtzguido in #3303
- Queue library by @meganfrisella in #2958
- FStar.Queue: rename to FStar.FunctionalQueue by @mtzguido in #3304
- Misc changes by @mtzguido in #3306
- Fix 3286 by @mtzguido in #3308
- Extract FStar.List.Pure.Base by @mtzguido in #3313
- Tactics: introduce ide() to check if running interactively by @mtzguido in #3314
- Resugaring for dependent tuples by @mtzguido in #3316
- Make parenthesis break binding on dtuples by @mtzguido in #3317
- All: replace all uses of
*for tuples by&by @mtzguido in #3318 - Allow empty record patterns by @mtzguido in #3321
- Add an interface for FStar.Reflection.V2.TermEq, and mark it a plugin by @mtzguido in #3322
- Introduce call_subtac_tm by @mtzguido in #3323
- Tactics: nit in compare_term to get better order, termination proof trickier by @mtzguido in #3324
- Misc tactics cleanup by @mtzguido in #3325
- Some basic simplification rules for reals by @mtzguido in #3305
- A fix in Core, revealed by FStarLang/pulse#100 by @mtzguido in #3326
- Fix a possible crash for empty record patterns by @mtzguido in #3327
- Implement query caching by @mtzguido in #3328
- Some interleaving improvements, in support of splice vals by @mtzguido in #3329
- devcontainer: fix Ubuntu to 23.10 and remove libicu by @mtzguido in #3331
- Make sure to catch missing definitions by @mtzguido in #3330
- Misc fixes by @mtzguido in #3334
- Tc: Env: rename nosynth->flychecking by @mtzguido in #3335
- Tactics: make splice_t always run without admit/lax by @mtzguido in #3336
- Fix 2583 by @mtzguido in #3338
- reflection: fix extraction for quoted real literals by @mtzguido in #3340
- Resugar: improve resugaring for projectors by @mtzguido in #3341
- Misc changes by @mtzguido in #3342
- Tactics: allow an expected typ for refl_instantiate_implicits by @mtzguido in #3343
- ci: disable --query_stats by @mtzguido in #3346
- extraction: krml: recognize mul_underspec as a multiplication by @mtzguido in #3349
- FStar.Math.Lemmas: Add an interface by @mtzguido in #3351
- Keeping an updated TC environment around during krml extraction by @mtzguido in #3350
- Misc: improving an error by @mtzguido in #3352
- Add test for #2419 by @mtzguido in #3354
- Normalizer: make sure to not leak cfgs across norm requests by @mtzguido in #3355
- Adding a missing simplifcation rule by @nikswamy in #3356
- Small refactor in the reflection modules by @mtzguido in #3347
- Plugin: fix arity mismatch by @mtzguido in #3357
- Extraction: sizet has uint_to_t, not int_to_t by @mtzguido in #3359
- norm: remove Cfg node altogether by @mtzguido in #3362
- Monotonic.Heap: mark mref as new by @mtzguido in #3365
- Frontend support for language extension with #lang-X by @nikswamy in #3363
- Math.Lemmas: remove needless include in fsti by @mtzguido in #3367
- Tidying lax vs admit, options vs environment by @mtzguido in #3337
- Generalize
FStar.Dynby @gebner in #3364 - Add clarification by @kant2002 in #2672
- Support tagging TacticFailure with an optional range by @nikswamy in #3370
- Add a --krmloutput option to chose filename for krml extraction by @mtzguido in #3371
- Add a new syntax to support partial
opens andincludes by @W95Psp in #3369 - Tactics: restoring ID info table on a failure by @mtzguido in #3374
- Advance to 2024.08.14~dev by @dzomo in #3375
- Tidy up hint usage by @mtzguido in #3377
New Contributors
- @meganfrisella made their first contribution in #2958
Full Changelog: v2024.01.13...v2024.08.14