Skip to content

Commit

Permalink
update for v4.2.0-rc2
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 16, 2023
1 parent 3a01976 commit f98fb8a
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 8 deletions.
9 changes: 2 additions & 7 deletions RELEASES.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,10 @@ only an expectation that breaking changes will be documented in this file.
This file contains work-in-progress notes for the upcoming release, as well as previous stable releases.
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status of each version.

v4.2.0
v4.3.0 (development in progress)
---------

No breaking changes at present.
v4.3.0 (development in progress)
v4.2.0
---------

* [isDefEq cache for terms not containing metavariables.](https://github.com/leanprover/lean4/pull/2644).
Expand All @@ -24,10 +23,6 @@ v4.3.0 (development in progress)
* [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616).
* [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598).
* **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](https://github.com/leanprover/lake/issues/185))

v4.2.0
---------

* Improvements to Lake startup time ([#2572](https://github.com/leanprover/lean4/pull/2572), [#2573](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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.
Expand Down
2 changes: 1 addition & 1 deletion src/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 3)
set(LEAN_VERSION_MINOR 2)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 1) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
Expand Down

0 comments on commit f98fb8a

Please sign in to comment.