Lean 3.5.0c Released

Stream: general

[Simon Hudon]

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.

[Rob Lewis]

This is great! Thanks for the hard work guys.

[Rob Lewis]

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.

[Simon Hudon]

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

[Rob Lewis]

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.

[Rob Lewis]

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.

[Simon Hudon]

Cool :) Are you thinking of some specific?

[Rob Lewis]

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

[Patrick Massot]

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.

[Kevin Buzzard]

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

[Chris Hughes]

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?

[Yury G. Kudryashov]

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.

[Patrick Massot]

Indeed rcases is not backward compatible, I was wrong.

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Yury G. Kudryashov]

@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.

[Patrick Massot]

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.

[Kevin Buzzard]

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".

[Simon Hudon]

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

[Patrick Massot]

But isn't rintro fully compatible with intro?

[Simon Hudon]

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.

[Patrick Massot]

Yes.

[Yury G. Kudryashov]

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].