diff --git a/RELEASES.md b/RELEASES.md index 74650588b3..6ed853ec98 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -11,6 +11,61 @@ of each version. v4.6.0 (development in progress) --------- +* Add custom simplification procedures (aka `simproc`s) to `simp`. Simprocs can be triggered by the simplifier on a specified term-pattern. Here is an small example: +```lean +import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat + +def foo (x : Nat) : Nat := + x + 10 + +/-- +The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`. +-/ +simproc reduceFoo (foo _) := + /- A term of type `Expr → SimpM (Option Step) -/ + fun e => OptionT.run do + /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/ + guard (e.isAppOfArity ``foo 1) + /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/ + let n ← Nat.fromExpr? e.appArg! + /- + The `Step` type has two constructors: `.done` and `.visit`. + * The constructor `.done` instructs `simp` that the result does + not need to be simplied further. + * The constructor `.visit` instructs `simp` to visit the resulting expression. + + If the result holds definitionally as in this example, the field `proof?` can be omitted. + -/ + return .done { expr := Lean.mkNatLit (n+10) } +``` +We disable simprocs support by using the command `set_option simprocs false`. This command is particularly useful when porting files to v4.6.0. +Simprocs can be scoped, manually added to `simp` commands, and suppressed using `-`. They are also supported by `simp?`. `simp only` does not execute any `simproc`. Here are some examples for the `simproc` defined above. +```lean +example : x + foo 2 = 12 + x := by + set_option simprocs false in + /- This `simp` command does make progress since `simproc`s are disabled. -/ + fail_if_success simp + simp_arith + +example : x + foo 2 = 12 + x := by + /- `simp only` must not use the default simproc set. -/ + fail_if_success simp only + simp_arith + +example : x + foo 2 = 12 + x := by + /- + `simp only` does not use the default simproc set, + but we can provide simprocs as arguments. -/ + simp only [reduceFoo] + simp_arith + +example : x + foo 2 = 12 + x := by + /- We can use `-` to disable `simproc`s. -/ + fail_if_success simp [-reduceFoo] + simp_arith +``` + + v4.5.0 --------- @@ -50,7 +105,7 @@ v4.5.0 - `Widget.UserWidgetDefinition` is deprecated in favour of `Widget.Module`. The annotation `@[widget]` is deprecated in favour of `@[widget_module]`. To migrate a definition of type `UserWidgetDefinition`, remove the `name` field and replace the type with `Widget.Module`. Removing the `name` results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using `
{name}{rest_of_widget}
`. See an example migration [here](https://github.com/leanprover/std4/pull/475/files#diff-857376079661a0c28a53b7ff84701afabbdf529836a6944d106c5294f0e68109R43-R83). - The new command `show_panel_widgets` allows displaying always-on and locally-on panel widgets. - `RpcEncodable` widget props can now be stored in the infotree. - - See [RFC 2963](https://github.com/leanprover/lean4/issues/2963) for more details and motivation. + - See [RFC 2963](https://github.com/leanprover/lean4/issues/2963) for more details and motivation. * If no usable lexicographic order can be found automatically for a termination proof, explain why. See [feat: GuessLex: if no measure is found, explain why](https://github.com/leanprover/lean4/pull/2960). @@ -71,7 +126,7 @@ v4.5.0 * Tactics with `withLocation *` [no longer fail](https://github.com/leanprover/lean4/pull/2917) if they close the main goal. * Implementation of a `test_extern` command for writing tests for `@[extern]` and `@[implemented_by]` functions. - Usage is + Usage is ``` import Lean.Util.TestExtern @@ -79,8 +134,8 @@ v4.5.0 ``` The head symbol must be the constant with the `@[extern]` or `@[implemented_by]` attribute. The return type must have a `DecidableEq` instance. -Bug fixes for -[#2853](https://github.com/leanprover/lean4/issues/2853), [#2953](https://github.com/leanprover/lean4/issues/2953), [#2966](https://github.com/leanprover/lean4/issues/2966), +Bug fixes for +[#2853](https://github.com/leanprover/lean4/issues/2853), [#2953](https://github.com/leanprover/lean4/issues/2953), [#2966](https://github.com/leanprover/lean4/issues/2966), [#2971](https://github.com/leanprover/lean4/issues/2971), [#2990](https://github.com/leanprover/lean4/issues/2990), [#3094](https://github.com/leanprover/lean4/issues/3094). Bug fix for [eager evaluation of default value](https://github.com/leanprover/lean4/pull/3043) in `Option.getD`. @@ -93,19 +148,19 @@ 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