v4.15.0-rc1

What's Changed

• chore: begin development cycle for v4.15 by @kim-em in #5936
• chore: upstream lemmas about Fin.foldX by @kim-em in #5937
• chore: upstream List.ofFn and relate to Array.ofFn by @kim-em in #5938
• feat: List.mapFinIdx, lemmas, relate to Array version by @kim-em in #5941
• feat: introduce synthetic atoms in bv_decide by @hargoniX in #5942
• feat: add Int16/Int32/Int64 by @hargoniX in #5885
• feat: update toolchain on lake update by @tydeu in #5684
• fix: make all_goals admit goals on failure by @kmill in #5934
• chore: port release notes for v4.13.0 to master by @kim-em in #5947
• feat: List.pmap_eq_self by @vihdzp in #5927
• feat: add Option.or_some' by @vihdzp in #5926
• chore: remove @[simp] from BitVec.ofFin_sub and sub_ofFin by @kim-em in #5951
• feat: relate Array.takeWhile with List.takeWhile by @kim-em in #5950
• feat: relate Array.eraseIdx with List.eraseIdx by @kim-em in #5952
• chore: CI: check for GitHub Actions updates once per month by @Kha in #5954
• chore: CI: bump nwtgck/actions-netlify from 2.0 to 3.0 by @dependabot in #5956
• chore: CI: bump softprops/action-gh-release from 1 to 2 by @dependabot in #5955
• chore: CI: bump raven-actions/actionlint from 1 to 2 by @dependabot in #5957
• chore: CI: bump actions/stale from 8 to 9 by @dependabot in #5958
• chore: CI: give Linux Debug unlimited test stack size by @Kha in #5953
• chore: CI: bump lycheeverse/lychee-action from 1.9.0 to 2.0.2 by @dependabot in #5959
• chore: CI: bump actions/github-script from 6 to 7 by @dependabot in #5962
• chore: CI: bump dawidd6/action-download-artifact from 2 to 6 by @dependabot in #5964
• chore: CI: bump dcarbone/install-jq-action from 1.0.1 to 2.1.0 by @dependabot in #5965
• feat: define ISize and basic operations on it by @hargoniX in #5961
• fix: do not link statically against pthread/dl/rt by @TwoFX in #5966
• chore: fix all_goals test, simulate the max rec depth error by @kmill in #5967
• chore: deprecate Array.split in favour of identical Array.partition by @kim-em in #5970
• fix: arg conv tactic misreported number of arguments on error by @kmill in #5968
• feat: relate Array.isPrefixOf with List.isPrefixOf by @kim-em in #5971
• chore: consolidate decide_True and decide_true_eq_true by @kim-em in #5949
• feat: relate Array.zipWith/zip/unzip with List versions by @kim-em in #5972
• chore: exclude leanruntest_task_test_io for now by @TwoFX in #5973
• feat: add another List.find?_eq_some lemma by @kim-em in #5974
• chore: CI: bump mymindstorm/setup-emsdk from 12 to 14 by @dependabot in #5963
• chore: tag prerelease builds with -pre by @Kha in #5943
• feat: BitVec.twoPow in bv_decide by @hargoniX in #5979
• feat: minor lemmas about List.ofFn by @kim-em in #5982
• chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas by @kim-em in #5969
• feat: interactions between List.foldX and List.filterX by @kim-em in #5984
• feat: lemmas relating Array.findX and List.findX by @kim-em in #5985
• feat: BitVec.getMsbD in bv_decide by @hargoniX in #5987
• refactor: name the default SizeOf instance by @nomeata in #5981
• chore: fix test exclusion by @Kha in #5990
• style: fix style in bv_decide normalizer by @hargoniX in #5992
• feat: BitVec.sshiftRight' in bv_decide by @hargoniX in #5995
• chore: new PR changelog template by @Kha in #5976
• chore: revert "CI: give Linux Debug unlimited test stack size" by @Kha in #6001
• chore: List.modifyTailIdx naming fix by @kim-em in #6007
• chore: missing @[ext] attribute on monad transformer ext lemmas by @kim-em in #6008
• feat: verify keys method on HashMaps by @monsterkrampe in #5866
• fix: unset trailing for simpa? "try this" suggestion by @kmill in #5907
• feat: change bv_decide to an elaborated config by @hargoniX in #6010
• fix: ensure instantiateMVarsProfiling adds a trace node by @alexkeizer in #5501
• fix: avoid max heartbeat error in completion by @mhuisi in #5996
• perf: avoid negative environment lookup by @Kha in #5429
• chore: CI: exempt drafts from PR body check by @Kha in #6002
• feat: decide +revert and improvements to native_decide by @kmill in #5999
• feat: prop instance yields theorems by @kmill in #5856
• fix: avoid delaborating with field notation if object is a metavariable by @kmill in #6014
• fix: bv_decide benchmarks by @hargoniX in #6017
• chore: cleanup by @JovanGerb in #6021
• feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero by @bollu in #5616
• feat: variants of List.forIn_eq_foldlM by @kim-em in #6023
• chore: deprecate duplicated Fin.size_pos by @kim-em in #6025
• feat: change Array.set to take a Nat and a tactic provided bound by @kim-em in #5988
• feat: BitVec normalization rule for udiv by twoPow by @bollu in #6029
• fix: simp only [· ∈ ·] by @nomeata in #6030
• feat: bv_decide and flattening by @hargoniX in #6035
• fix: avoid new term info around def bodies by @Kha in #6031
• fix: bv_decide embedded constraint substitution changes models by @hargoniX in #6037
• feat: only direct parents of classes create projections by @kmill in #5920
• feat: change Array.get to take a Nat and a proof by @kim-em in #6032
• chore: review Array operations argument order by @kim-em in #6041
• feat: various minor changes to List/Array API by @kim-em in #6044
• chore: deprecate Array.sequenceMap by @kim-em in #6027
• chore: mark Meta.Context.config as private by @leodemoura in #6051
• refactor: mark the Simp.Context constructor as private by @leodemoura in #6054
• refactor: omega: avoid MVar machinery by @nomeata in #5991
• chore: pr-body: run as part of merge_group, but do not do anything by @nomeata in #6069
• fix: line break in simp? output by @Kha in #6048
• feat: Bool.to(U)IntX by @hargoniX in #6060
• test: synthetic simp_arith benchmark by @nomeata in #6061
• perf: optimize Nat.Linear.Expr.toPoly by @nomeata in #6062
• fix: make sure monad lift coercion elaborator has no side effects by @kmill in #6024
• perf: optimize Nat.Linear.Poly.norm by @nomeata in #6064
• feat: message kinds by @tydeu in #5945
• chore: add newline at end of file for lake new templates by @alissa-tung in #6026
• chore: remove >6 month old deprecations by @kim-em in #6057
• chore: upstream some NameMap functions by @kim-em in #6056
• feat: lemmas about for loops over Array by @kim-em in #6055
• feat: add Context.setConfig by @leodemoura in #6072
• refactor: lake: avoid v! in builtin code by @tydeu in #6073
• refactor: allow Sort u in Squash by @vihdzp in #6074
• perf: make andFlattening work on deeply nested hyps in one pass by @hargoniX in #6075
• feat: add options to configure all of bv_decide's preprocessing by @hargoniX in #6077
• fix: validate atoms modulo leading and trailing whitespace by @david-christiansen in #6012
• feat: Lean.RArray by @nomeata in #6070
• perf: simp_arith: faster denote through Lean.RArray by @nomeata in #6068
• feat: add date and time functionality by @algebraic-dev in #4904
• fix: pretty print .coeFun with terminfo of coercee by @kmill in #6085
• feat: implementation of Array.pmap by @kim-em in #6052
• chore: join → flatten in docstring by @vihdzp in #6040
• chore: bv_decide remove noop rewrites by @hargoniX in #6080
• fix: constant folding for Nat.ble and Nat.blt by @TwoFX in #6087
• perf: add LEAN_ALWAYS_INLINE to some functions by @TwoFX in #6045
• perf: remove @[specialize] from mkBinding by @JovanGerb in #6019
• refactor: use mkFreshUserName in ArgsPacker by @nomeata in #6093
• chore: remove decide! tactic by @kmill in #6016
• feat: pp.parens option to pretty print with all parentheses by @kmill in #2934
• feat: add Float.toBits and Float.fromBits by @leodemoura in #6094
• chore: naming convention and NaN normalization by @leodemoura in #6097
• fix: use Expr.equal instead of == in MVarId.replaceTargetDefEq and MVarId.replaceLocalDeclDefEq by @kmill in #6098
• fix: improvements to change tactic by @kmill in #6022
• feat: IO.getTID by @Kha in #6049
• fix: circular assignment at structure instance elaborator by @leodemoura in #6105
• chore: fix canonicalizer handling over forall/lambda by @kim-em in #6082
• chore: avoid stack overflow in debug tests by @Kha in #6103
• chore: fix naming of left/right injectivity lemmas by @kim-em in #6106
• fix: isDefEq, whnf, simp caching and configuration by @leodemoura in #6053
• fix: backtrack at injection failure by @leodemoura in #6109
• chore: document Lean.Elab.StructInst, refactor by @kmill in #6110
• feat: lemmas for Array.findSome? and find? by @kim-em in #6111
• chore: make Lean.Elab.Command.mkMetaContext public by @kim-em in #6113
• fix: liberalize rules for atoms by allowing leading '' by @david-christiansen in #6114
• fix: handle reordered indices in structural recursion by @nomeata in #6116
• chore: fix apply? error reporting when out of heartbeats by @kim-em in #6121
• chore: turn off pp.mvars in apply? results by @kim-em in #6108
• feat: use BaseIO at IO.rand by @tydeu in #6102
• feat: structure auto-completion & partial InfoTrees by @mhuisi in #5835
• test: fix brittle structure instance completion test by @mhuisi in #6127
• chore: generalize List.get_mem by @eric-wieser in #6095
• fix: don't issue atomic id completions when there is a dangling dot by @mhuisi in #5837
• fix: only consider salient bytes in sharecommon eq, hash by @tkoeppe in #5840
• fix: isDefEq when zetaDelta := false by @leodemoura in #6129
• fix: add a missing case to Level.geq by @digama0 in #2689
• fix: isDefEq for constants with different universe parameters by @leodemoura in #6131
• feat: have #print show precise fields of structures by @kmill in #6096
• feat: add BitVec.(msb, getMsbD)_(rotateLeft, rotateRight) by @luisacicolini in #6120
• feat: duplicate List.attach/attachWith/pmap API for Array by @kim-em in #6132
• feat: Array.insertIdx/eraseIdx take a tactic-provided proof by @kim-em in #6133
• feat: thread support for trace.profiler.output by @Kha in #6137
• fix: trace.profiler pretty-printing by @Kha in #6138
• fix: Inhabited Float produced a bogus run-time value by @Kha in #6136
• refactor: make use of recursive structures in snapshot types by @Kha in #6141
• fix: type occurs check bug by @JovanGerb in #6128
• doc: doc-strings to module docs in Data/Array/Lemmas by @adomani in #6144
• chore: avoid runtime array bounds checks by @kim-em in #6134
• feat: BitVec.getElem_[sub|neg|sshiftRight'|abs] by @tobiasgrosser in #6126
• chore: add changelog-* labels via comment by @kim-em in #6147
• fix: nontermination when generating the match-expression splitter theorem by @leodemoura in #6146
• refactor: one more recursive structure by @Kha in #6159
• fix: make sure whitespace is printed before tactic configuration by @kmill in #6161
• perf: speed up reflection of if in bv_decide by @hargoniX in #6162
• doc: adjust file reference in Data.Sum by @b-mehta in #6158
• feat: BitVec.toInt_[or|and|xor|not] by @tobiasgrosser in #6151
• feat: BitVec.getMsbD_[ofNatLt|allOnes|not] by @tobiasgrosser in #6149
• fix: revert creates natural metavariable goal by @JovanGerb in #6145
• feat: display coercions with a type ascription by @tonyxty in #6119
• feat: add builtin attribute to support elaboration of mutual inductives/structures by @kmill in #6166
• feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound by @kim-em in #6139
• feat: allow structure in mutual blocks by @kmill in #6125
• feat: create temporary directories by @david-christiansen in #6148
• fix: make the stack handling more robust to sanitizers and -O3 by @eric-wieser in #6143
• doc: fix typo and make docstring more precise by @david-christiansen in #6009
• feat: creation and reporting for asynchronous elaboration tasks by @Kha in #6170
• chore: add test for recursive structures by @kmill in #6173
• chore: refactor Elab.StructInst to use mutual for its structures/inductives by @kmill in #6174
• feat: have "motive is not type correct" come with an explanation by @kmill in #6168
• fix: nontermination while generating equation lemmas for match-expressions by @leodemoura in #6180
• fix: make sure #check id heeds pp.raw by @kmill in #6181
• chore: use Array.findFinIdx? where it is better than findIdx? by @kim-em in #6184
• feat: BitVec.toInt BitVec.signExtend by @bollu in #6157
• fix: remove obsolete sentence in doc-string by @kant2002 in #6185
• doc: refine kernel code comments by @nomeata in #6150
• chore: missing deprecations for Lean.HashMap by @kim-em in #6192
• feat: Array.zipWithAll by @kim-em in #6191
• fix: structures with copied parents can now use other parents as instances by @kmill in #6175
• feat: remove partial keyword and runtime bounds checks from Array.binSearch by @kim-em in #6193
• feat: Array.swap takes Nat arguments, with tactic provided proofs by @kim-em in #6194
• feat: rename Array.setD to setIfInBounds by @kim-em in #6195
• feat: upstream definition of Vector from Batteries by @kim-em in #6197
• feat: ensure Fin.foldl/r are semireducible by @kim-em in #6207
• feat: non-opaque UInt64.toUSize by @tydeu in #6202
• chore: fix Vector.indexOf? by @kim-em in #6208
• feat: add a coercion from List Nat to Lean.Meta.Occurrences by @kmill in #6206
• feat: make dot notation be affected by export/open by @kmill in #6189
• feat: missing lemmas about List's BEq by @kim-em in #6217
• feat: @[deprecated] requires a replacement identifier or message, and a since field by @kim-em in #6112
• chore: improve consistency & documentation for hash table insert and insertMany by @TwoFX in #6222
• feat: proper let_fun support in simp by @leodemoura in #6220
• feat: GitHub cloud releases do not clobber prebuilt artifacts by @tydeu in #6218
• fix: lake: eager logging when materializing deps by @tydeu in #6225
• feat: USize.size inequalities by @tydeu in #6203
• feat: Nat.lt_pow_self by @tydeu in #6200
• feat: expose diff at "synthesized type class instance is not definitionally equal" error by @kmill in #6213
• feat: Array fold lemmas by @kim-em in #6230
• feat: BitVec.toNat BitVec.signExtend by @bollu in #6155
• feat: add Nat.mod_eq_sub and fix dependencies from Nat.sub_mul_eq_mod_of_lt_of_le by @luisacicolini in #6160
• feat: BitVec.toInt_abs by @bollu in #6154
• feat: upstream Vector lemmas by @kim-em in #6233
• feat: upstream List.finRange from Batteries by @kim-em in #6234
• feat: lake: detailed Reservoir fetch error by @tydeu in #6231
• feat: relate Nat.fold/foldRev/any/all to List.finRange by @kim-em in #6235
• feat: Lean.loadPlugin by @tydeu in #6130
• chore: default parseQuotWithCurrentStage to true in stage 0 by @Kha in #6212
• fix: reparsing may need to backtrack two commands by @Kha in #6236
• fix: add cmake COPY_CADICAL option to allow turning off install copy by @juhp in #5931
• fix: Runtime.markPersistent is unsafe by @Kha in #6209
• fix: improve directory fallback on Linux and trim local time identifier by @algebraic-dev in #6221
• doc: explain abstraction order by @Vtec234 in #6239
• chore: cleanup in Array/Lemmas by @kim-em in #6243
• chore: deprecate Fin.ofNat (replaced by Fin.ofNat', subsequently to be renamed) by @kim-em in #6242
• feat: System.Platform.numBits inequalities by @tydeu in #6247
• feat: more UInt lemmas by @tydeu in #6205
• chore: cleanup of List/Array lemmas by @kim-em in #6249
• chore: lake: fix typo in materialize error by @tydeu in #6250
• feat: USize.reduceToNat by @tydeu in #6190
• feat: simpler trace timing annotation logic by @Kha in #6259
• chore: harden markPersistent uses by @Kha in #6257
• fix: don't walk full project file tree on every file save by @mhuisi in #6246
• feat: Simp.Config.implicitDefEqProofs by @leodemoura in #4595
• feat: add structInstFieldDecl syntax category by @kmill in #6265
• feat: parity between structure instance notation and where notation by @kmill in #6165
• chore: post-stage0 cleanup for #6165 by @kmill in #6268
• feat: remove runtime bounds checks and partial from qsort by @kim-em in #6241
• feat: more UInt bitwise theorems by @tydeu in #6188

New Contributors

• @dependabot made their first contribution in #5956
• @monsterkrampe made their first contribution in #5866
• @alissa-tung made their first contribution in #6026
• @algebraic-dev made their first contribution in #4904
• @tkoeppe made their first contribution in #5840
• @adomani made their first contribution in #6144
• @tonyxty made their first contribution in #6119

Full Changelog: v4.14.0...v4.15.0-rc1