v4.0.0-rc1
Pre-release
Pre-release
·
7133 commits
to master
since this release
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 | altby @digama0 in #1455 - Drop last type parameter of
RpcEncodingby @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_uint8to 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.toStringby @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.transformAPI 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:
dbgStackTraceby @Kha in #1515 - Document, fix EOF behavior by @Kha in #1503
- fix: @[inheritDoc] on notation by @digama0 in #1523
- chore: remove
def impliesby @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 uuniverses 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
doextensions by @Kha in #1589 - doc: document Init.Data.Queue by @digama0 in #1583
- feat: allow optional type in
exampleby @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
caseby @digama0 in #1628 - feat:
injectionswith 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
deltaby @digama0 in #1630 - feat:
if _ : cond then t else esyntax 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 hby @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/inductioncase names by @digama0 in #1660 - fix:
.identhover 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.Memshould 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:
importcommand stub by @digama0 in #1716 - chore: replace let by have in stx matches by @gebner in #1720
- perf: improve
Unhygienic.runcode 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_attrby @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_tracetactic by @digama0 in #1747 - chore: remove
#resolve_nameby @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.deprecatedoption 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
withoutPositionconsistently 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 letanddo ifby @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
congrNto 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_docby @digama0 in #1807 - Update script/apply.lean by @Kha in #1810
- feat: allow
doSeqinlet x <- e | seqby @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.natModby @digama0 in #1819 - fix:
protectedonNat.add_zeroby @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 : convby @digama0 in #1826 - doc: document Init.Data.Nat.Basic by @digama0 in #1827
- feat: add decl links for
Quotviaadd_decl_docby @digama0 in #1823 - fix: integer overflows by @Kha in #1832
- perf: optimize
--deps --jsonby @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_casesby @digama0 in #1838 - ElimDeadBranches for LCNF by @hargoniX in #1818
- doc: update widget docs by @EdAyers in #1839
- feat: implement
workspace/applyEditserver request by @Kha in #1846 - chore: remove remnants of C++
formatby @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_terminatesshould 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
exampleby @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
withPositionindoReassignArrowby @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 recby @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
MessageDataconstructors 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
byby @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
ignoreLevelMVarDepthbylevelAssignDepthby @gebner in #1953 - Deterministic tests by @gebner in #1977
- Chain
CoeOutinstances during coercion resolution by @gebner in #1923 - fix: lsp change debouncing by @gebner in #1978
- fix: remove
Inhabited Environmentinstance 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 β¦ ysyntax by @gebner in #1984 - fix: avoid warning by dropping '#pragma once' by @tobiasgrosser in #2007
- feat: introduce custom
leanSorryLikesemantic token type forsorry,admit,stopby @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.uncoveredin syntax match by @Kha in #2008 - doc: Add more detail to the
splittactic docs by @jeremysalwen in #1988 - feat: implement
Usetfor 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_succby @chabulhwi in #2024 - fix: add done alternative to
decreasing_withby @JamesGallicchio in #2019 - Include timings in trace messages when
profileris true by @Kha in #1995 - perf: do not backtrack after eta-defeq by @gebner in #2002
- refactor: redefine
Nat.modsuch thatrfl : 0 % n = 0by @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:
funextno 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.leanby @rish987 in #1625 - fix:
binop%info tree by @Kha in #1903 - fix: show tactic info on canonical
byby @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
Exprdocs 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-outputby @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_precheckLean.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
calcindentation 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
calcsyntax inRELEASES.mdby @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.replacecache 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
Intand 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:
matchdiscriminant 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
privatefrom 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.indby @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
inferTypeinignoreFieldby @cppio in #2056 - fix: stop iterating over visited mvars in
collectUnassignedMVarsby @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
calcby @digama0 in #2251 - feat: implement
have thisby @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
partialin Init.Data.String.Basic by @digama0 in #2214 - doc: improve documentation of
Init.Coeby @chabulhwi in #2107 - fix:
savewhen 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.initializinginstead ofIO.initializingby @digama0 in #2269 - feat: allow upper case single character identifiers when relaxedAutoImplicit false by @semorrison in #2277
- feat: add flag for
applyto defer failed typeclass syntheses as goals by @semorrison in #2274 - fix: incorrect type for
SpecInfo.argKindsby @digama0 in #2280 - fix: delete Measure and SizeOfRef by @fpvandoorn in #2275
- fix: basic ident fallback in
identComponentsby @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
SizeOfand 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.divdocstring 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.splitOnAuxby @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
Coeby @chabulhwi in #2342 - feat: add
IO.FS.renameby @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:
repeatconv 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
orelseFnby @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.instFromJsonProdby @eric-wieser in #2382 - chore: make Lean build shell configurable by @tydeu in #2386
- test: update
parserbenchmark, add to speedcenter suite by @Kha in #2392 - test: lake: make 116 deterministic & related tweaks by @tydeu in #2384
- feat:
lake.lockfile 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.subby @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.lockon error & test by @tydeu in #2406 - doc: one more
enableInitializersExecutionremark 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.getPIDtweak +IO.FS.Modeby @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.lockdisappears 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