v4.0.0-rc1

This is the first release candidate for the first official release of Lean 4.

What's Changed

• doc: finish Init.Prelude docs by @digama0 in #1445
• feat: implement USize.toUInt64 model by @digama0 in #1446
• feat: support let mut x := e | alt by @digama0 in #1455
• Drop last type parameter of RpcEncoding by @gebner in #1356
• fix: ac_rfl in subgoal by @pcpthm in #1453
• feat: go to definition for antiquot kinds by @digama0 in #1454
• fix: printing of integral JsonNumbers by @Vtec234 in #1456
• fix: use saturating casts in lean_float_to_uint8 to avoid UB by @digama0 in #1458
• doc: explain acronym by @Vtec234 in #1463
• doc: typos and indentation by @digama0 in #1468
• feat: prefer syntax doc over elab when both are present by @digama0 in #1467
• feat: add lineEq parser alias by @digama0 in #1466
• fix: don't show NaN sign info in Float.toString by @digama0 in #1459
• feat: generalize ReaderT instances by @digama0 in #1447
• feat: simple uri escaping and unescaping by @lovettchris in #1452
• feat: add more float functions by @digama0 in #1460
• doc: documentation for Init.Coe by @digama0 in #1472
• doc: relocate doc strings from elab to syntax by @digama0 in #1471
• feat: add hover info for quot precheck by @digama0 in #1475
• fix: use resolveGlobalConstNoOverloadWithInfo more by @digama0 in #1477
• Join point checker by @hargoniX in #1476
• feat: attributes on notation by @digama0 in #1478
• feat: attributes on {macro,elab}(_rules) by @digama0 in #1483
• Collapsible traces with messages by @gebner in #1448
• doc: some SimplePersistentEnvExtension methods by @PatrickMassot in #1487
• fix: decodeScientificLitVal? parses 1.0e+1 correctly by @EdAyers in #1486
• feat: utilities for using scientific notation and floats in json by @EdAyers in #1464
• doc: Format by @EdAyers in #1489
• feat: add @[inheritDoc] attribute by @digama0 in #1480
• feat: add declId hover for syntax/notation/mixfix/elab/macro by @digama0 in #1482
• doc: documentation for Init.Notation by @digama0 in #1481
• fix: missing digits in scientific literal should be an error by @EdAyers in #1492
• feat: add join point detector by @hargoniX in #1495
• doc: documentation for Init.Tactics by @digama0 in #1490
• doc: documentation for Init.SizeOf by @digama0 in #1491
• Handle out of scope join points in the join point finder by @hargoniX in #1496
• fix: hygienic resolution of namespaces by @Kha in #1442
• fix: CI: create portable tarballs by @Kha in #1498
• fix: alternative tar fix by @Kha in #1499
• feat: blocking behavior on EOF for readLine by @goens in #1479
• chore: remove unexpanded coercion support from pp.analyze by @gebner in #1507
• doc: fix typo by @neelance in #1508
• fix: remove incorrect syntax coercion by @gebner in #1511
• feat: make (_ : a = b) hoverable in infoview by @gebner in #1506
• fix: remove duplicate OfNat Int instance by @pcpthm in #1509
• feat: Float.abs function by @fynnsu in #1514
• fix: Core.transform API and uses by @Kha in #1512
• feat: generalise forEachExpr by @EdAyers in #1504
• fix: use withContext at ac_rfl by @digama0 in #1519
• chore: remove outdated TODO by @digama0 in #1520
• doc: ptrAdr, JSON-RPC by @EdAyers in #1516
• feat: dbgStackTrace by @Kha in #1515
• Document, fix EOF behavior by @Kha in #1503
• fix: @[inheritDoc] on notation by @digama0 in #1523
• chore: remove def implies by @digama0 in #1530
• fix: prove decidable_of_decidable_of_eq without cast by @digama0 in #1531
• refactor: golf proof of funext by @digama0 in #1532
• doc: documentation for Init.Core by @digama0 in #1533
• chore: move Std -> Bootstrap by @digama0 in #1534
• doc: explanations for LCNF. by @bollu in #1538
• chore: move Bootstrap.System.Uri to Init by @digama0 in #1540
• refactor: generalize ShareCommon to a typeclass by @digama0 in #1537
• chore: move ShareCommon to Init / Lean by @digama0 in #1539
• refactor: Init.SimpLemmas proof golf / cleanup by @digama0 in #1544
• chore: move Bootstrap.Data -> Lean.Data by @digama0 in #1541
• Basic Pass Manager by @hargoniX in #1550
• Show parser docstrings independent of info tree by @Kha in #1517
• feat: add TR versions of Nat.{fold, any, all, repeat} by @digama0 in #1545
• fix: collision between implicit and auto-bound level names by @Kha in #1513
• feat: add Hashable for Subtype by @marcusrossel in #1553
• feat: use RPC method from first snapshot by @gebner in #1548
• chore: move Bootstrap.Dynamic -> Init.Dynamic by @digama0 in #1542
• chore: remove Bootstrap package by @digama0 in #1543
• doc: update the mdbook instructions by @lovettchris in #1521
• doc: update lean 3 -> lean 4 in declarations.md by @digama0 in #1557
• feat: utils for RBMap by @EdAyers in #1552
• A basic compiler pass test framework by @hargoniX in #1559
• doc: fix typo by @digama0 in #1561
• Additional concurrency primitives by @gebner in #1555
• doc: add documentation on monads by @lovettchris in #1505
• feat: deriving Repr for TSyntax by @digama0 in #1570
• feat: remove description argument from register_simp_attr by @gebner in #1566
• fix: visit jp bodies in join point finder by @hargoniX in #1574
• fix doc typos and do some polish on wording by @lovettchris in #1568
• fix: use Type u universes in List.foldl by @digama0 in #1579
• chore: remove map₂, [specialize] zipWith by @digama0 in #1580
• doc: enable syntax highlighting for the Macro Overview by @eyelash in #1577
• doc: some do extensions by @Kha in #1589
• doc: document Init.Data.Queue by @digama0 in #1583
• feat: allow optional type in example by @digama0 in #1593
• doc: fix an example in the Macro Overview by @eyelash in #1584
• Show error message for empty instances by @gebner in #1588
• feat: support {s with ..} by @digama0 in #1582
• fix: deindent docstrings with empty lines by @gebner in #1596
• feat: move docstring before | in ctors by @gebner in #1598
• feat: tail-recursive List.{mapM, foldrM} by @digama0 in #1581
• fix: make all syntax accessors non-panicking by @gebner in #1595
• docs: fix typo in SeqRight docstring by @jpablo in #1602
• chore: fix a typo in def name getOptionDefaulValue by @alexjbest in #1605
• fix: fixes #1599 by adding correct indentation by @ydewit in #1603
• chore: import reductions by @digama0 in #1601
• doc: fix Markdown code-blocks in declarations.md by @eyelash in #1611
• feat: Kleisli operators by @EdAyers in #1608
• doc: MetavarContext by @EdAyers in #1613
• feat: use sepBy1Indent for tactic and conv blocks by @gebner in #1612
• doc: refine mdbook docs by @Kha in #1621
• chore: fixed typos in Expr docstrings by @ydewit in #1623
• feat: expose that panic α = default by @digama0 in #1614
• feat: use colEq in sepByIndent by @gebner in #1622
• feat: remove bounds checks in Array.{reverse, insertAt} by @digama0 in #1609
• feat: multiple case by @digama0 in #1628
• feat: injections with names by @digama0 in #1631
• chore: remove getElem', use a custom delab by @digama0 in #1597
• chore: few updates to Expr docstrings by @ydewit in #1624
• feat: multiple delta by @digama0 in #1630
• feat: if _ : cond then t else e syntax by @digama0 in #1634
• feat: goal-diffs by @EdAyers in #1610
• RB tree refinements by @Kha in #1643
• feat: add tactic.simp.trace option by @digama0 in #1626
• feat: generalize e = x at h by @digama0 in #1635
• feat: show decl module in hover by @digama0 in #1638
• feat: pattern (occs := ...) conv by @digama0 in #1632
• chore: move Std.* data structures to Lean.* by @digama0 in #1645
• feat: basic constant folder by @hargoniX in #1652
• doc: add docstrings in PersistentExtension by @PatrickMassot in #1649
• doc: some documentation for Message.lean by @EdAyers in #1655
• feat: add (canonical := true) option in Syntax by @digama0 in #1620
• feat: datatypes for LSP code actions by @EdAyers in #1654
• feat: fromJson? derivations now say where a parsing error occurred by @EdAyers in #1656
• feat: more conv goal structuring tactics by @digama0 in #1636
• fix: prefer longer parse even if unsuccessful by @Kha in #1658
• feat: hover for cases/induction case names by @digama0 in #1660
• fix: .ident hover in patterns by @digama0 in #1664
• fix: derive Repr missing a comma by @pcpthm in #1671
• feat: extend join point context pass by @hargoniX in #1676
• feat: RBMap simplifications by @digama0 in #1677
• chore: benchmark new compiler by @Kha in #1685
• fix: handle multi namespace/section in foldingRange and documentSymbol by @digama0 in #1680
• feat: make CustomInfo use Dynamic instead of Json by @EdAyers in #1662
• fix: replace highlight with diffTag by @EdAyers in #1666
• feat: add rbmap_fbip benchmark by @Kha in #1695
• doc: normalize Init.Conv docs by @Kha in #1667
• feat: improve expression diff by @EdAyers in #1699
• doc: Lean USize maps to C++ size_t, not usize_t by @dwrensha in #1704
• doc: fix link to initialization section in ffi section by @dwrensha in #1702
• fix: Clear Diagnostics when file is closed by @lovettchris in #1591
• fix: path normalization should not case-normalize entire path by @Kha in #1701
• fix: List.Mem should have two parameters by @digama0 in #1709
• FloatLetIn by @hargoniX in #1706
• doc: add question mark to LEAN_IDENT_RE by @lovettchris in #1713
• feat: go to duplicate definition by @digama0 in #1714
• feat: add implementation-detail hypotheses by @gebner in #1692
• feat: import command stub by @digama0 in #1716
• chore: replace let by have in stx matches by @gebner in #1720
• perf: improve Unhygienic.run code by @gebner in #1721
• test: benchmark workspace symbols search by @Kha in #1723
• chore: CI: cancel outdated workflows by @Kha in #1724
• feat: optional doc comment for register_simp_attr by @digama0 in #1726
• fix: hovers in appUnexpander attr by @digama0 in #1728
• chore: CI: make jobs actually cancellable by @Kha in #1731
• fix: improve fuzzy-matching heuristics by @rish987 in #1710
• Bump up to LLVM 15 by @bollu in #1691
• feat: unexpander for mkArray0 by @digama0 in #1727
• feat: function coercions with unification by @gebner in #1729
• chore: update stage0 by @gebner in #1733
• feat: basic compiler probing framework with examples by @hargoniX in #1734
• fix: 'AND' escaping for 'if(LLVM) ...' in 'src/shell' by @bollu in #1736
• chore: inline control primitives by @hargoniX in #1735
• chore: CI: exclude "full program" tests from debug/sanitized builds by @Kha in #1732
• chore: add Update changelog action by @Kha in #1742
• fix: dbg_trace tactic by @digama0 in #1747
• chore: remove #resolve_name by @digama0 in #1746
• Add dynamic quotations for syntax categories by @gebner in #1748
• doc: Option is a monad again by @PatrickMassot in #1751
• chore: snake-case attributes by @digama0 in #1752
• fix: environment leak on Windows by @awson in #1739
• fix: catch kernel exceptions in Kernel.{isDefEq, whnf} by @digama0 in #1757
• feat: CodeActionProvider by @EdAyers in #1661
• feat: Min/Max typeclasses by @gebner in #1765
• Erase common jp args by @hargoniX in #1754
• fix: jp context extender missed out on some variables by @hargoniX in #1766
• doc: fix some typos by @dwrensha in #1770
• feat: hovers & name resolution in registerCombinatorAttribute by @digama0 in #1771
• Add linter.deprecated option to silence deprecation warnings by @digama0 in #1768
• fix typo by @joaogui1 in #1769
• fix: add local Hashable instance by @ydewit in #1738
• fix: typo by @mcdoll in #1775
• doc: fix some typos by @dwrensha in #1776
• refactor: line wrapping in parser code by @digama0 in #1772
• refactor: instantiateTypeLevelParams in Lean by @gebner in #1761
• feat: use withoutPosition consistently by @digama0 in #1773
• fix: hoverableInfoAt? in presence of canonical syntax by @Kha in #1753
• fix: revert LLVM 15 bump on MacOS aarch64 by @digama0 in #1778
• fix: bug in level normalization (soundness bug) by @digama0 in #1781
• fix: missed a file from #1771 by @digama0 in #1782
• feat: improve import duplicate definition error by @gebner in #1786
• Make tokens in <|> relevant to syntax match by @Kha in #1744
• Fix typo in manual ToC by @david-christiansen in #1790
• feat: jp ctx extender after lambda lifting by @hargoniX in #1789
• fix: bug in replaceLocalDeclDefEq by @digama0 in #1794
• fix: formatting for if let and do if by @digama0 in #1788
• chore: revert "fix: revert LLVM 15 bump on MacOS aarch64" by @Kha in #1795
• fix: reorder goals after specialize by @semorrison in #1796
• feat: tweak behavior of congrN to match lean 3 by @digama0 in #1798
• chore: typo fix in error message of overlapping structure fields by @alexjbest in #1802
• feat: reduce precedence of unary neg to below pow by @alexjbest in #1803
• Add empty type ascription syntax (e :) by @digama0 in #1797
• Add hover/go-to-def/refs for options by @digama0 in #1783
• fix: improved error span for inherit_doc by @digama0 in #1807
• Update script/apply.lean by @Kha in #1810
• feat: allow doSeq in let x <- e | seq by @digama0 in #1809
• Require strict indentation in nested by-s by @AdrienChampion in #1811
• Introduce parser memoization to avoid exponentional behavior by @Kha in #1799
• refactor: split paren parser by @Kha in #1800
• chore: abort build on panic by @Kha in #1816
• chore: remove Int.natMod by @digama0 in #1819
• fix: protected on Nat.add_zero by @digama0 in #1817
• chore: protect Int.repr by @alexjbest in #1820
• chore: remove [Inhabited A] from binSearch / binInsert by @digama0 in #1784
• feat: elab_rules : conv by @digama0 in #1826
• doc: document Init.Data.Nat.Basic by @digama0 in #1827
• feat: add decl links for Quot via add_decl_doc by @digama0 in #1823
• fix: integer overflows by @Kha in #1832
• perf: optimize --deps --json by @Kha in #1833
• doc: mention ignoreLevelMVarDepth by @gebner in #1835
• fix: attribute info nesting by @digama0 in #1712
• feat: go to definition for KeyedDeclsAttributes by @digama0 in #1824
• fix: spacing in by_cases by @digama0 in #1838
• ElimDeadBranches for LCNF by @hargoniX in #1818
• doc: update widget docs by @EdAyers in #1839
• feat: implement workspace/applyEdit server request by @Kha in #1846
• chore: remove remnants of C++ format by @Kha in #1849
• fix: inconsistent use of precompiled symbols from interpreter on Windows by @Kha in #1843
• doc: document Init.Data.List.Basic by @digama0 in #1828
• fix: Nat.log2_terminates should not be private by @digama0 in #1857
• perf: pick cache size coprime to pointer alignment by @gebner in #1840
• Overhaul update-stage0 by @Kha in #1860
• feat: add LLVM C API bindings by @bollu in #1497
• fix: do method lifting across choice nodes by @Kha in #1847
• chore: fix typo in getNumBuiltiAttributes name by @alexjbest in #1864
• fix: print universe level lists in lean 4 style by @digama0 in #1865
• chore: CI: update all actions to avoid warnings by @Kha in #1873
• chore: make <;> left associative by @digama0 in #1875
• chore: bundle libatomic in releases by @gebner in #1877
• Update Lake to latest prerelease by @gebner in #1879
• fix: save correct environment in info tree for example by @Kha in #1880
• chore: change simp default to decide := false by @semorrison in #1888
• feat: add HashSet.insertMany by @semorrison in #1889
• feat: build libleanrt.bc with -O3 alwaysinline by @bollu in #1871
• perf: remove unnecessary, cache-defeating withPosition in doReassignArrow by @Kha in #1830
• feat: intra-line withPosition formatting by @digama0 in #1872
• refactor: revise server architecture by @Kha in #1884
• Optimizing multiplication and division operations of powers of 2 into shift operations. by @hargoniX in #1890
• fix: synthesize tc instances before propagating expected type by @gebner in #1893
• feat: infer def/theorem DefKind for let rec by @digama0 in #1866
• Work around VS Code completion bug by @Kha in #1885
• chore: protect Prod.Lex by @semorrison in #1895
• fix: do not ignore applicationTime in parametric attributes by @gebner in #1905
• Support dashes in field names by @gebner in #1896
• Replace all hashes by MurmurHash by @gebner in #1906
• chore: rename Prod.ext by @ChrisHughes24 in #1909
• chore: update Lake by @tydeu in #1912
• chore: ignore document version errors by @gebner in #1911
• refactor: consolidate MessageData constructors into lazy formatting with infos by @Kha in #1919
• feat: CI: capture core dumps by @gebner in #1925
• doc: update widget example by @Vtec234 in #1934
• fix: List.groupBy by @digama0 in #1941
• Make toString operations tail-recursive by @gebner in #1944
• fix: ignore empty character literals by @Kha in #1931
• fix: show correct goal state after an empty by by @Kha in #1930
• fix: protect against jumping over the stack guard page by @Kha in #1949
• fix: avoid mapping .oleans in the way of the stack by @Kha in #1950
• Fix typo (--ldlags) by @iacore in #1947
• fix: macro scopes in Conv.congr by @digama0 in #1955
• chore: add iff_self to simpOnlyBuiltins by @semorrison in #1936
• fix: disable memoize in pattern conv by @digama0 in #1956
• refactor: replace ignoreLevelMVarDepth by levelAssignDepth by @gebner in #1953
• Deterministic tests by @gebner in #1977
• Chain CoeOut instances during coercion resolution by @gebner in #1923
• fix: lsp change debouncing by @gebner in #1978
• fix: remove Inhabited Environment instance by @gebner in #1966
• fix: implement assertAfter using revert by @gebner in #1968
• Pretty-print signatures in hover and #check <ident> by @Kha in #1943
• Whitespace fixes in pretty-printer by @gebner in #1945
• Miscellaneous coercion fixes by @gebner in #1981
• feat: add derive handler for Nonempty by @gebner in #1983
• perf: avoid lifting ← over an if by @gebner in #1987
• [WIP] LLVM Backend by @bollu in #1837
• feat: add fun x ↦ y syntax by @gebner in #1984
• fix: avoid warning by dropping '#pragma once' by @tobiasgrosser in #2007
• feat: introduce custom leanSorryLike semantic token type for sorry, admit, stop by @Kha in #1976
• doc: replace maximum? in minimum? docstring by @gdahia in #2012
• LLVM: fix unboxed initializers by @bollu in #2015
• fix: be more careful with MatchResult.uncovered in syntax match by @Kha in #2008
• doc: Add more detail to the split tactic docs by @jeremysalwen in #1988
• feat: implement Uset for LLVM by @bollu in #2025
• fix: remove unnecessary hypothesis by @fgdorais in #1997
• feat Init.Data.Nat add simp attribute to mod_zero by @ChrisHughes24 in #1932
• chore: rename le_or_eq_or_le_succ by @chabulhwi in #2024
• fix: add done alternative to decreasing_with by @JamesGallicchio in #2019
• Include timings in trace messages when profiler is true by @Kha in #1995
• perf: do not backtrack after eta-defeq by @gebner in #2002
• refactor: redefine Nat.mod such that rfl : 0 % n = 0 by @eric-wieser in #2020
• feat: implement unreachable codegen for LLVM by @bollu in #2029
• chore: CI: do not cancel release job on master push by @Kha in #2030
• fix: metadata codegen for LLVM by @bollu in #2031
• Provide context info in interactive goals by @Vtec234 in #1969
• feat: funext no arg tactic by @JamesGallicchio in #2027
• chore: remove unused isTaggedPtr from IR. by @bollu in #2032
• feat: add --target flag for LLVM backend to build objects of a different architecture by @bollu in #2034
• doc: improve documentation of MetavarContext.lean by @rish987 in #1625
• fix: binop% info tree by @Kha in #1903
• fix: show tactic info on canonical by by @Kha in #2039
• fix: fuzzy-find bonus for matching last characters of pattern and symbol by @rish987 in #1917
• Make go-to-definition on a typeclass projection application go to the instance(s) by @rish987 in #1767
• Expr docs fix by @lakesare in #2047
• fix: catch missing exceptions in kernel by @gebner in #2036
• Fixes for SMALL_ALLOCATOR=OFF by @gebner in #2059
• chore: CI: avoid deprecated set-output by @Kha in #2062
• fix: notation unexpander on overapplication of non-nullary notation by @Kha in #2046
• Info tree absence fixes by @Kha in #2016
• fix: disable gmp on windows by @gebner in #2067
• fix: unify types in calc by @gebner in #2066
• chore: fix typos by @int-y1 in #2069
• chore: update Lake by @tydeu in #2070
• doc: update FPiL entry in README by @Kha in #2078
• chore: update Lake by @tydeu in #2081
• fix: reenable structure eta during tc search by @gebner in #2093
• feat : add quot_precheck Lean.Parser.Term.explicit by @joneugster in #2098
• fix: unify goal before executing nested tactics in calc by @gebner in #2100
• perf: whnf projections during defeq by @gebner in #2003
• Profiler fixes without regressions by @Kha in #2106
• fix unintuitive calc indentation by @AdrienChampion in #1844
• fix: reject occurrences of inductive type in index by @gebner in #2127
• doc: typo by @madvorak in #2133
• Miscellaneous TC fixes by @gebner in #2142
• feat: profile tactic execution by @Kha in #2101
• chore: discuss alternative calc syntax in RELEASES.md by @AdrienChampion in #2124
• chore: fix typos in prelude by @int-y1 in #2118
• Fix leaking of file descriptors into spawned processes by @Kha in #2138
• fix: ignore vanishing files during watchdog update by @Kha in #2144
• Even more profile metrics by @Kha in #2149
• perf: scale Expr.replace cache with input size by @Kha in #2151
• Cache more type class queries by @gebner in #2152
• doc: fix typos by @pitmonticone in #2160
• chore: fix typos by @int-y1 in #2168
• Show typeclass and tactic names in profile output by @Kha in #2170
• fix: update nix files to use strings instead of URL literals by @ConnorBaker in #2172
• Docstring for Int and its basic operations by @AdrienChampion in #2167
• fix: respect pp.raw in interactive .ofGoal by @gebner in #2176
• fix: modify buildLeanPackage.nix for huge deps by @enricozb in #2179
• doc: heading by @chabulhwi in #2180
• fix: advance pointer into array when generating random bytes by @olitb in #2185
• Add structured trace profiler by @Kha in #2181
• feat: reorder tc subgoals according to out-params by @gebner in #2174
• fix: reset local context in mkInjectiveTheorems by @gebner in #2190
• chore: add missing simp lemma (¬ False) = True by @semorrison in #2182
• fix: simp: strip mdata when testing for True/False by @gebner in #2177
• fix: match discriminant reduction should not unfold irreducible defs by @Kha in #2162
• feat: add timing profiling to the new compiler by @hargoniX in #2187
• feat: profiling of linters by @hargoniX in #2196
• chore: update Lake by @gebner in #2198
• doc: uncapitalize a letter by @chabulhwi in #2201
• fix: remove private from string defs by @digama0 in #2205
• fix: LCNF simp forgot to mark normalized decls as simplified by @hargoniX in #2148
• doc: f(x) is no longer allowed by @madvorak in #2135
• fix: change the type of Quotient.ind by @chabulhwi in #2114
• fix: use snake case for @[code_action_provider] by @digama0 in #2209
• fix: bug in reference implementation of String.get? by @digama0 in #2213
• Skip proof arguments during unification, and try structure eta last by @gebner in #2210
• fix: offset unification with a+a+1 by @gebner in #2146
• chore: lower monad for Term.reportUnsolvedGoals by @semorrison in #2206
• fix: remove repeat calls to inferType in ignoreField by @cppio in #2056
• fix: stop iterating over visited mvars in collectUnassignedMVars by @cppio in #2057
• fix: use withoutPosition in anon constructor by @digama0 in #2216
• doc: add docstring to String.next' by @chabulhwi in #2234
• fix: implement String.toName using decodeNameLit by @digama0 in #2233
• fix: ignore implDetail hyps in withLocation by @JLimperg in #2219
• feat: add compiler.enableNew for the new compiler by @hargoniX in #2075
• fix: spacing and indentation fixes by @digama0 in #2240
• fix: infinite loop in isClassApp? by @digama0 in #2245
• chore: update Lake by @Kha in #2241
• style: remove whitespace by @chabulhwi in #2244
• feat: trace nodes for kernel type checking by @hargoniX in #2211
• fix: spacing around calc by @digama0 in #2251
• feat: implement have this by @digama0 in #2247
• fix: prefer resolving parser alias over declaration by @Kha in #2253
• add ₚ to lstlean.tex by @odanoburu in #2221
• fix: interpret initializers in order by @Kha in #2256
• feat: remove partial in Init.Data.String.Basic by @digama0 in #2214
• doc: improve documentation of Init.Coe by @chabulhwi in #2107
• fix: save when used as last tactic by @Kha in #2259
• fix: hygieneInfo should not consume whitespace by @digama0 in #2262
• feat: binder info for generalize by @digama0 in #2261
• feat: report section name in invalid end msg by @digama0 in #2255
• fix: simp: synthesize non-inst-implicit tc args by @gebner in #2266
• fix: misleading indentation by @digama0 in #2270
• fix: use Lean.initializing instead of IO.initializing by @digama0 in #2269
• feat: allow upper case single character identifiers when relaxedAutoImplicit false by @semorrison in #2277
• feat: add flag for apply to defer failed typeclass syntheses as goals by @semorrison in #2274
• fix: incorrect type for SpecInfo.argKinds by @digama0 in #2280
• fix: delete Measure and SizeOfRef by @fpvandoorn in #2275
• fix: basic ident fallback in identComponents by @digama0 in #2268
• doc: fix typos by @pitmonticone in #2287
• chore: compact objects in post-order by @digama0 in #2286
• chore: update Lake by @tydeu in #2296
• fix: reference implementation for Array.mapM by @digama0 in #2295
• Update quickstart by @Kha in #2294
• fix: add missing instantiateMVars by @Vtec234 in #2290
• feat: trace nodes for SizeOf and injectivity theorem generation by @Kha in #2272
• chore: update Lake by @tydeu in #2303
• Clarify status of release process by @Kha in #2304
• fix: lazy_binop + coercion bug by @digama0 in #2301
• Kill descendant processes on worker exit by @Kha in #2307
• fix: don't run [builtin_init] when builtin = false by @digama0 in #2314
• fix: calling convention for module initializers by @digama0 in #2313
• feat: use nat_pow in the kernel by @semorrison in #2310
• chore: fix Int.div docstring examples by @AdrienChampion in #2315
• Compile against glibc 2.26 by @Kha in #2316
• perf: pointer set by @leodemoura in #2318
• Do not use GMP on ARM Linux by @Kha in #2319
• doc: document generating releases via tags by @semorrison in #2302
• feat: relax test in checkLocalInstanceParameters to allow instance implicits by @semorrison in #2312
• fix: fixes #2321 by @leodemoura in #2322
• chore: write "|-" as "|" noWs "-" by @fpvandoorn in #2299
• chore: update Lake by @tydeu in #2323
• Transfer Lake into repo by @Kha in #2155
• fix: fixes #2327 by @leodemoura in #2331
• fix: protect sizeOf lemmas by @fgdorais in #2332
• doc: fix contradictory docstring by @Vtec234 in #2264
• refactor: redefine String.splitOnAux by @chabulhwi in #2271
• chore: better error message for loose bvar in whnf by @JLimperg in #2338
• Allow linking against Lake by @Kha in #2337
• doc: fix type signature of Coe by @chabulhwi in #2342
• feat: add IO.FS.rename by @digama0 in #2345
• style: remove unnecessary space by @chabulhwi in #2347
• perf: dont repeatedly elab term in rw at multiple locations by @alexjbest in #2317
• feat: LLVM backend: support for visibility Style & DLL storage by @bollu in #2354
• macOS linker fixes by @Kha in #2356
• fix: repeat conv should not auto-close the goal by @digama0 in #2357
• chore: Nix bump to LLVM 15 by @bollu in #2365
• fix: missing mkCIdents in Lean.Elab.Deriving.Util by @Kha in #2352
• Auto-complete declaration names in arbitrary namespaces by @Kha in #2351
• fix: handle error in withTraceNode message action by @Vtec234 in #2364
• chore: revert #2317 by @semorrison in #2366
• Avoid syntax stack copy at orelseFn by @Kha in #2306
• chore: disable lake 116 test. by @bollu in #2358
• perf: faster replace "\r\n" "\n" by @digama0 in #2369
• fix: do not unnecessarily wait on additional snapshot in server request handlers by @Kha in #2370
• chore: get rid of all inline C annotations for LLVM by @bollu in #2363
• chore: Lake touchups by @tydeu in #2377
• chore: avoid "unused parameter" warnings in lean.h by @Kha in #2375
• chore: more Lake touchups by @tydeu in #2380
• chore: correct doc-string for elabTerm by @semorrison in #2378
• fix: lake: do not hash remote dep names by @tydeu in #2383
• test: reverse FFI from C with Lake by @Kha in #2381
• fix: correct universe polymorphism in Lean.instFromJsonProd by @eric-wieser in #2382
• chore: make Lean build shell configurable by @tydeu in #2386
• test: update parser benchmark, add to speedcenter suite by @Kha in #2392
• test: lake: make 116 deterministic & related tweaks by @tydeu in #2384
• feat: lake.lock file for builds by @tydeu in #2385
• feat: lake clean [<pkgs>...] & other touchups by @tydeu in #2396
• doc: writing good tests by @Kha in #2394
• doc: fix comment for Nat.sub by @marcusrossel in #2399
• fix: generalize Prod.lexAccessible to match Lean 3 by @alreadydone in #2388
• feat: lake: lean lib extraDepTargets & related tweaks by @tydeu in #2401
• fix: lake: lock test timeout + README typos by @tydeu in #2404
• fix: delete lake.lock on error & test by @tydeu in #2406
• doc: one more enableInitializersExecution remark by @Kha in #2411
• LLVMBindings.lean & llvm.cpp updates for Linkage by @hargoniX in #2410
• chore: remove trailing whitespace in EmitLLVM by @tobiasgrosser in #2417
• Remove trailing whitespaces in CMakeLists.txt by @tobiasgrosser in #2418
• feat: add failIfUnchanged flag to simp by @semorrison in #2334
• LLVM CI by @hargoniX in #2416
• doc: IO.Process.getPID tweak + IO.FS.Mode by @tydeu in #2400
• feat: lake update <pkg> & related tweaks by @tydeu in #2405
• feat: LLVM backend: implement the equivalent of -fstack-clash-protection by @hargoniX in #2376
• fix: lake: reverse-ffi, manifest, and 62 tests by @tydeu in #2424
• feat: warn on local changes to dependency & related fixes by @tydeu in #2425
• fix: interpret module initializer at most once by @Kha in #2423
• feat: turning on failIfUnchanged by default in simp by @semorrison in #2336
• doc: fix markup in IO.RealWorld by @nomeata in #2430
• feat: warn rather than error if lake.lock disappears by @tydeu in #2432
• fix: FFI signature mismatches by @Kha in #2433

