diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 22bb3f0de71..7352a939e57 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -1,9 +1,6 @@
 # Upcoming
 
-- fix: Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/2854)
-- fix: Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833)
-- fix: Handle sequence-to-string equality correctly in the JavaScript runtime (https://github.com/dafny-lang/dafny/pull/2877)
-- fix: A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters. (https://github.com/dafny-lang/dafny/pull/2847)
+See [docs/dev/news/](docs/dev/news/).
 
 # 3.9.0
 
@@ -11,7 +8,6 @@
 - feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (https://github.com/dafny-lang/dafny/pull/2717)
 - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
 - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
-- feat: Support arbitrary version of z3 for the language server. Dafny is still distributed with z3 4.8.5 and uses that version by default. (https://github.com/dafny-lang/dafny/pull/2820)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
 - fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)
diff --git a/Scripts/prepare_release.py b/Scripts/prepare_release.py
new file mode 100755
index 00000000000..6fca1d407dd
--- /dev/null
+++ b/Scripts/prepare_release.py
@@ -0,0 +1,413 @@
+#!/usr/bin/env python
+import argparse
+import json
+import re
+import subprocess
+import sys
+
+import datetime
+from pathlib import Path
+from textwrap import indent
+from urllib.request import Request, urlopen
+from shlex import quote
+from xml.etree import ElementTree
+
+from typing import Any, Callable, Dict, List, Optional, TypeVar, NamedTuple
+
+SKIP_ALL_CHECKS = False
+
+class CannotReleaseError(Exception):
+    pass
+
+def progress(msg: str="", **kwargs) -> None:
+    print(msg, **{"file": sys.stderr, "flush": True, **kwargs})
+
+def git(cmd: str, *args: str, **kwargs) -> subprocess.CompletedProcess:
+    return subprocess.run(["git", cmd, *args], # pylint: disable=subprocess-run-check
+        **{"capture_output": True, "check": False, "encoding": "utf-8", **kwargs})
+
+A = TypeVar(name="A")
+def with_error(fn: Callable[[], A]) -> A:
+    try:
+        return fn()
+    except Exception as e:
+        progress(f"failed: {e}")
+        if isinstance(e, subprocess.CalledProcessError):
+            progress("Process output: ")
+            progress(e.stdout)
+            progress(e.stderr)
+        raise CannotReleaseError() from e
+
+def assert_one(msg: str, condition: Callable[[], Any]):
+    assert msg.endswith("?")
+    progress(msg + " ", end="")
+    if not SKIP_ALL_CHECKS and not with_error(condition):
+        progress("no, exiting.")
+        raise CannotReleaseError()
+    progress("yes.")
+
+def run_one(msg: str, operation: Callable[[], None]):
+    assert msg.endswith("...")
+    progress(msg + " ", end="")
+    with_error(operation)
+    progress("done.")
+
+def unwrap(opt: Optional[A]) -> A:
+    assert opt
+    return opt
+
+class NewsFragment(NamedTuple):
+    pr: str
+    contents: str
+    path: Optional[Path]
+
+    @classmethod
+    def from_file(cls, pth: Path) -> "NewsFragment":
+        return NewsFragment(pth.stem, pth.read_text(encoding="utf-8"), pth)
+
+class NewsFragments:
+    r"""A collection of release note entries.
+
+    >>> import tempfile
+    >>> with tempfile.TemporaryDirectory() as tmpdir:
+    ...   fpath = Path(tmpdir) / "1234.fix"
+    ...   _ = fpath.write_text("Dafny will now detect and report burning toast.\n\n", encoding="utf-8")
+    ...   fpath = Path(tmpdir) / "5678.feat"
+    ...   _ = fpath.write_text("Two new toast patterns:\n- Dafny waterfall logo\n- Dafny haircut logo\n(They are the same.)", encoding="utf-8")
+    ...   print(NewsFragments.from_directory(tmpdir).render())
+    ## New features
+    <BLANKLINE>
+    - Two new toast patterns:
+      - Dafny waterfall logo
+      - Dafny haircut logo
+      (They are the same.)
+      (https://github.com/dafny-lang/dafny/pull/5678)
+    <BLANKLINE>
+    ## Bug fixes
+    <BLANKLINE>
+    - Dafny will now detect and report burning toast. (https://github.com/dafny-lang/dafny/pull/1234)
+    """
+
+    IGNORED = {".gitignore", "README.md"}
+    KNOWN_EXTENSIONS = {".feat": "New features",
+                        ".fix": "Bug fixes"}
+
+    def __init__(self) -> None:
+        self.fragments: Dict[str, List[NewsFragment]] = {}
+        self.unrecognized: List[Path] = []
+
+    @staticmethod
+    def from_directory(dirpath: str) -> "NewsFragments":
+        ns = NewsFragments()
+        ns._read_directory(Path(dirpath))
+        return ns
+
+    def _read_directory(self, dirpath: Path) -> None:
+        if dirpath.exists():
+            for fpath in dirpath.iterdir():
+                if fpath.suffix in self.KNOWN_EXTENSIONS:
+                    fragment = NewsFragment.from_file(fpath)
+                    self.fragments.setdefault(fpath.suffix, []).append(fragment)
+                elif fpath.name not in self.IGNORED:
+                    self.unrecognized.append(fpath)
+
+    def check(self):
+        if self.unrecognized:
+            names = ', '.join(quote(f.name) for f in sorted(self.unrecognized))
+            raise ValueError(f"Not sure what to do with {names}.")
+
+    def render(self) -> str:
+        rendered = []
+        for ext, title in self.KNOWN_EXTENSIONS.items():
+            if ext not in self.fragments:
+                continue
+            rendered.append(f"## {title}")
+            for fr in sorted(self.fragments[ext], key=lambda f: f.pr):
+                link = f"(https://github.com/dafny-lang/dafny/pull/{fr.pr})"
+                contents = fr.contents.strip()
+                sep = "\n" if "\n" in contents else " "
+                entry = indent(f"- {contents}{sep}{link}", "  ").lstrip()
+                rendered.append(entry)
+        return "\n\n".join(rendered)
+
+    def delete(self):
+        for _, fragment in self.fragments.items():
+            for fr in fragment:
+                if fr.path is not None:
+                    fr.path.unlink()
+
+class Version(NamedTuple):
+    """Support functions for version numbers.
+
+    >>> v = Version.from_string("3.8.2-xyz", datetime.date(2022, 8, 1))
+    >>> v.short
+    '3.8.2-xyz'
+    >>> v.full
+    '3.8.2.40801-xyz'
+    >>> v.comment
+    'Version 3.8.2, year 2018+4, month 8, day 1.'
+    """
+
+    VERSION_NUMBER_PATTERN = re.compile("^(?P<prefix>[0-9]+[.][0-9]+[.][0-9]+)(?P<identifier>-.+)?$")
+
+    main: str # Main version number (1.2.3)
+    date: datetime.date # Release date
+    identifier: str # Optional marker ("alpha")
+
+    @classmethod
+    def from_string(cls, vernum: str, date: Optional[datetime.date]=None) -> Optional["Version"]:
+        """Parse a short version string into a `Version` object."""
+        if m := cls.VERSION_NUMBER_PATTERN.match(vernum):
+            prefix, identifier = m.group("prefix", "identifier")
+            date = date or datetime.date.today()
+            return Version(prefix, date, identifier or "")
+        return None
+
+    @property
+    def year_delta(self):
+        return self.date.year - 2018
+
+    @property
+    def short(self):
+        return f"{self.main}{self.identifier}"
+
+    @property
+    def timestamp(self):
+        return str((self.year_delta * 100 + self.date.month) * 100 + self.date.day)
+
+    @property
+    def full(self):
+        return f"{self.main}.{self.timestamp}{self.identifier}"
+
+    @property
+    def comment(self):
+        return (f"Version {self.main}, year 2018+{self.year_delta}, " +
+                f"month {self.date.month}, day {self.date.day}.")
+
+class Release:
+    REMOTE = "origin"
+    MASTER_BRANCH = "refs/heads/master"
+    NEWSFRAGMENTS_PATH = "docs/dev/news"
+
+    def __init__(self, version: str) -> None:
+        self.version = version
+        self.branch_name = f"release-{version}"
+        self.branch_path = f"refs/heads/{self.branch_name}"
+        self.tag = f"v{version}"
+        self.build_props_path = Path("Source/Directory.Build.props")
+        self.release_notes_md_path = Path("RELEASE_NOTES.md")
+        self.newsfragments = NewsFragments.from_directory(self.NEWSFRAGMENTS_PATH)
+
+    @staticmethod
+    def _in_git_root() -> bool:
+        return Path(".git").exists()
+
+    def _has_origin(self) -> bool:
+        return git("remote", "url", self.REMOTE).returncode == 0
+
+    @staticmethod
+    def _has_git() -> bool:
+        return git("rev-parse", "--verify", "HEAD").returncode == 0
+
+    def _has_news(self) -> bool:
+        self.newsfragments.check()
+        return bool(self.newsfragments.fragments)
+
+    def _build_props_file_exists(self) -> bool:
+        return self.build_props_path.is_file()
+
+    def _parse_build_props_file(self) -> ElementTree.ElementTree:
+        parser = ElementTree.XMLParser(target=ElementTree.TreeBuilder(insert_comments=True))
+        return ElementTree.parse(self.build_props_path, parser=parser)
+
+    def _build_props_file_parses(self) -> bool:
+        try:
+            self._parse_build_props_file()
+            return True
+        except ElementTree.ParseError as e:
+            print(e)
+            return False
+
+    def _release_notes_file_exists(self) -> bool:
+        return self.release_notes_md_path.is_file()
+
+    RELEASE_NOTES_MARKER = "See [docs/dev/news/](docs/dev/news/)."
+    def _release_notes_have_header(self) -> bool:
+        contents = self.release_notes_md_path.read_text(encoding="utf-8")
+        return self.RELEASE_NOTES_MARKER in contents
+
+    def _version_number_is_fresh(self) -> bool:
+        contents = self.release_notes_md_path.read_bytes()
+        return b"# " + self.version.encode("utf-8") not in contents
+
+    @staticmethod
+    def _get_branch(check: bool) -> str:
+        return git("symbolic-ref", "--quiet", "HEAD", check=check).stdout.strip()
+
+    def _parse_vernum(self) -> Optional[Version]:
+        return Version.from_string(self.version)
+
+    def _is_release_branch(self) -> bool:
+        return self._get_branch(check=False) in (self.MASTER_BRANCH, self.branch_path)
+
+    @staticmethod
+    def _is_repo_clean() -> bool:
+        return git("status", "--short", "--untracked-files=no").stdout.strip() == ""
+
+    @classmethod
+    def _head_up_to_date(cls) -> bool:
+        git("fetch")
+        return "behind" not in git("status", "--short", "--branch").stdout
+
+    @staticmethod
+    def _no_release_blocking_issues() -> bool:
+        progress("Checking... ", end="")
+        HEADERS = {"Accept": "application/vnd.github.v3+json"}
+        ENDPOINT = 'https://api.github.com/repos/dafny-lang/dafny/issues?labels=severity%3A+release-blocker'
+        with urlopen(Request(ENDPOINT, data=None, headers=HEADERS)) as fs:
+            response = fs.read().decode("utf-8")
+        return json.loads(response) == []
+
+    def _no_release_branch(self) -> bool:
+        return git("rev-parse", "--quiet", "--verify", self.branch_path).returncode == 1
+
+    def _no_release_tag(self) -> bool:
+        return git("tag", "--verify", self.tag).returncode == 1
+
+    def _update_build_props_file(self) -> None:
+        vernum = Version.from_string(self.version)
+        assert vernum
+        xml = self._parse_build_props_file()
+        for version_element in xml.iter("VersionPrefix"):
+            tail = version_element.tail
+            version_element.clear()
+            version_element.tail = tail
+            version_element.text = vernum.full
+            comment = ElementTree.Comment(vernum.comment)
+            version_element.append(comment)
+        xml.write(self.build_props_path, encoding="utf-8")
+
+    def _create_release_branch(self):
+        git("checkout", "-b", self.branch_name, check=True)
+
+    def _consolidate_news_fragments(self):
+        news = self.newsfragments.render()
+        new_section = f"\n\n# {self.version}\n\n{news.rstrip()}"
+        contents = self.release_notes_md_path.read_text(encoding="utf-8")
+        nl = "\r\n" if "\r\n" in contents else "\n"
+        replacement = self.RELEASE_NOTES_MARKER + new_section.replace("\n", nl)
+        contents = contents.replace(self.RELEASE_NOTES_MARKER, replacement)
+        self.release_notes_md_path.write_text(contents, encoding="utf-8")
+
+    def _delete_news_fragments(self):
+        self.newsfragments.delete()
+
+    def _commit_changes(self):
+        git("commit", "--quiet", "--all",
+            "--no-verify", "--no-post-rewrite",
+            f"--message=Release Dafny {self.version}",
+            check=True)
+
+    def _push_release_branch(self):
+        git("push", "--force-with-lease", "--set-upstream",
+            self.REMOTE, f"{self.branch_path}:{self.branch_path}",
+            check=True)
+
+    # Still TODO:
+    # - Run deep test as part of release workflow
+
+    def prepare(self):
+        assert_one("Can we run `git`?",
+                   self._has_git)
+        assert_one(f"Is {self.version} a valid version number?",
+                   self._parse_vernum)
+        assert_one("Are we running from the root of a git repo?",
+                   self._in_git_root)
+        assert_one(f"Can we find `{self.build_props_path}`?",
+                   self._build_props_file_exists)
+        assert_one(f"Can we parse `{self.build_props_path}`?",
+                   self._build_props_file_parses)
+        assert_one(f"Can we find `{self.release_notes_md_path}`?",
+                   self._release_notes_file_exists)
+        assert_one(f"Does `{self.release_notes_md_path}` have a header?",
+                   self._release_notes_have_header)
+        assert_one(f"Can we create a section for `{self.version}` in `{self.release_notes_md_path}`?",
+                   self._version_number_is_fresh)
+        assert_one(f"Do we have news in {self.NEWSFRAGMENTS_PATH}?",
+                   self._has_news)
+        assert_one(f"Is the current branch `master` or `{self.branch_name}`?",
+                   self._is_release_branch)
+        assert_one("Is repo clean (all changes committed)?",
+                   self._is_repo_clean)
+        assert_one("Is HEAD is up to date?",
+                   self._head_up_to_date)
+        assert_one("Are all release-blocking issues closed?",
+                   self._no_release_blocking_issues)
+        assert_one(f"Can we create release tag `{self.tag}`?",
+                   self._no_release_tag)
+        if self._get_branch(check=False) != self.branch_path:
+            assert_one(f"Can we create release branch `{self.branch_name}`?",
+                       self._no_release_branch)
+            run_one(f"Creating release branch {self.branch_path}...",
+                    self._create_release_branch)
+        else:
+            progress("Note: Release branch already checked out, so not creating it.")
+        run_one(f"Updating `{self.build_props_path}`...",
+                self._update_build_props_file)
+        run_one(f"Updating `{self.release_notes_md_path}` from `{self.NEWSFRAGMENTS_PATH}`...",
+                self._consolidate_news_fragments)
+        run_one("Deleting news fragments...",
+                self._delete_news_fragments)
+        run_one("Creating commit...",
+                self._commit_changes)
+        run_one("Pushing release branch...",
+                self._push_release_branch)
+
+        progress("Done!")
+        progress()
+
+        DEEPTESTS_URL = "https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml"
+        progress(f"Now, start a deep-tests workflow manually for branch {self.branch_name} at\n"
+                 f"<{DEEPTESTS_URL}>.\n"
+                 "Once it completes, re-run this script with argument `release`.")
+        progress()
+
+    def _tag_release(self):
+        git("tag", "--annotate", f"--message=Dafny {self.tag}",
+            self.tag, self.branch_path, capture_output=False).check_returncode()
+
+    def _push_release_tag(self):
+        git("push", self.REMOTE, f"{self.tag}",
+            capture_output=False).check_returncode()
+
+    def release(self):
+        run_one("Tagging release...",
+                self._tag_release)
+        run_one("Pushing tag...",
+                self._push_release_tag)
+
+        progress("Done!")
+        progress()
+
+        PR_URL = f"https://github.com/dafny-lang/dafny/pull/new/{self.branch_name}"
+        progress("You can merge this branch by opening a PR at\n"
+                 f"<{PR_URL}>.")
+
+def parse_arguments() -> argparse.Namespace:
+    parser = argparse.ArgumentParser(description="Dafny release helper")
+    parser.add_argument("version", help="Version number for this release (A.B.C-xyz)")
+    parser.add_argument("action", help="Which part of the release process to run",
+                        choices=["prepare", "release"])
+    return parser.parse_args()
+
+def main() -> None:
+    args = parse_arguments()
+    try:
+        release = Release(args.version)
+        {"prepare": release.prepare,
+         "release": release.release}[args.action]()
+    except CannotReleaseError:
+        sys.exit(1)
+
+if __name__ == "__main__":
+    main()
diff --git a/docs/dev/RELEASE.md b/docs/dev/RELEASE.md
index 9438aab7c33..7e80e27cf96 100644
--- a/docs/dev/RELEASE.md
+++ b/docs/dev/RELEASE.md
@@ -2,80 +2,64 @@
 
 ## Making a new Github release
 
-0. Check that there are no open issues with the `release-blocker` label:
-   https://github.com/dafny-lang/dafny/issues?q=is%3Aopen+is%3Aissue+label%3Arelease-blocker
-
-1. In an up-to-date repository, with the `master` branch checked out and
-   up-to-date (e.g., after `git pull upstream`), checkout a new branch
-   from `master` (e.g., `git checkout -b branchname master`) change to
-   the root directory of the repository (i.e., `dafny`, which contains
-   `Source`, `Binaries`, etc.)
-
-2. Select a version number (descriptor) `$VER` (e.g., "3.0.0" or
-   "3.0.0-alpha") and select an internal version number (e.g.,
-   "3.0.0.30203"). The major.minor.patch numbers may already have been
-   incremented since the last release, so they do not necessarily need
-   to be updated, but you may want to increment them further,
-   use judgement. The last section is in "ymmdd" format, where "y" is
-   the number of years since 2018 and "mmdd" the month and day portions
-   of the release date (e.g., a release on January 12th, 2022 would be
-   x.y.z.40112). Edit the internal version number in 
-  `Source/Directory.Build.Props`.
-
-   Put the public version number in place of the "Upcoming" header in
-   `RELEASE_NOTES.md`, and add a new "Upcoming" header above it.
-
-   Push and cut a PR, get it approved, and squash and merge those
-   changes to the `master` branch.
-
-3. Kick off the deep test suite by navigating to
-   https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml,
-   clicking the "Run workflow" dropdown, ensuring `master` is selected,
-   and clicking the "Run workflow" button. The automation for releasing
-   below will check for a run of this workflow on the exact commit
-   to release.
-
-4. Create a fresh clone of the repo locally, making sure the latest commit
-   is the squashed commit you just merged and tested, and push the tag for this release.
-
-   ```
-   git clone git@github.com:dafny-lang/dafny.git dafny-for-tagging
-   cd dafny-for-tagging
-   git tag v<$VER>
-   git push origin v<$VER>
-   ```
-
-5. A GitHub action will automatically run in reaction to the tag being pushed,
-   which will build the artifacts, upload them to NuGet, build the reference manual,
-   and then create a draft GitHub release.
-   You can find and watch the progress of this workflow at
-   https://github.com/dafny-lang/dafny/actions.
-
-6. Once the action completes, you should find the draft release at
-   https://github.com/dafny-lang/dafny/releases. Edit the release body
-   to add in the release notes from `RELEASE_NOTES.md`.
-   Also check the box to create a new discussion based on
-   the release, if this is not a pre-release.
-
-7. Push the "Publish" button. This will trigger yet another workflow
-   that will download the published artifacts (from both GitHub and NuGet)
-   and run a smoke test on multiple platforms. 
-   Again you can watch for this workflow at
-   https://github.com/dafny-lang/dafny/actions.
-
-8. If preparing a pre-release, stop here, as
-   the following steps declare the release as the latest version, which
-   is not the intention.
-
-9. If something goes wrong, delete the tag and release in GitHub, fix the
-   problem and try again.
-
-10. Update the Homebrew formula for Dafny (see below).
-    Note that it is fine to leave this for the next day,
-    and other members of the community may update the formula
-    in the meantime anyway.
-
-11. Announce the new release to the world.
+0. Ensure that you are in a clean and up-to-date repository, with the `master`
+   branch checked out and up-to-date and no uncommitted changes.
+
+1. Select a version number `$VER` (e.g., "3.0.0" or "3.0.0-alpha"), then run
+   `Scripts/release.py $VER prepare` from the root of the repository.  The
+   script will check that the repository is in a good state, create and check
+   out a new release branch, update `Source/version.cs` and `RELEASE_NOTES.md`,
+   prepare a release commit, and push it.
+
+2. Kick off the deep test suite by navigating to
+   <https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml>,
+   clicking the "Run workflow" dropdown, selecting the newly created branch, and
+   clicking the "Run workflow" button. The automation for releasing below will
+   check for a run of this workflow on the exact commit to release.  (TODO:
+   Run this automatically as part of the prepare-release script.)
+
+3. Once the the tests complete, run `Scripts/release.py $VER release` from the
+   root of the repository.  The script will tag the current commit and push
+   it. (TODO: Merge with the two steps above.)  A GitHub action will
+   automatically run in reaction to the tag being pushed, which will build the
+   artifacts and reference manual and then create a draft GitHub release. You
+   can find and watch the progress of this workflow at
+   <https://github.com/dafny-lang/dafny/actions>.
+
+4. Once the action completes, you should find the draft release at
+   <https://github.com/dafny-lang/dafny/releases>. Edit the release body to add in
+   the release notes from `RELEASE_NOTES.md`.  If this is not a pre-release,
+   check the box to create a new discussion based on the release.
+
+5. Push the "Publish" button. This will trigger yet another workflow
+   that will download the published artifacts and run a smoke test
+   on multiple platforms. Again you can watch for this workflow at
+   <https://github.com/dafny-lang/dafny/actions>.
+
+6. Create a pull request to merge the newly created branch into `master` (the
+   script will give you a link to do so).  Get it approved and merged.
+
+7. Clone <https://github.com/dafny-lang/ide-vscode> and run `publish_process.js`
+   to create a new release of the VSCode plugin.
+
+8. Update the Homebrew formula for Dafny (see below).
+   Note that it is fine to leave this for the next day,
+   and other members of the community may update the formula
+   in the meantime anyway.
+
+9. Announce the new release to the world!
+
+If something goes wrong with the `prepare` step:
+
+- Remove the release commit (`git reset --hard HEAD~1`)
+- Commit fixes
+- Re-run the `prepare` step; the script will recognize the `release-` branch and will not recreate it.
+
+If something goes wrong with the `release` step:
+
+- Delete the local tag: `git tag -d vA.B.C`
+- Delete the remote tag: `git push --delete origin vA.B.C`
+- Return to the `prepare` step.
 
 ## Updating Dafny on Homebrew
 
diff --git a/docs/dev/news/2820.feat b/docs/dev/news/2820.feat
new file mode 100644
index 00000000000..b8fe8e9999b
--- /dev/null
+++ b/docs/dev/news/2820.feat
@@ -0,0 +1 @@
+The language server now supports all versions of z3 ≥ 4.8.5.  Dafny is still distributed with z3 4.8.5 and uses that version by default.
\ No newline at end of file
diff --git a/docs/dev/news/2833.fix b/docs/dev/news/2833.fix
new file mode 100644
index 00000000000..9d7df855ba0
--- /dev/null
+++ b/docs/dev/news/2833.fix
@@ -0,0 +1 @@
+Crash in the LSP in some code that does not parse
\ No newline at end of file
diff --git a/docs/dev/news/2847.fix b/docs/dev/news/2847.fix
new file mode 100644
index 00000000000..506644b4c28
--- /dev/null
+++ b/docs/dev/news/2847.fix
@@ -0,0 +1 @@
+A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters.
diff --git a/docs/dev/news/2854.fix b/docs/dev/news/2854.fix
new file mode 100644
index 00000000000..b5dfaee13dd
--- /dev/null
+++ b/docs/dev/news/2854.fix
@@ -0,0 +1 @@
+Compiled lambdas now close only on non-ghost variables
\ No newline at end of file
diff --git a/docs/dev/news/2877.fix b/docs/dev/news/2877.fix
new file mode 100644
index 00000000000..c2fc759f88f
--- /dev/null
+++ b/docs/dev/news/2877.fix
@@ -0,0 +1 @@
+Handle sequence-to-string equality correctly in the JavaScript runtime
diff --git a/docs/dev/news/README.md b/docs/dev/news/README.md
new file mode 100644
index 00000000000..3265b9793dc
--- /dev/null
+++ b/docs/dev/news/README.md
@@ -0,0 +1,40 @@
+# Latest Dafny changes
+
+Each file in this folder describes one change in Dafny since the latest release.
+
+Files in this directory are named `<PR number>.<kind>` and each contains release notes for one merged PR.  `kind` is `feat` or `fix`.  No need to include a link to the PR in the file: it will be added automatically.
+
+## Examples
+
+- `1234.fix`
+
+   ```
+   Dafny will now detect and report burning toast.
+   ```
+
+- `5678.feat`
+
+  ```
+  Two new toast patterns:
+  - Dafny waterfall logo
+  - Dafny haircut logo
+  (They are the same.)
+  ```
+
+At release time, these two files become bullet points in a new section of `RELEASE_NOTES.md` with links to the corresponding PRs, like this:
+
+```
+## New features
+
+- Two new toast patterns:
+  - Dafny waterfall logo
+  - Dafny haircut logo
+  (They are the same.)
+  (https://github.com/dafny-lang/dafny/pull/5678)
+
+## Bug fixes
+
+- Dafny will now detect and report burning toast. (https://github.com/dafny-lang/dafny/pull/1234)
+```
+
+Note that a newline is added before the link only if the original is more than one line long.