From 1fac294a2eeec2653147ca5e6de2bf8435b43241 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 29 Aug 2023 23:10:55 +1000 Subject: [PATCH] chore: add introduction to RELEASES.md (#2476) --- RELEASES.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/RELEASES.md b/RELEASES.md index ccbc3a79f6..8c04606dd5 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -1,4 +1,13 @@ -Unreleased +# Lean 4 releases + +We intend to provide regular "minor version" releases of the Lean language at approximately monthly intervals. +There is not yet a strong guarantee of backwards compatibility between versions, +only an expectation that breaking changes will be documented in this file. + +This file contains work-in-progress notes for the upcoming release, as well as previous stable releases. +Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status of each version. + +v4.0.0 --------- * [`dsimp` / `simp` / `simp_all` now fail by default if they make no progress](https://github.com/leanprover/lean4/pull/2336).