v4.4.0

Changes since v4.3.0 (from RELEASES.md)

• Lake and the language server now support per-package server options using the moreServerOptions config field, as well as options that apply to both the language server and lean using the leanOptions config field. Setting either of these fields instead of moreServerArgs ensures that viewing files from a dependency uses the options for that dependency. Additionally, moreServerArgs is being deprecated in favor of the moreGlobalServerArgs field. See PR #2858.

  A Lakefile with the following deprecated package declaration:

  def moreServerArgs := #[
    "-Dpp.unicode.fun=true"
  ]
  def moreLeanArgs := moreServerArgs
  
  package SomePackage where
    moreServerArgs := moreServerArgs
    moreLeanArgs := moreLeanArgs

  ... can be updated to the following package declaration to use per-package options:

  package SomePackage where
    leanOptions := #[⟨`pp.unicode.fun, true⟩]

• Rename request handler.

• Import auto-completion.

• `pp.beta`` to apply beta reduction when pretty printing.

• Embed and check githash in .olean.

• Guess lexicographic order for well-founded recursion.

• Allow trailing comma in tuples, lists, and tactics.

Bug fixes for #2628, #2883 #2810, #2925, and #2914.

Lake:

• lake init . and a bare lake init and will now use the current directory as the package name. #2890
• lake new and lake init will now produce errors on invalid package names such as .., foo/bar, Init, Lean, Lake, and Main. See issue #2637 and PR #2890.
• lean_lib no longer converts its name to upper camel case (e.g., lean_lib bar will include modules named bar.* rather than Bar.*). See issue #2567 and PR #2889.
• Lean and Lake now properly support non-identifier library names (e.g., lake new 123-hello and import «123Hello» now work correctly). See issue #2865 and PR #2889.
• Lake now filters the environment extensions loaded from a compiled configuration (lakefile.olean) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via elab in configurations). See issue #2632 and PR #2896.
• Cloud releases will now properly be re-unpacked if the build directory is removed. See PR #2928.
• Lake's math template has been simplified. See PR #2930.
• lake exe <target> now parses target like a build target (as the help text states it should) rather than as a basic name. For example, lake exe @mathlib/runLinter should now work. See PR #2932.
• lake new foo.bar [std] now generates executables named foo-bar and lake new foo.bar exe properly creates foo/bar.lean. See PR #2932.
• Later packages and libraries in the dependency tree are now preferred over earlier ones. That is, the later ones "shadow" the earlier ones. Such an ordering is more consistent with how declarations generally work in programming languages. This will break any package that relied on the previous ordering. See issue #2548 and PR #2937.
• Executable roots are no longer mistakenly treated as importable. They will no longer be picked up by findModule?. See PR #2937.

Full Changelog: v4.3.0...v4.4.0

v4.4.0-rc1

Changes since v4.3.0 (from RELEASES.md):

• Lake and the language server now support per-package server options using the moreServerOptions config field, as well as options that apply to both the language server and lean using the leanOptions config field. Setting either of these fields instead of moreServerArgs ensures that viewing files from a dependency uses the options for that dependency. Additionally, moreServerArgs is being deprecated in favor of the moreGlobalServerArgs field. See PR #2858.

  A Lakefile with the following deprecated package declaration:

  def moreServerArgs := #[
    "-Dpp.unicode.fun=true"
  ]
  def moreLeanArgs := moreServerArgs
  
  package SomePackage where
    moreServerArgs := moreServerArgs
    moreLeanArgs := moreLeanArgs

  ... can be updated to the following package declaration to use per-package options:

  package SomePackage where
    leanOptions := #[⟨`pp.unicode.fun, true⟩]

• Rename request handler.

• Import auto-completion.

• pp.beta to apply beta reduction when pretty printing.

• Embed and check githash in .olean.

• Guess lexicographic order for well-founded recursion.

• Allow trailing comma in tuples, lists, and tactics.

Bug fixes for #2628, #2883,
#2810, #2925, and #2914.

Lake:

