Skip to content

Commit

Permalink
doc: add migration guide for per-package server options (#3025)
Browse files Browse the repository at this point in the history
This PR adjusts `RELEASES.md` to match the recently adjusted release
notes.

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
  • Loading branch information
mhuisi and digama0 authored Dec 5, 2023
1 parent d6c81f8 commit feb0cb6
Showing 1 changed file with 19 additions and 1 deletion.
20 changes: 19 additions & 1 deletion RELEASES.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,28 @@ v4.5.0 (development in progress)
v4.4.0
---------

* 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 either of 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).

A Lakefile with the following deprecated package declaration:
```lean
def moreServerArgs := #[
"-Dpp.unicode.fun=true"
]
def moreLeanArgs := moreServerArgs
package SomePackage where
moreServerArgs := moreServerArgs
moreLeanArgs := moreLeanArgs
```

... can be updated to the following package declaration to use per-package options:
```lean
package SomePackage where
leanOptions := #[⟨`pp.unicode.fun, true⟩]
```
* [Rename request handler](https://github.com/leanprover/lean4/pull/2462).
* [Import auto-completion](https://github.com/leanprover/lean4/pull/2904).
* [`pp.beta`` to apply beta reduction when pretty printing](https://github.com/leanprover/lean4/pull/2864).
* [Per-package server options](https://github.com/leanprover/lean4/pull/2858).
* [Embed and check githash in .olean](https://github.com/leanprover/lean4/pull/2766).
* [Guess lexicographic order for well-founded recursion](https://github.com/leanprover/lean4/pull/2874).
* [Allow trailing comma in tuples, lists, and tactics](https://github.com/leanprover/lean4/pull/2643).
Expand Down

0 comments on commit feb0cb6

Please sign in to comment.