Zulip Chat Archive

Stream: general

Topic: Lean 3.5.0c Released


view this post on Zulip Simon Hudon (Dec 27 2019 at 23:32):

Dear Lean community,

We finally have a release for Lean 3.5.0c! Using elan, it can be installed with the following command line:

elan toolchain install leanprover-community/lean:3.5.0

leanpkg.toml files can be updated to refer to 3.5.0c:

lean_version = "leanprover-community/lean:3.5.0"

The binaries can be found here and, as before, they are available for Linux, OS X, Windows and for the browser.

All the code that works with 3.4.2 should still work and we made sure that the current version of mathlib still works with this release. A more detailed summary of the changes can be found here.

Going forward, we will continue fixing bugs and adding features that makes Leaners' (or Lean-atics?) life easier. We have been strict so far in maintaining backward compatibility but we will now start considering breaking changes as well.

Special thanks to those who made this release possible: @Bryan Gin-ge Chen, @Edward Ayers, @Gabriel Ebner, @Wojciech Nawrocki, @Mario Carneiro, @matt rice, @Keeley Hoek and of course @Leonardo de Moura and @Sebastian Ullrich.

view this post on Zulip Rob Lewis (Dec 27 2019 at 23:45):

This is great! Thanks for the hard work guys.

view this post on Zulip Rob Lewis (Dec 27 2019 at 23:47):

I think the workshop in January would be a good time to talk about "porting" mathlib to 3.5c, that is, taking advantage of changes that aren't backward compatible.

view this post on Zulip Simon Hudon (Dec 27 2019 at 23:48):

Good idea :) I think @Jeremy Avigad planned on mathlib discussion, we can bring it up then

view this post on Zulip Rob Lewis (Dec 27 2019 at 23:50):

Yup. We'll put up more details about the schedule soon. But we have a few blocks of time set aside for this kind of stuff.

view this post on Zulip Rob Lewis (Dec 27 2019 at 23:52):

With proper elan integration, I don't see any reason not to make the change, and some of the new features/fixes will really be helpful.

view this post on Zulip Simon Hudon (Dec 27 2019 at 23:55):

Cool :) Are you thinking of some specific?

view this post on Zulip Rob Lewis (Dec 28 2019 at 00:42):

Renaming all the primed tactics, first of all, but I think there's a lot.

view this post on Zulip Patrick Massot (Dec 28 2019 at 10:33):

I'm very much interested in this for teaching. Is there anything I could do to get a version of Lean for linux, windows and MacOS where all primed versions become unprimed and, much more importantly, rintros becomes intro and rcases becomes cases? I think those would intro and cases changes would even be backward compatible.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 10:52):

I think cases H with H1 H2 becomes rcases H with ⟨H1, H2⟩.

view this post on Zulip Chris Hughes (Dec 28 2019 at 10:58):

There's plenty of little updates to the library that we'd like to do (e.g. get rid of nat.pow and discrete_field). Would it be a good idea to move the core library into mathlib and make these changes?

view this post on Zulip Yury G. Kudryashov (Dec 28 2019 at 11:01):

BTW, which part of the Lean C++ code is responsible for class instances resolution? I think about adding an algorithm that works better with algebraic classes, namely go down the chain from existing constants, not up from the goal.

view this post on Zulip Patrick Massot (Dec 28 2019 at 12:06):

Indeed rcases is not backward compatible, I was wrong.

view this post on Zulip Patrick Massot (Dec 28 2019 at 12:08):

Yury, what you are asking for is a huge change.

view this post on Zulip Patrick Massot (Dec 28 2019 at 12:10):

It seems that what I'm asking should actually be rather easy. The intro tactic is defined in Lean (in core lib of course) so it should be possible to change it without recompiling Lean, and I could try to find a completely new name for rcases. Too bad split and destruct are already taken.

view this post on Zulip Patrick Massot (Dec 28 2019 at 12:13):

@Simon Hudon Is there any reason why intro wasn't changed to rintro in Lean 3.5.0c?

view this post on Zulip Yury G. Kudryashov (Dec 28 2019 at 12:13):

@Patrick Massot I don't know whether I'll have time/skills to work on this, and I don't expect it to be done soon. However I feel that this is a way to go, at least for algebraic structures.

view this post on Zulip Patrick Massot (Dec 28 2019 at 12:15):

I don't deny that, I'm only trying to keep a distinction between easy modifications that could be made before or during Fomm2020 and long-term goals.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 14:45):

Yury, you would probably be better off talking to @Daniel Selsam directly about this. He understands type class inference well. In some sense type class inference has turned out to be one of the biggest problems which mathematicians have had with Lean 3, and things were written about it in the mathlib paper. My impression is that it was originally written with modest goals in mind perhaps inspired by the way it is used in computer science, and then mathematicians wanted to push it a whole lot further ("if group is a typeclass then I guess module should be too, because modules are defined by a few axioms just like groups -- oh dear things just got complicated" was something that happened, and "if group is a typeclass then I guess ring and comm_ring and field and complete_topological_field and 100 other things are too -- oh crap, type class inference is now trying 20 times to prove that the integers are a field".

view this post on Zulip Simon Hudon (Dec 28 2019 at 16:35):

Simon Hudon Is there any reason why intro wasn't changed to rintro in Lean 3.5.0c?

The goal of the first community release was to be conservative, to make a Lean version that could be used interchangeably (almost) with 3.4.2. If we move rintro into Lean core, we have to remove it from mathlib. That can be a suitable next step but I think there needs to be a discussion about the willingness of the mathlib community to break compatibility with Leo's Lean 3

view this post on Zulip Patrick Massot (Dec 28 2019 at 16:36):

But isn't rintro fully compatible with intro?

view this post on Zulip Simon Hudon (Dec 28 2019 at 16:38):

You mean move rintro and call it intro? You're right, that might not break anything. This is in the category of changes we could call moving mathlib tactics to core (which especially concerns the primed tactics). The best is to make one decision for the block with little variations from tactic to tactic.

view this post on Zulip Patrick Massot (Dec 28 2019 at 16:40):

Yes.

view this post on Zulip Yury G. Kudryashov (Jan 01 2020 at 13:03):

BTW, a smaller change that could help: add a command #cache_instance that adds an instance to the cache. Should work for instances involving local variables. Then a file can start with several #cache_instances instead of local attribute [instance, priority 10000].


Last updated: May 10 2021 at 17:39 UTC