• lake init . and a bare lake init and will now use the current directory as the package name. #2890
• lake new and lake init will now produce errors on invalid package names such as .., foo/bar, Init, Lean, Lake, and Main. See issue #2637 and PR #2890.
• lean_lib no longer converts its name to upper camel case (e.g., lean_lib bar will include modules named bar.* rather than Bar.*). See issue #2567 and PR #2889.
• Lean and Lake now properly support non-identifier library names (e.g., lake new 123-hello and import «123Hello» now work correctly). See issue #2865 and PR #2889.
• Lake now filters the environment extensions loaded from a compiled configuration (lakefile.olean) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via elab in configurations). See issue #2632 and PR #2896.
• Cloud releases will now properly be re-unpacked if the build directory is removed. See PR #2928.
• Lake's math template has been simplified. See PR #2930.
• lake exe <target> now parses target like a build target (as the help text states it should) rather than as a basic name. For example, lake exe @mathlib/runLinter should now work. See PR #2932.
• lake new foo.bar [std] now generates executables named foo-bar and lake new foo.bar exe properly creates foo/bar.lean. See PR #2932.
• Later packages and libraries in the dependency tree are now preferred over earlier ones. That is, the later ones "shadow" the earlier ones. Such an ordering is more consistent with how declarations generally work in programming languages. This will break any package that relied on the previous ordering. See issue #2548 and PR #2937.
• Executable roots are no longer mistakenly treated as importable. They will no longer be picked up by findModule?. See PR #2937.

Pull requests merged:

• chore: update release notes after v4.3.0-rc2 by @semorrison in #2891
• chore: Issue template: Suggest #eval Lean.versionString by @nomeata in #2884
• fix: support non-identifier library names by @tydeu in #2888
• refactor: lake: use plain lib name for root and native name by @tydeu in #2889
• feat: bare lake init & validated pkg names by @tydeu in #2890
• Allow trailing comma in tuples, lists, and tactics by @vleni in #2643
• chore: syntax documentation for universe, open, export, variable by @AdrienChampion in #2645
• fix: lake: whitelist loaded config olean env exts by @tydeu in #2896
• chore: ignore forgotten Lake test artifacts by @tydeu in #2886
• doc: fix typos by @marcusrossel in #2915
• fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument by @kmill in #2918
• doc: release notes for recent lake fixes by @tydeu in #2906
• fix: PackMutual: Deal with extra arguments by @nomeata in #2892
• feat: Lean.MVarId.cleanup configuration by @kmill in #2919
• feat: helpful error message about supportInterpreter by @semorrison in #2912
• doc: Adjust contributor's docs to squash merging by @nomeata in #2927
• feat: rename request handler by @digama0 in #2462
• doc: mention dite in ite docstring by @AdrienChampion in #2924
• fix: eq_refl tactic’s name is eqRefl by @nomeata in #2911
• refactor: WF.Fix: Pass all remaining goals to Term.reportUnsolvedGoals by @nomeata in #2922
• chore: run CI on merge_group by @semorrison in #2948
• fix: most-recently-nightly-tag does not assume a 'nightly' remote by @semorrison in #2947
• fix: Use whnf for mutual recursion with types hiding → by @nomeata in #2926
• chore: CI: pin macos-11 to work around 12.7.1 breakage by @Kha in #2946
• fix: Float RecApp out of applications by @nomeata in #2818
• fix: PackMutual: Eta-Expand as needed by @nomeata in #2902
• chore: script/most-recent-nightly-tag uses https rather than ssh repo URL by @semorrison in #2951
• chore: Run CI on all PRs, even base ≠ master by @nomeata in #2955
• doc: Markdown fixes in Lean.Expr by @nomeata in #2956
• feat: import auto-completion by @mhuisi in #2904
• chore: remove unused MonadBacktrack instance for SimpM by @semorrison in #2943
• feat: pp.beta to apply beta reduction when pretty printing by @kmill in #2864
• feat: per-package server options by @mhuisi in #2858
• fix: ignore errors on IO.FS.Handle finalization by @Kha in #2935
• feat: embed and check githash in .olean by @Kha in #2766
• fix: missing withContext in simp trace by @digama0 in #2053
• feat: Add MatcherApp. and CasesOnApp.refineThrough by @nomeata in #2882
• fix: untar cloud release if no build dir by @tydeu in #2928
• fix: lake: proper exe targets & pkg generation by @tydeu in #2932
• refactor: reverse pkg/lib search & no exe roots in import by @tydeu in #2937
• feat: Guess lexicographic order for well-founded recursion by @nomeata in #2874
• refactor: lake: simplify math template & test it by @tydeu in #2930
• doc: release notes for recent lake changes by @tydeu in #2938
• feat: WF.GuessLex: If there is only one plausible measure, use it by @nomeata in #2954
• fix: remove unnecessary step in pr-release.yml by @semorrison in #2976
• chore: Check PR title, not commit, for commit convention by @nomeata in #2978
• chore: CI: Create an all-builds-ok job by @nomeata in https://github.com/leanprover/lean4/pul...

