From 30324dd6e599c7750a0c1f32a7836ca7839d5436 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Wed, 29 Nov 2023 14:23:32 +0100 Subject: [PATCH] doc: update RELEASES.md --- RELEASES.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index 2d1b7941dad5..d43a84d68d9f 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -13,11 +13,14 @@ v4.4.0 (development in progress) * [Allow trailing comma in tuples, lists, and tactics](https://github.com/leanprover/lean4/pull/2643). +* [Support auto-completion for imports](https://github.com/leanprover/lean4/pull/2904). + * `lake init .` and a bare `lake init` and will now use the current directory as the package name. [#2890](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/issue/2637) and PR [#2890](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/issue/2567) and PR [#2889](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/issue/2865) and PR [#2889](https://github.com/leanprover/lean4/pull/2888). * 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](https://github.com/leanprover/lean4/issue/2632) and PR [#2896](https://github.com/leanprover/lean4/pull/2896). +* 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 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](https://github.com/leanprover/lean4/pull/2858). * Cloud releases will now properly be re-unpacked if the build directory is removed. See PR [#2928](https://github.com/leanprover/lean4/pull/2928). * Lake's `math` template has been simplified. See PR [#2930](https://github.com/leanprover/lean4/pull/2930).