From 9b1999b7662e234fb2d40f1892e7b09025501423 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 2 Nov 2023 16:38:03 -0400 Subject: [PATCH] doc: lake: flexible manifest release notes --- RELEASES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index ee24504c39f8..4b87eb193918 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -13,6 +13,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:** Update manifest format to version 7 (see [lean4#2801](https://github.com/leanprover/lean4/pull/2801) for details on the changes). +* **Lake:** Deprecate the `manifestFile` field of a package configuration. v4.3.0 ---------