v4.3.0

Changes since 4.2.0 (from RELEASES.md)

• simp [f] does not unfold partial applications of f anymore. See issue #2042.
  To fix proofs affected by this change, use unfold f or simp (config := { unfoldPartialApp := true }) [f].

• By default, simp will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by simp, and the decide tactic may be useful in such cases. The decide simp configuration option can be used to locally restore the old simp behavior, as in simp (config := {decide := true}); this includes using Decidable instances to verify side goals such as numeric inequalities.

• Many bug fixes:

  • Add left/right actions to term tree coercion elaborator and make `^`` a right action
  • Fix for #2775, don't catch max recursion depth errors
  • Reduction of Decidable instances very slow when using cases tactic
  • simp not rewriting in binder
  • simp unfolding let even with zeta := false option
  • simp (with beta/zeta disabled) and discrimination trees
  • unknown free variable introduced by rw ... at h
  • dsimp doesn't use rfl theorems which consist of an unapplied constant
  • dsimp does not close reflexive equality goals if they are wrapped in metadata
  • rw [h] uses h from the environment in preference to h from the local context
  • missing withAssignableSyntheticOpaque for assumption tactic
  • ignoring default value for field warning

• Cancel outstanding tasks on document edit in the language server.

• Remove unnecessary % operations in Fin.mod and Fin.div

• Avoid DecidableEq in Array.mem

• Ensure USize.size unifies with ?m + 1

• Improve compatibility with emacs eglot client

Lake:

• Sensible defaults for lake new MyProject math
• Changed postUpdate? configuration option to a post_update declaration. See the post_update syntax docstring for more information on the new syntax.
• A manifest is automatically created on workspace load if one does not exists..
• The := syntax for configuration declarations (i.e., package, lean_lib, and lean_exe) has been deprecated. For example, package foo := {...} is deprecated.
• support for overriding package URLs via LAKE_PKG_URL_MAP
• Moved the default build directory (e.g., build), default packages directory (e.g., lake-packages), and the compiled configuration (e.g., lakefile.olean) into a new dedicated directory for Lake outputs, .lake. The cloud release build archives are also stored here, fixing #2713.
• Update manifest format to version 7 (see lean4#2801 for details on the changes).
• Deprecate the manifestFile field of a package configuration.
• There is now a more rigorous check on lakefile.olean compatibility (see #2842 for more details).

Pull requests merged:

• chore: lake: simplify config decl syntax by @tydeu in #2705
• feat: lake: run_io to execute IO at term elab time by @tydeu in #2707
• feat: add Simp.Config.ground for simplifying nested ground terms by @leodemoura in #2715
• Lake: A manifest is automatically created on workspace load if one does not exists. by @tydeu in #2680
• refactor: change postUpdate? config to a decl by @tydeu in #2723
• fix: allow constants to be marked for dsimp by @thorimur in #2686
• chore: remove unnecessary % operations at Fin.mod and Fin.div by @leodemoura in #2688
• fix: fixes #2552 by @leodemoura in #2730
• fix: fixes #1926 by @leodemoura in #2732
• fix: don't pack ._ files on MacOS by @digama0 in #2743
• chore: remove "paper cut" when using Fin USize.size by @leodemoura in #2724
• chore: typos by @semorrison in #2746
• fix: version numbers in code actions by @bustercopley in #2721
• fix: add instantiateMVars to replaceLocalDecl by @thorimur in #2712
• fix: rw ... at h unknown fvar bug by @thorimur in #2728
• Update contribution guides by @DenisGorbachev in #2624
• feat: LAKE_PKG_URL_MAP by @tydeu in #2709
• fix: issues #2669 #2281 by @leodemoura in #2734
• Cancel outstanding tasks on document edit in the language server, second edition by @Kha in #2714
• chore: update 'nightly' branch to track nightly releases by @semorrison in #2767
• chore: run CI against the head of the branch, not a virtual merge with master by @semorrison in #2769
• feat: Sensible defaults arguments for math project by @PatrickMassot in #2770
• fix: dsimp missing consumeMData when closing goals by rfl by @kmill in #2776
• doc: fix a link in developent documentation by @ericrbg in #2780
• feat: Array.mem: Avoid DecidableEq, set up decreasing_trivial by @nomeata in #2774
• fix: replace DecidableEq with BEq/LawfulBEq in List mem theorems by @cppio in #2041
• fix: make rw [foo] look in the local context for foo before it looks in the environment by @thorimur in #2738
• feat: withAssignableSyntheticOpaque in assumption by @semorrison in #2596
• fix: fixes #2178 by @leodemoura in #2784
• doc: complete release notes for v4.3.0-rc1 by @semorrison in #2791
• chore: begin development cycle for v4.4.0 by @semorrison in #2792
• feat: reorder Lake help by @semorrison in #2725
• fix: lake: consistent order for manifest packages by @tydeu in #2788
• chore: fix duplication in release notes by @semorrison in #2794
• chore: change simp default to decide := false by @collares in #2722
• feat: use nightly-testing-YYYY-MM-DD branches on Mathlib for testing PRs, and be more conservative about launching Mathlib CI by @semorrison in #2798
• chore: fix to Mathlib combined CI by @semorrison in #2804
• chore: fix to Mathlib combined CI by @semorrison in #2806
• doc: Add docstrings to dbg_trace and assert! in do blocks by @nomeata in #2787
• chore: don't run irrelevant CI steps by @semorrison in #2807
• chore: force push to nightly branch when making nightly-YYYY-MM-DD tags by @semorrison in #2808
• feat: hovers on open and export decls by @digama0 in #2797
• Teach CMake about LLVM builds by @hargoniX in #2809
• chore: more adjustments to new CI scripts by @semorrison in #2811
• fix: fixes #2775 by @leodemoura in #2790
• chore: still fixing Mathlib CI by @semorrison in #2817
• perf: avoid quadratic number of info tree nodes in DecEq deriving handler by @Kha in #2820
• feat: Better error location in structural recursion by @nomeata in #2819
• chore: add Mathlib CI comments using the mathlib bot by @semorrison in #2824
• chore: fix identification of most recent nightly tag by @semorrison in #2827
• chore: use flow control rather than exit codes in CI scripts by @semorrison in #2828
• fix: Escape ? in C literal strings to avoid trigraphs by @nomeata in https://github.com/leanprover/lean4/pul...

v4.3.0-rc2

What's Changed

• feat: reorder Lake help by @semorrison in #2725
• fix: lake: consistent order for manifest packages by @tydeu in #2788
• chore: fix duplication in release notes by @semorrison in #2794
• chore: change simp default to decide := false by @collares in #2722
• doc: Add docstrings to dbg_trace and assert! in do blocks by @nomeata in #2787
• feat: hovers on open and export decls by @digama0 in #2797
• Teach CMake about LLVM builds by @hargoniX in #2809
• fix: fixes #2775 by @leodemoura in #2790
• perf: avoid quadratic number of info tree nodes in DecEq deriving handler by @Kha in #2820
• feat: Better error location in structural recursion by @nomeata in #2819
• fix: Escape ? in C literal strings to avoid trigraphs by @nomeata in #2833
• test: C trigraph by @nomeata in #2832
• doc: mention the proof-binding syntax in match by @eric-wieser in #2834
• Ensure nested proofs in equation and unfold lemmas have been abstracted by @leodemoura in #2825
• chore: add import Lean benchmark by @Kha in #2840
• feat: extend API of KVMap by @semorrison in #2851
• feat: Lean.Linter.logLintIf by @semorrison in #2852
• fix: issue 2042 by @leodemoura in #2783
• doc: fix typo by @marcusrossel in #2856
• refactor: TerminationHint: Remove duplicted code line by @nomeata in #2859
• feat: find Decidable instances via unification by @semorrison in #2816
• feat: add left/right actions to term tree coercion elaborator and make ^ a right action by @kmill in #2778
• refactor: .lake directory for Lake outputs by @tydeu in #2749
• Mark environments not freed before process exit persistent eagerly by @Kha in #2841
• fix: re-read HTTP header when skipping notification in Ipc.readResponseAs by @Kha in #2870
• fix: have parenthesizer copy source info to parenthesized term by @kmill in #2866
• doc: fix typo by @eric-wieser in #2878
• refactor: lake: more flexible manifest by @tydeu in #2801
• feat: release web assembly by @abentkamp in #2855
• doc: code owners by @Kha in #2875
• fix: stricter lakefile.olean compatibility check by @tydeu in #2842

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

v4.3.0-rc1

• Many bug fixes:
  • Reduction of Decidable instances very slow when using cases tactic
  • simp not rewriting in binder
  • simp unfolding let even with zeta := false option
  • simp (with beta/zeta disabled) and discrimination trees
  • unknown free variable introduced by rw ... at h
  • dsimp doesn't use rfl theorems which consist of an unapplied constant
  • dsimp does not close reflexive equality goals if they are wrapped in metadata
  • rw [h] uses h from the environment in preference to h from the local context
  • missing withAssignableSyntheticOpaque for assumption tactic
  • ignoring default value for field warning
• Cancel outstanding tasks on document edit in the language server.
• Remove unnecessary % operations in Fin.mod and Fin.div
• Avoid DecidableEq in Array.mem
• Ensure USize.size unifies with ?m + 1
• Improve compatibility with emacs eglot client

Lake:

• Sensible defaults for lake new MyProject math
• Changed postUpdate? configuration option to a post_update declaration. See the post_update syntax docstring for more information on the new syntax.
• A manifest is automatically created on workspace load if one does not exists..
• The := syntax for configuration declarations (i.e., package, lean_lib, and lean_exe) has been deprecated. For example, package foo := {...} is deprecated.
• support for overriding package URLs via LAKE_PKG_URL_MAP

v4.2.0

v4.2.0

• isDefEq cache for terms not containing metavariables..
• Make Environment.mk and Environment.add private, and add replay as a safer alternative.
• IO.Process.output no longer inherits the standard input of the caller.
• Do not inhibit caching of default-level match reduction.
• List the valid case tags when the user writes an invalid one.
• The derive handler for DecidableEq now handles mutual inductive types.
• Show path of failed import in Lake.
• Fix linker warnings on macOS.
• Lake: Add postUpdate? package configuration option. Used by a package to specify some code which should be run after a successful lake update of the package or one of its downstream dependencies. (lake#185)
• Improvements to Lake startup time (#2572, #2573)
• refine e now replaces the main goal with metavariables which were created during elaboration of e and no longer captures pre-existing metavariables that occur in e (#2502).
  • This is accomplished via changes to withCollectingNewGoalsFrom, which also affects elabTermWithHoles, refine', calc (tactic), and specialize. Likewise, all of these now only include newly-created metavariables in their output.
  • Previously, both newly-created and pre-existing metavariables occurring in e were returned inconsistently in different edge cases, causing duplicated goals in the infoview (issue #2495), erroneously closed goals (issue #2434), and unintuitive behavior due to refine e capturing previously-created goals appearing unexpectedly in e (no issue; see PR).

Merged PRs

• Add new issue templates by @mhuisi in #2519
• chore: begin development cycle for 4.2.0 by @semorrison in #2545
• chore: do not generate PR releases from forks by @semorrison in #2550
• chore: when bumping Mathlib testing branches, bump to latest nightly-testing by @semorrison in #2553
• fix: uninterpolated error message in registerRpcProcedure by @thorimur in #2547
• Enforce linebreak between calc steps by @Kha in #2532
• fix: rename parameter of withImportModules to match doc string by @dwrensha in #2530
• perf: reduce allocations in unused variable linter by @hargoniX in #2491
• fix: set MACOSX_DEPLOYMENT_TARGET in CI only by @Kha in #2556
• CI: label stale PRs by @Kha in #2561
• chore: disambiguate whnf system category by @Kha in #2560
• fix: use MoveFileEx for rename on win by @digama0 in #2546
• fix: set ref in getCalcFirstStep by @PatrickMassot in #2563
• perf: Use flat ByteArrays in Trie by @nomeata in #2529
• chore: update domain by @Kha in #2566
• feat: lake: add name to manifest by @tydeu in #2565
• fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom by @thorimur in #2502
• fix: don't try to generate below for nested predicates. by @arthur-adjedj in #2390
• perf: do not detect lean's toolchain by @tydeu in #2570
• test: add lake benchmarks by @tydeu in #2457
• perf: lake: build lakefile environments incrementally by @Kha in #2573
• perf: lake: no lean --githash when collocated by @tydeu in #2572
• test: lake: add env & dep cfg benchmarks + cleanup by @tydeu in #2574
• 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 RE...

v4.2.0-rc4

Full Changelog: v4.2.0-rc3...v4.2.0-rc4

Fixes a bug that could lead to data loss from lake clean when switching between this version and previous stable versions. Users upgrading a project from 4.2.0-rc2 or 4.2.0-rc3 should manually remove their lakefile.olean after adjusting lean-toolchain.

v4.2.0-rc3

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.

This is a fix for v4.2.0-rc2 as lean4#2648 appears to cause intermittent crashes in VSCode.

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

v4.2.0-rc1

No breaking changes so far since v4.1.0.

What's Changed

• Add new issue templates by @mhuisi in #2519
• chore: begin development cycle for 4.2.0 by @semorrison in #2545
• chore: do not generate PR releases from forks by @semorrison in #2550
• chore: when bumping Mathlib testing branches, bump to latest nightly-testing by @semorrison in #2553
• fix: uninterpolated error message in registerRpcProcedure by @thorimur in #2547
• Enforce linebreak between calc steps by @Kha in #2532
• fix: rename parameter of withImportModules to match doc string by @dwrensha in #2530
• perf: reduce allocations in unused variable linter by @hargoniX in #2491
• fix: set MACOSX_DEPLOYMENT_TARGET in CI only by @Kha in #2556
• CI: label stale PRs by @Kha in #2561
• chore: disambiguate whnf system category by @Kha in #2560
• fix: use MoveFileEx for rename on win by @digama0 in #2546
• fix: set ref in getCalcFirstStep by @PatrickMassot in #2563
• perf: Use flat ByteArrays in Trie by @nomeata in #2529
• chore: update domain by @Kha in #2566
• feat: lake: add name to manifest by @tydeu in #2565
• fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom by @thorimur in #2502
• fix: don't try to generate below for nested predicates. by @arthur-adjedj in #2390
• perf: do not detect lean's toolchain by @tydeu in #2570
• test: add lake benchmarks by @tydeu in #2457
• perf: lake: build lakefile environments incrementally by @Kha in #2573
• perf: lake: no lean --githash when collocated by @tydeu in #2572
• test: lake: add env & dep cfg benchmarks + cleanup by @tydeu in #2574

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