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!
type_contextto the VM (lean#391)
- Add position information to declarations added in user commands (lean#488)
abug is replaced by the
- New instance naming heuristic (lean#458, lean#493)
by_contradictionuses classical logic and the name
- is busily being prepared (#4802)
Johan Commelin (Oct 29 2020 at 14:40):
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
and you might not notice immediately if they were in different files.
The new heuristic tries to use both of the parts
even when inside a namespace, while removing some redundant
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):
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 (Oct 30 2020 at 05:29):
I've kicked #4802 on the queue.
a bug is dead! Long live
Last updated: May 10 2021 at 18:22 UTC