## Stream: general

### Topic: Lean 3.23

#### Gabriel Ebner (Oct 29 2020 at 14:38):

A new Lean release has been long overdue, so let me announce the latest release of the community edition, Lean 3.23.0! Thanks to @Edward Ayers, @Reid Barton and @Mario Carneiro for contributing exciting new features!

Features:

• Expose kabstract in type_context to the VM (lean#391)

Bug fixes:

• The a bug is replaced by the ᾰ bug (lean#490)

Changes:

• New instance naming heuristic (lean#458, lean#493)
• by_contradiction uses classical logic and the name h (lean#491)

Mathlib PR:

• is busily being prepared (#4802)

#### Johan Commelin (Oct 29 2020 at 14:48):

Quoting @Reid Barton from lean#458:

Previously, inside a namespace, in a common situation like

namespace ns

instance : ring foo := ...
instance : ring bar := ...

end


both instances would be assigned the name ns.ring;
and you might not notice immediately if they were in different files.

The new heuristic tries to use both of the parts ring and foo,
even when inside a namespace, while removing some redundant
namespace components.

Two instances in the core libraries needed to have names added,
because the method to find the name appearing in the class argument
can't see through typed values (_ : T) or the use of parameters.
(These instances wouldn't have been automatically assigned names
if located outside a namespace.) I gave them their old names;
however, it's possible names of other instances have changed.

#### Johan Commelin (Oct 29 2020 at 14:49):

This is probably important information for everybody. Not just contributors, but also users of lean/mathlib

#### Kevin Lacker (Oct 29 2020 at 15:30):

Is the intention for Lean 4 to be compatible with a particular milestone of Lean 3? Like when there are changes to the c++ on the community version, are those changes also going to need to go into the Lean 4 codebase?

#### Mario Carneiro (Oct 29 2020 at 15:31):

This is very far from a question that we can answer

#### Mario Carneiro (Oct 29 2020 at 15:32):

The leanprover-community group has very little visibility or influence on the goings on in lean 4, so I personally consider it unlikely that we will end up with such an arrangement

#### Kevin Lacker (Oct 29 2020 at 15:33):

maybe @Sebastian Ullrich or @Leonardo de Moura has thoughts? dunno if they pay attention to this zulip

#### Kevin Buzzard (Oct 29 2020 at 15:42):

Leo doesn't (and likes to be left alone, please don't ping him). Sebastian does.

#### Kevin Buzzard (Oct 29 2020 at 15:44):

What little I know is this: when we get Lean 4 (and judging by the PR's happening right now, this might be soon...ish) there could well be no simplifier and no support for auto-generated variable names, so those are two things which will be quite brakey.

#### Alex J. Best (Oct 29 2020 at 16:30):

a bug is dead! Long live ᾰ bug!