v4.2.0-rc2

This version is known to contain a bug that could lead to data loss from lake clean, which has been fixed in 4.2.0-rc4. Users upgrading a project from this version to 4.2.0 rc4 should manually remove their lakefile.olean after adjusting lean-toolchain.

What's Changed

• perf: lake: lazily acquire repo URL/tag in :release by @tydeu in #2583
• doc: add token error change to RELEASES.md by @Kha in #2579
• chore: begin development cycle for v4.3.0 by @semorrison in #2585
• fix: hover term/tactic confusion by @digama0 in #2586
• doc: fix doc comment syntax in declModifiers doc comment by @nomeata in #2590
• chore: add release note about lake startup time by @semorrison in #2597
• chore: Remove unused variables from kernel by @nomeata in #2576
• Fix typos by @DenisGorbachev in #2605
• docs: update RELEASES.md for #2502 by @thorimur in #2606
• [Backport releases/v4.2.0] docs: update RELEASES.md for #2502 by @github-actions in #2613
• refactor: remove redundant let by @DenisGorbachev in #2614
• Fix linker warnings on macOS by @Kha in #2598
• feat : derive DecidableEq for mutual inductives by @arthur-adjedj in #2591
• fix: withLocation should use withMainContext for target by @alexjbest in #2607
• fix: XML parsing bugs by @kuruczgy in #2601
• feat: Web Assembly Build by @abentkamp in #2599
• feat: make Environment.mk private by @digama0 in #2604
• doc: fix the link to contribution guidelines by @DenisGorbachev in #2623
• feat: show path of failed import by @bollu in #2616
• doc: add missing character in testing.md by @david-christiansen in #2630
• Tag names by @david-christiansen in #2629
• fix: eliminate widestring uses by @Kha in #2633
• chore: fix typos in comments by @int-y1 in #2636
• chore: fix more typos in comments by @int-y1 in #2638
• perf: do not inhibit caching of default-level match reduction by @Kha in #2612
• chore: add missing if statements to pr-release.yml workflow by @semorrison in #2639
• chore: fix MVarId.getType' by @semorrison in #2595
• chore: add axiom for tracing use of reduceBool / reduceNat by @semorrison in #2654
• feat: replay constants into an Environment by @semorrison in #2617
• chore: remove unnecessary partial in ForEachExpr.visit by @digama0 in #2657
• chore: change trustCompiler axiom to True by @semorrison in #2662
• Add development process docs by @david-christiansen in #2650
• fix: treat pretty-printed names as strings by @Vtec234 in #2652
• feat: ToMessageData (α × β) instance by @digama0 in #2658
• fix: implementation of Array.anyMUnsafe by @semorrison in #2641
• perf: use quick_is_def_eq first by @digama0 in #2671
• chore: make Environment.add private by @semorrison in #2642
• fix: quot reduction bug by @digama0 in #2673
• fix: stdin := .null in IO.Process.output by @tydeu in #2544
• test: lake: show module with failed import by @tydeu in #2677
• feat: lake: postUpdate? + test by @tydeu in #2603
• Cancel outstanding tasks on document edit in the language server by @Kha in #2648
• feat: lake: --no-build option to exit before a build by @tydeu in #2651
• Machinery for opt-in builds in language server by @Kha in #2665
• fix : make mk_no_confusion_type handle delta-reduction when generating telescope by @arthur-adjedj in #2501
• isDefEq cache for terms not containing metavariables. by @leodemoura in #2644
• chore: simp tracing reports ← by @semorrison in #2621
• feat: use nat_gcd in the kernel by @semorrison in #2533
• chore: add items to RELEASES.md by @semorrison in #2687

New Contributors

• @DenisGorbachev made their first contribution in #2605
• @kuruczgy made their first contribution in #2601
• @abentkamp made their first contribution in #2599

Full Changelog: v4.2.0-rc1...v4.2.0-rc2