Lean 3.6.0

Stream: general

[Gabriel Ebner]

Good morning, everyone! I am pleased to announce the latest release of the community fork, Lean 3.6.0!
There is an associated PR to mathlib, #2064, but unfortunately it's not finished yet and I have some higher priority stuff to do right now.

[Johan Commelin]

Patrick already has a suggestion for lean-3.6.1

[Gabriel Ebner]

Yes, I know that there are outstanding feature requests. This is not the last release. Please keep the PRs coming.

[Patrick Massot]

My suggestion is not a feature request, it's a bug fix.

[Gabriel Ebner]

Ah, I missed https://github.com/leanprover-community/lean/issues/126. If somebody PRs a fix, then we can release 3.6.1 if this is a big issue.

[Gabriel Ebner]

It should be fixed now in 3.6.1. Thanks @Markus Himmel for the PR! Please complain if the PR didn't actually fix the issue.

[Yury G. Kudryashov]

I merged master into lean36, and built it.

[Yury G. Kudryashov]

real_inner_product fails to find some class instance; everything else builds fine.

[Chris Hughes]

I spent some time trying to sort that out. It times out looking for add_comm_monoid alpha. I don't know why it's even looking for that instance.

[Yury G. Kudryashov]

Definition compiles if I make it take [add_comm_group] as an argument.

[Yury G. Kudryashov]

I guess something has changed in the class instance resolution procedure between 3.5.1 and 3.6.0

[Yury G. Kudryashov]

(after fixing a couple of simps) now normed_space instance fails

[Yury G. Kudryashov]

BTW, abel doesn't work with (a - b) - (a - c) = c - b in Lean 3.6.0.

[Yury G. Kudryashov]

And this leads to more build failures in real_inner_product.

[Gabriel Ebner]

I've just merged master and updated to 3.6.1. I'll look into the real_inner_product and abel issues.

[Gabriel Ebner]

Okay, I've stumbled into an ugly type-class instance cycle when synthesizing an instance for decidable (a ≤ b):

#print has_le.le.decidable
#print decidable_linear_ordered_comm_group.to_decidable_linear_order
#print decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group
#print linear_nonneg_ring.to_decidable_linear_ordered_comm_ring

Opinions on which instance to remove? I'll try removing linear_nonneg_ring.to_decidable_linear_ordered_comm_ring for now. Is there anything that actually uses linear_nonneg_ring?

[Floris van Doorn]

It's not really a cycle, right? We start with decidable (a ≤ b) and end with decidable (nonneg x).

If any of them should be removed, definitely the last one.

[Gabriel Ebner]

I think nonneg reduces to \le in this case. But maybe I got that wrong.

[Gabriel Ebner]

The real_inner_product.lean file is now fixed. Behold the horrible hack: https://github.com/leanprover-community/mathlib/pull/2064/commits/38d32c8b8aad86701d0018daf7a8a1d22759cc65
I have no idea why these type class issues pop up now.
At least for me, abel works just fine on -.
That's it for today.

[Floris van Doorn]

Oh, nonneg is a field of a structure, so yes, in some cases it can be defined to be fun x, 0 <= x. I agree that we should remove the instance attribute from linear_nonneg_ring.to_decidable_linear_ordered_comm_ring.

[Mario Carneiro]

I think that nonneg_ring and friends should be removed from the typeclass instance search entirely. That was an experimental smart constructor for building an ordered group or ring from a "nonneg" class, but the structure is only to make the smart constructor more palatable, so it need not participate in the typeclass hierarchy

[Patrick Massot]

I don't have enough time to read Zulip those days and I'm pretty confused. I see a lot of difficulties and I don't understand how they relate to Lean 3.6.0. Maybe they don't. Was there some change in the simplfier or type class search in Lean 3.6.0?

[Gabriel Ebner]

I don't think it's clear why all of these problems come out now. Most of them are also on master, see https://github.com/leanprover-community/lean/issues/137 and #2084. My best guess is that removing decidable_eq from field has slightly changed type class resolution in some places (or made it slightly slower), and stuff that was barely working before is now completely broken.

[Patrick Massot]

Ok, so I'm not the only one to be confused.

[Johan Commelin]

Major kudos to @Gabriel Ebner !

[Johan Commelin]

The bump PR now builds!

[Johan Commelin]

I guess we should merge this sooner rather than later.

[Gabriel Ebner]

Thanks to @Anne Baanen, @Rob Lewis, @Yury G. Kudryashov, and @Scott Morrison how did lots of the work.

[Scott Morrison]

Is someone on top of updating CI so that lean-3.6.1 always has oleans?