v2024.08.14

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.Dyn by @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 and includes 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