New Contributors

• @neelance made their first contribution in #1508
• @fynnsu made their first contribution in #1514
• @eyelash made their first contribution in #1577
• @jpablo made their first contribution in #1602
• @alexjbest made their first contribution in #1605
• @dwrensha made their first contribution in #1704
• @rish987 made their first contribution in #1710
• @awson made their first contribution in #1739
• @joaogui1 made their first contribution in #1769
• @mcdoll made their first contribution in #1775
• @david-christiansen made their first contribution in #1790
• @AdrienChampion made their first contribution in #1811
• @ChrisHughes24 made their first contribution in #1909
• @iacore made their first contribution in #1947
• @tobiasgrosser made their first contribution in #2007
• @gdahia made their first contribution in #2012
• @jeremysalwen made their first contribution in #1988
• @chabulhwi made their first contribution in #2024
• @JamesGallicchio made their first contribution in #2019
• @eric-wieser made their first contribution in #2020
• @lakesare made their first contribution in #2047
• @int-y1 made their first contribution in #2069
• @joneugster made their first contribution in #2098
• @madvorak made their first contribution in #2133
• @pitmonticone made their first contribution in #2160
• @enricozb made their first contribution in #2179
• @olitb made their first contribution in #2185
• @cppio made their first contribution in #2056
• @odanoburu made their first contribution in #2221
• @fpvandoorn made their first contribution in #2275
• @alreadydone made their first contribution in #2388

Full Changelog: v4.0.0-m5...v4.0.0-rc1