From 232b601cb8f0861c16cf73f131e7a2ce2297d9e4 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 26 Sep 2023 11:55:01 +1000 Subject: [PATCH] doc: add token error change to RELEASES.md (#2579) (#2584) (cherry picked from commit 4acdcc4c4063f28d04e1a6d3afa4f39919d80fd7) Co-authored-by: Sebastian Ullrich --- RELEASES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index c65f3cf818cf..7a57c81c964f 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -10,6 +10,8 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f v4.1.0 --------- +* The error positioning on missing tokens has been [improved](https://github.com/leanprover/lean4/pull/2393). In particular, this should make it easier to spot errors in incomplete tactic proofs. + * After elaborating a configuration file, Lake will now cache the configuration to a `lakefile.olean`. Subsequent runs of Lake will import this OLean instead of elaborating the configuration file. This provides a significant performance improvement (benchmarks indicate that using the OLean cuts Lake's startup time in half), but there are some important details to keep in mind: + Lake will regenerate this OLean after each modification to the `lakefile.lean` or `lean-toolchain`. You can also force a reconfigure by passing the new `--reconfigure` / `-R` option to `lake`. + Lake configuration options (i.e., `-K`) will be fixed at the moment of elaboration. Setting these options when `lake` is using the cached configuration will have no effect. To change options, run `lake` with `-R` / `--reconfigure`.