Zulip Chat Archive

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

Bug fixes:

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

Changes:

Mathlib PR:

  • is busily being prepared (#4802)

Johan Commelin (Oct 29 2020 at 14:40):

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 (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):

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

Johan Commelin (Oct 30 2020 at 05:29):

I've kicked #4802 on the queue.

a bug is dead! Long live bug!


Last updated: Dec 20 2023 at 11:08 UTC