v4.11.0-rc1

What's Changed

• feat: upstream List.attach and Array.attach from Batteries by @llllvvuu in #4586
• fix: typo hearbeats -> heartbeats by @kmill in #4590
• feat: total ByteArray.toList/findIdx? by @Vtec234 in #4582
• chore: release triggers update of release.lean-lang.org by @nomeata in #4531
• chore: begin development cycle for v4.11.0 by @semorrison in #4594
• chore: pr-release: adjust to new lakefile.lean syntax by @nomeata in #4598
• fix: adapt kernel interruption to new cancellation system by @Kha in #4584
• feat: omega error message: normalize constraint order by @nomeata in #4612
• fix: diagnostics: show kernel diags even if it is the only section by @nomeata in #4611
• feat: termination_by structural by @nomeata in #4542
• feat: mul recurrence theorems for LeanSAT by @bollu in #4568
• fix: unresolve name avoiding locals by @digama0 in #4593
• feat: Nat.and_le_(left|right) by @TwoFX in #4597
• feat: additional lemmas for Option by @TwoFX in #4599
• feat: additional lemmas for lists by @TwoFX in #4602
• feat: getElem_congr by @TwoFX in #4603
• feat: additional lemmas for cond by @TwoFX in #4604
• feat: additional lemmas for bounded integers by @TwoFX in #4605
• chore: defs that should be theorems by @semorrison in #4619
• chore: delete deprecations from 2022 by @semorrison in #4618
• chore: satisfy duplicate namespace linter by @semorrison in #4616
• chore: follow simpNF linter's advice by @semorrison in #4620
• chore: add 'since' dates to deprecated by @semorrison in #4617
• chore: make constructor-as-variable test more robust by @TwoFX in #4625
• fix: enforce isDefEqStuckEx at unstuckMVar procedure by @leodemoura in #4596
• fix: Windows build by @Kha in #4628
• chore: pr-release: use right tag name by @nomeata in #4632
• fix: set default value of pp.instantiateMVars to true and make the option be effective by @kmill in #4558
• feat: USize.and_toNat by @TwoFX in #4629
• feat: Option.or by @TwoFX in #4600
• chore: typo by @alok in #4635
• feat: safe exponentiation by @leodemoura in #4637
• fix: make sure syntax nodes always run their formatters by @kmill in #4631
• chore: manual nightly trigger by @Kha in #4638
• chore: CI: restart-on-label: view run more often by @nomeata in #4640
• refactor: include declNames in Structural.EqnInfo by @nomeata in #4639
• fix: snapshot subtree was not restored on reuse by @Kha in #4643
• refactor: lambdaBoundedTelescope by @nomeata in #4642
• fix: improve synthAppInstances by @leodemoura in #4646
• feat: EquivBEq and LawfulHashable classes by @TwoFX in #4607
• feat: additional lemmas for arrays by @TwoFX in #4627
• fix: universe level in .below and .brecOn construction by @nomeata in #4651
• refactor: Split Constructions module by @nomeata in #4656
• feat: Std.HashMap by @TwoFX in #4583
• chore: restart-on-label: wait for 30s by @nomeata in #4663
• fix: don't set pp.tagAppFns when pretty printing signatures by @kmill in #4665
• fix: move Std from libleanshared to much smaller libInit_shared by @Kha in #4661
• fix: explicitly initialize Std in lean_initialize by @Kha in #4668
• chore: make Antisymm a Prop by @semorrison in #4666
• fix: hasBadParamDep? to look at term, not type by @nomeata in #4672
• chore: bump actions/checkout and actions/upload-artifacts by @nomeata in #4664
• chore: cleanup unused arguments (from linter) by @semorrison in #4621
• fix: unorphan modules in Init by @TwoFX in #4680
• fix: unorphan modules in Std.Data by @TwoFX in #4679
• chore: update codeowners by @TwoFX in #4681
• chore: Inhabited instances for Std.HashMap by @TwoFX in #4682
• chore: fix "max dynamic symbols" metric by @Kha in #4669
• fix: calculate error suppression per snapshot by @Kha in #4657
• chore: update comments in kernel/declaration.h by @nomeata in #4683
• feat: structural mutual recursion by @nomeata in #4575
• feat: Process.tryWait by @hargoniX in #4660
• chore: adjust List.replicate simp lemmas by @semorrison in #4687
• chore: upstream ToExpr FilePath and compile_time_search_path% by @semorrison in #4453
• chore: forward and backward directions of not_exists by @semorrison in #4688
• chore: upstream SMap.foldM by @semorrison in #4690
• chore: improve compatibility of tests/list_simp with Mathlib by @semorrison in #4691
• chore: add step to release checklist by @semorrison in #4693
• refactor: InductiveVal.numNested instead of .isNested by @nomeata in #4684
• feat: make @[ext] derive ext_iff theorems from user ext theorems by @kmill in #4543
• chore: upstream eq_iff_true_of_subsingleton by @semorrison in #4689
• chore: make use of ext_iff realization now that stage0 is updated by @kmill in #4694
• feat: lake: require @ git by @tydeu in #4692
• feat: omega doesn't push coercion over multiplication unnecessarily by @semorrison in #4695
• feat: chore upstream List.Sublist and API from Batteries by @semorrison in #4697
• fix: prefer original module in const2ModIdx by @digama0 in #4652
• feat: characterisations of List.Sublist by @semorrison in #4704
• feat: basic material on List.Pairwise and Nodup by @semorrison in #4706
• doc: update release checklist for new release notes workflow by @kmill in #4458
• feat: lemmas for List.head and List.getLast by @semorrison in #4678
• feat: simp normal form tests for Pairwise and Nodup by @semorrison in #4707
• chore: reorganise lemmas on list getters by @semorrison in #4708
• fix: Repr instances for Int and Float by @leodemoura in #4709
• fix: decide tactic transparency by @leodemoura in #4711
• fix: make iff theorem generated by @[ext] preserve inst implicits by @kmill in #4710
• fix: deprecated warnings for overloaded symbols by @leodemoura in #4713
• fix: mutual structural recursion: check that datatype parameters agree by @nomeata in #4715
• feat: upstream more erase API by @semorrison in #4720
• chore: fix typo in doc-string by @grunweg in #4719
• feat: further theorems for List.erase by @semorrison in #4723
• fix: make matcher pretty printer sensitive to pp.explicit by @kmill in #4724
• fix: nested structural recursion over reflexive data type by @nomeata in #4728
• feat: detailed feedback on decide tactic failure by @kmill in #4674
• feat: Meta.withErasedFVars by @nomeata in #4731
• feat: add #discr_tree_key command and discr_tree_key tactic by @mattrobball in #4447
• feat: .below and .brecOn for nested inductive by @nomeata in #4658
• refactor: use indVal.numNested or indVal.numTypeFormers where applicable by @nomeata in #4734
• feat: lake: cleaner release handling & related touchups by @tydeu in #4735
• doc: fix misplaced docstring for getThe by @sullyj3 in #4737
• refactor: IndGroupInfo and IndGroupInst by @nomeata in #4738
• test: extend test for #4671 with nice example reported on zulip by @nomeata in #4740
• feat: infer mutual structural recursion by @nomeata in #4718
• feat: structural recursion over nested datatypes by @nomeata in #4733
• feat: PProd and MProd syntax (part 1) by @nomeata in #4747
• feat: PProd and MProd syntax (part 2) by @nomeata in #4730
• chore: exclude more symbols to get below Windows symbol limit by @Kha in #4746
• chore: rename HashMap.remove to HashMap.erase by @TwoFX in #4725
• chore: missing profileitM by @leodemoura in #4753
• feat: add Lean.Expr.numObjs by @leodemoura in #4754
• chore: rename TC to Relation.TransGen by @semorrison in #4760
• chore: add comment for why anonymous constructor notation isn't flattened during pretty printing by @kmill in #4764
• feat: PProd syntax (part 3) by @nomeata in #4756
• refactor: move Synax.hasIdent, shake dependencies by @nomeata in #4766
• perf: add ShareCommon.shareCommon' by @leodemoura in #4767
• chore: add missing withTraceNode by @leodemoura in #4769
• feat: simprocs for #[1,2,3,4,5][2] by @semorrison in #4765
• chore: fix BEq argument order in hash map lemmas by @TwoFX in #4732
• fix: resolve instances for HashMap via unification by @TwoFX in #4759
• doc: mention linearity in hash map docstring by @TwoFX in #4771
• chore: simplify shareCommon' by @leodemoura in #4775
• perf: Replacement.apply by @leodemoura in #4776
• fix: missing assignment validation at closeMainGoal by @leodemoura in #4777
• feat: improve @[ext] error message when ext_iff generation fails by @kmill in #4762
• feat: add some low level helper APIs by @leodemoura in #4778
• fix: have elabAsElim check inferred motive for type correctness by @kmill in #4722
• perf: ensure Expr.replaceExpr preserve DAG structure in Exprs by @leodemoura in #4779
• chore: document replaceUnsafeM issue by @leodemoura in #4783
• fix: .eq_def theorem generation with messy universes by @leodemoura in #4712
• chore: Simp.Config.implicitDefEqProofs := true by default by @leodemoura in #4784
• refactor: IndGroupInst.brecOn by @nomeata in #4787
• refactor: add numFixed to Structural.EqnInfo by @nomeata in #4788
• fix: add term elaborator for Lean.Parser.Term.namedPattern by @leodemoura in #4792
• feat: theory from LeanSAT by @hargoniX in #4742
• perf: for_each with precise cache by @leodemoura in #4794
• perf: find? and findExt? by @leodemoura in #4795
• perf: kernel replace with precise cache by @leodemoura in #4796
• fix: for_each_fn.cpp by @leodemoura in #4797
• fix: replace_fn.cpp by @leodemoura in #4798
• perf: Expr.replace by @leodemoura in #4799
• doc: remove reference to HashMap.find? from Option docstring by @TwoFX in #4782
• fix: remove typeclass assumptions for Nodup.eraseP by @TwoFX in #4790
• feat: usize for array types by @fgdorais in #4801
• feat: use usize for array types by @fgdorais in #4802
• refactor: FunInd overhaul by @nomeata in #4789
• refactor: Introduce PProdN module by @nomeata in #4807
• chore: remove bif from hash map lemmas by @TwoFX in #4791
• feat: functional induction for mutual structural recursion by @nomeata in #4772
• feat: unnecessary termination_by clauses cause warnings, not errors by @nomeata in #4809
• doc: document Command.Scope by @grunweg in #4748
• fix: make elab_as_elim eagerly elaborate arguments for parameters appearing in the types of targets by @kmill in #4800
• feat: more hash map lemmas by @TwoFX in #4803
• doc: update quickstart guide by @mhuisi in #4806
• chore: release notes for mutual structural induction by @nomeata in #4808
• feat: safer #eval, and #eval! by @nomeata in #4810
• test: update test output following stage0 update by @nomeata in #4815
• test: test case for #4751 by @nomeata in #4819
• chore: List.filterMapM runs and returns left-to-right by @semorrison in #4820
• feat: trailing whitespace changes should not invalidate imports by @Kha in #4580
• feat: respond to info view requests as soon as relevant tactic has finished execution by @Kha in #4727
• fix: make sure anonymous dot notation works with pi-type-valued type synonyms by @kmill in #4818
• feat: create ci workflow on lake new/init by @austinletson in #4608
• fix: filter duplicate subexpressions by @mhuisi in #4786
• test: make #1697 test case Linux-Debug safe by @nomeata in #4829
• chore: report github actions failure on zulip by @nomeata in #4830
• fix: structural recursion: do not check for brecOn too early by @nomeata in #4831
• chore: upstream IsPrefix/IsSuffix/IsInfix by @semorrison in #4836
• feat: gaps/cleanup in List lemmas by @semorrison in #4835
• feat: List.IsPrefix/IsSuffix is decidable by @semorrison in #4837
• chore: upon nightly release, trigger nightly_bump_toolchain on mathlib4 by @nomeata in #4838
• chore: fix List deprecations by @semorrison in #4842
• chore: correct List.Subset lemma names by @semorrison in #4843
• fix: calling programs with spaces on Windows by @Kha in #4515
• doc: lake: require @ git in README by @tydeu in #4849
• feat: lake: CLI options to control output & failure log levels by @tydeu in #4847
• feat: bitVec shiftLeft recurrences for bitblasting by @bollu in #4571
• chore: cleanups for Mathlib.Init by @semorrison in #4852
• fix: handle unimported builtin names for location links by @kmill in #4780
• chore: update Topological.lean by @eltociear in #4853
• feat: upstream more List operations by @semorrison in #4855
• fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance, no chaining by @nomeata in #4839
• refactor: IndPredBelow: use apply_assumption by @nomeata in #4841
• fix: handle dependent fields when deriving BEq by @arthur-adjedj in #3792
• feat: upstream more List lemmas by @semorrison in #4856
• chore: CI: fix msys2 by @Kha in #4859
• chore: fix universe in PSigma.exists by @semorrison in #4862
• feat: more than one optional argument can be omitted while pretty printing by @kmill in #4854
• fix: make elabAsElim aware of explicit motive arguments by @kmill in #4817
• refactor: deriving DecidableEq to use termination_by structural by @nomeata in #4826
• chore: split Init.Data.List.Lemmas by @semorrison in #4863
• chore: upstream List.pairwise_iff_getElem by @semorrison in #4866
• chore: upstream List.eraseIdx lemmas by @semorrison in #4865
• chore: fix naming of List.Subset lemmas by @semorrison in #4868
• perf: precise cache for foldConsts by @leodemoura in #4871
• chore: fix binder explicitness in List.map_subset by @semorrison in #4877
• chore: rename PSigma.exists by @semorrison in #4878
• fix: mistake in statement of List.take_takeWhile by @kmill in #4875
• chore: copy release notes from releases/v4.10.0 by @kmill in #4864
• fix: make "use `set_option diagnostics true" message conditional on current setting by @kmill in #4781
• chore: updates to release_checklist.md by @semorrison in #4876
• chore: correct doc-string for Array.swap! by @semorrison in #4869
• refactor: split out Lean.Language.Lean.Types by @Kha in #4881
• feat: include command by @Kha in #4883
• fix: make import resolution case-sensitive on all platforms by @Kha in #4538
• feat: Nat simprocs for simplifying bit expressions by @bollu in #4874
• chore: shorten suggestion about diagnostics by @semorrison in #4882
• refactor: sharecommon by @leodemoura in #4887
• feat: ushiftRight bitblasting by @bollu in #4872
• perf: precise cache for expr_eq_fn by @leodemoura in #4890
• fix: export symbols needed by Verso by @david-christiansen in #4884
• fix: LEAN_EXPORT in sharecommon by @Kha in #4893
• chore: revert "fix: make import resolution case-sensitive on all platforms" by @Kha in #4896
• doc: add docstring to IO.FS.realpath by @alok in #4648
• feat: getLsb_replicate by @bollu in #4873
• chore: deprecate Nix-based build, remove interactive components by @Kha in #4895
• feat: accept user-defined options on the cmdline by @Kha in #4741
• perf: fix implementation of move constructors and move assignment ope… by @legrosbuffle in #4700
• perf: avoid expr copies in replace_rec_fn::apply by @legrosbuffle in #4702
• perf: use NatPow Int instead of HPow Int Nat Int by @leodemoura in #4903

New Contributors

• @grunweg made their first contribution in #4719
• @eltociear made their first contribution in #4853
• @legrosbuffle made their first contribution in #4700

Full Changelog: v4.10.0...v4.11.0-rc1