Lean 3.23

Stream: general

[Gabriel Ebner]

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)
• Add position information to declarations added in user commands (lean#488)

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]

PR discussion is happening in: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Replacing.20the.20.60a.60.20bug.20by.20the.20.60.E1.BE.B0.60.20bug/near/214975201

[Johan Commelin]

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]

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

[Kevin Lacker]

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]

This is very far from a question that we can answer

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

https://twitter.com/derKha/status/1321780568116334592

Lean 4 passed two important milestones on the way to its first release this week: * All Lean files have been ported from the old frontend written in C++ to the new one written in Lean * After removing the old frontend, Lean is now the dominant implementation language of Lean :tada: https://twitter.com/derKha/status/1321780568116334592/photo/1

- Sebastian Ullrich (@derKha)

[Johan Commelin]

I've kicked #4802 on the queue.

a bug is dead! Long live ᾰ bug!