doc: add note on .lake to RELEASES.md

leanprover · Nov 8, 2023 · 0b594ea · 0b594ea
1 parent b5cbc5b
commit 0b594ea
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/RELEASES.md b/RELEASES.md
@@ -12,6 +12,8 @@ v4.4.0 (development in progress)
 ---------
 
 * 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.
+* **Lake:** 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](https://github.com/leanprover/lean4/issues/2713).
+* **Lake:** Changed `postUpdate?` configuration option to a `post_update` declaration. See the `post_update` syntax docstring for more information on the new syntax.
 
 v4.3.0
 ---------