v4.14.0-rc2 discussion

Stream: general

[Kim Morrison]

Discusion of the v4.14.0 release candidates can go here.

[Kim Morrison]

Note that we've already released the second release candidate. rc1 had a linking problem that was affecting some downstream projects. rc2 should be functionally identical. I've updated Mathlib and lean4checker to use v4.14.0-rc2, but as of the moment I write this some others (Batteries, Aesop, ProofWidgets, lean4-cli, quote4, import-graph ...) are still on rc1. Hopefully authors/maintainers of those projects can do those bumps. If anyone else runs into problems because of something upstream using rc1, please ping here!

[Jannis Limperg]

I just noticed that lake didn't rebuild anything when I switched from rc1 to rc2. Could this cause any problems?

[Kim Morrison]

Just noting something great that has arrived with v4.14.0-rc2: @Kyle Miller's #18699 which switches over simp (config := {contextual := true}) to just simp +contextual!

This new syntax for boolean configuration options is available for all tactics now.

[Kyle Miller]

Here are some other features that I'm excited made it into this release candidate:

• Dot notation can now make use of CoeFun instances. For example, given m : Multiset α, you can write m.card even though Multiset.card has type Multiset α →+ ℕ.
• The structure command now supports recursion, so no need to write such structures using inductive.
• There's now no need to write the : Prop in structure ... : Prop or inductive ... : Prop if the type obviously should be a proposition, for example a structure with only propositional fields.
• The congr and arg/enter/lhs/rhs conv tactics are now more powerful. You can also write things like arg -2 to get the second-to-last explicit argument or arg @-1 to get the last argument.
• You can use @[simp ←] to add the reverse direction of a theorem as a simp lemma, without needing to modify the lemma statement.
• #eval now can use ToExpr instances, giving hoverable results in the Infoview, and a number of bugs have been fixed, like missing messages when evaluating some monads. It attempts to auto-derive Repr instances too.
• There's now better tactic completion even when your cursor is in the middle of whitespace.

There are plenty of great changes that I neglected to mention, and here's the full change log.

[Johan Commelin]

I really love the m.card feature! It would be great if we could (automatically?!) refactor mathlib to take a lot of advantage of this.

[Johan Commelin]

I also notice that there are already a lot of simp +contextuals in mathlib. I'm working on a PR to replace the remaining occurences of simp (config := {contextual := true})

[Johan Commelin]

Voila: #18718 (touches 91 files)

[Ruben Van de Velde]

Johan Commelin said:

I really love the m.card feature! It would be great if we could (automatically?!) refactor mathlib to take a lot of advantage of this.

That feature was really missed during the port. There might even be some porting notes about it

[Joachim Breitner]

Thanks for the summary, Kyle! Good substitute for propor release notes :-)

[Marcus Rossel]

Kyle Miller said:

• The congr and arg/enter/lhs/rhs conv tactics are now more powerful.

In what way is congr more powerful now?

[Asei Inoue]

Lean.Eval class is removed?

[Kyle Miller]

@Marcus Rossel congr can handle over-applied functions now; there's an example in the test file in lean4#5861. Also, arg now does not make use of congr, but instead it synthesizes its own specialized congruence lemma to access a particular argument. It too can handle over-applied functions.

[Kyle Miller]

@Asei Inoue Yes. The #eval system splits the typeclass into two separate concerns. First, there's the new docs#MonadEval, which is docs#MonadLift but specifically for adapting monads to a monad that #eval can support (IO, CoreM, MetaM, TermElabM, and CommandElabM). Second, there's finding a way to represent the evaluated value; it looks for a ToExpr, Repr, or ToString instance.