From 49bdeb3c4641bc095e54b9f882c93b0c963c9e05 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 31 Oct 2023 13:50:06 +1100
Subject: [PATCH] doc: complete release notes for v4.3.0-rc1 (#2791)

---
 RELEASES.md | 28 +++++++++++++++++++++++-----
 1 file changed, 23 insertions(+), 5 deletions(-)

diff --git a/RELEASES.md b/RELEASES.md
index f149781167..9ee9d64577 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -7,20 +7,38 @@ 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.3.0 (development in progress)
+v4.3.0
 ---------
 
-* **Lake:** Changed `postUpdate?` configuration option to a `post_update` declaration. See the `post_update` syntax docstring for more information on the new syntax.
+* Many bug fixes:
+  * [Reduction of `Decidable` instances very slow when using `cases` tactic](https://github.com/leanprover/lean4/issues/2552)
+  * [`simp` not rewriting in binder](https://github.com/leanprover/lean4/issues/1926)
+  * [`simp` unfolding `let` even with `zeta := false` option](https://github.com/leanprover/lean4/issues/2669)
+  * [`simp` (with beta/zeta disabled) and discrimination trees](https://github.com/leanprover/lean4/issues/2281)
+  * [unknown free variable introduced by `rw ... at h`](https://github.com/leanprover/lean4/issues/2711)
+  * [`dsimp` doesn't use `rfl` theorems which consist of an unapplied constant](https://github.com/leanprover/lean4/issues/2685)
+  * [`dsimp` does not close reflexive equality goals if they are wrapped in metadata](https://github.com/leanprover/lean4/issues/2514)
+  * [`rw [h]` uses `h` from the environment in preference to `h` from the local context](https://github.com/leanprover/lean4/issues/2729)
+  * [missing `withAssignableSyntheticOpaque` for `assumption` tactic](https://github.com/leanprover/lean4/issues/2361)
+  * [ignoring default value for field warning](https://github.com/leanprover/lean4/issues/2178)
+* [Cancel outstanding tasks on document edit in the language server](https://github.com/leanprover/lean4/pull/2648).
+* [Remove unnecessary `%` operations in `Fin.mod` and `Fin.div`](https://github.com/leanprover/lean4/pull/2688)
+* [Avoid `DecidableEq` in `Array.mem`](https://github.com/leanprover/lean4/pull/2774)
+* [Ensure `USize.size` unifies with `?m + 1`](https://github.com/leanprover/lean4/issues/1926)
+* [Improve compatibility with emacs eglot client](https://github.com/leanprover/lean4/pull/2721)
 
-* [Lake: A manifest is automatically created on workspace load if one does not exists.](https://github.com/leanprover/lean4/pull/2680).
+**Lake:**
 
-* **Lake:** The `:=` syntax for configuration declarations (i.e., `package`, `lean_lib`, and `lean_exe`) has been deprecated. For example, `package foo := {...}` is deprecated.
+* [Sensible defaults for `lake new MyProject math`](https://github.com/leanprover/lean4/pull/2770)
+* 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.](https://github.com/leanprover/lean4/pull/2680).
+* 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`](https://github.com/leanprover/lean4/pull/2709)
 
 v4.2.0
 ---------
 
 * [isDefEq cache for terms not containing metavariables.](https://github.com/leanprover/lean4/pull/2644).
-* [Cancel outstanding tasks on document edit in the language server](https://github.com/leanprover/lean4/pull/2648).
 * Make [`Environment.mk`](https://github.com/leanprover/lean4/pull/2604) and [`Environment.add`](https://github.com/leanprover/lean4/pull/2642) private, and add [`replay`](https://github.com/leanprover/lean4/pull/2617) as a safer alternative.
 * `IO.Process.output` no longer inherits the standard input of the caller.
 * [Do not inhibit caching](https://github.com/leanprover/lean4/pull/2612) of default-level `match` reduction.