Lean 3.11.0

Stream: general

[Gabriel Ebner]

I am proud to announce the release of the latest and greatest version of the Lean community fork, Lean 3.11.0! Thanks to @Jannis Limperg, @Bryan Gin-ge Chen, @Yury G. Kudryashov, and @Mario Carneiro for their contributions! Here is the excerpt from the changelog:

Feature:

- Do not unfold irreducible definitions in unification (lean#211)
- Instantiate metavariables in rw (lean#213)

Bug fixes:

- Fix docstring of tactic.interactive.rename (lean#210)

This is the first release with the new CI using github actions and bors. There are probably issues with the binaries. Please test the release and report any issues!

[Johan Commelin]

@Gabriel Ebner Are you starting a PR to bump mathlib?

[Johan Commelin]

I hope that the lean_211_pr branch can be merged cleanly

[Gabriel Ebner]

I'll leave the updating PR to somebody else.

[Bryan Gin-ge Chen]

If no one else gets to it before me I'll open one tonight based on lean_211_pr.

[Johan Commelin]

I've battled through my teaching duties¹, so now I can work on this PR (-;

——

¹ And created a python script that will generate LaTeX code for Gaussian elimination exercises with all the intermediate steps for the solution. (Speaking of structured procrastination²…)

² http://www.structuredprocrastination.com/

[Johan Commelin]

I've started the lean-3-11-0 branch on top of lean_211_pr

[Bryan Gin-ge Chen]

I think lean-3* matches some branch protection rules, so we've been using lean_3 for the PR branches.

[Bryan Gin-ge Chen]

This probably won't be a problem until we try to delete the branch after it merges.

[Bryan Gin-ge Chen]

Oh, it also looks like only admins can push to that branch, though this might also not be a problem.

[Johan Commelin]

Ooops... I wasn't aware of that

[Johan Commelin]

Shall I change the branch name?

[Bryan Gin-ge Chen]

Hmm, I don't think it's necessary. I think we can change the branch protection to be more specific (e.g. to only match stuff starting with lean-3.). edit: done. This also makes it match up better with our github actions workflow.

[Johan Commelin]

@Bryan Gin-ge Chen Future me will forget this again and use lean-3.12.0 for the next bump PR :oops:

[Johan Commelin]

I'm at 15% of the build. No errors so far. :fencing:

[Johan Commelin]

Do we actually expect any errors?
Instantiating metavariables in rw shouldn't cause new errors, I hope.

[Johan Commelin]

And fixing a docstring.... (-;

[Johan Commelin]

Let's see if my build finishes before CI

[Johan Commelin]

~ 50% and still no errors

[Johan Commelin]

A rw error :boom:

[Johan Commelin]

Somewhere deep in data/polynomial

[Johan Commelin]

The rw in question hasn't been touched in 2 years :slight_smile:

[Johan Commelin]

:fencing: is done :tada:
#2632

[Patrick Massot]

Thanks Johan!

[Patrick Massot]

I'm curious about https://github.com/leanprover-community/mathlib/pull/2632/commits/52b910ef0392a7675899a236e75697f7ed0cc634. What was the issue here?

[Patrick Massot]

https://github.com/leanprover-community/mathlib/pull/2632/commits/40f0f53b66f6d57989580d49f80f5e27725bf0ee :head_bandage: what happened here?

[Johan Commelin]

Patrick Massot said:

I'm curious about https://github.com/leanprover-community/mathlib/pull/2632/commits/52b910ef0392a7675899a236e75697f7ed0cc634. What was the issue here?

With the hyperreals... I don't really know. The little black triangle sometimes still fails for reasons that I find mysterious.

[Johan Commelin]

Patrick Massot said:

https://github.com/leanprover-community/mathlib/pull/2632/commits/40f0f53b66f6d57989580d49f80f5e27725bf0ee :head_bandage: what happened here?

This is indeed a bit sad. I don't completely understand what happens there. Maybe @Gabriel Ebner can explain.

[Patrick Massot]

Yes I guess anything involving the cursed triangle hardly counts as a new mystery.

[Gabriel Ebner]

The hyperreals: I think @Reid Barton conjectured that the proofs relied on the definitional reduction of real numbers, in particular that (0 + 0 : ℝ) = 0 is true definitionally.

[Gabriel Ebner]

The manifolds: I have changed the proofs almost back, you just need to provide some arguments explicitly. I've got no good explanation here.

[Patrick Massot]

Oh nice, I didn't see this.

[Patrick Massot]

Little variation on elaboration results are probably not surprising.

[Johan Commelin]

What should go into the commit message? I fixed a bunch of errors, but I'm bad at explaining why things were broken in the first place.

[Bryan Gin-ge Chen]

I'm hoping @Gabriel Ebner can give some suggestions...

[Johan Commelin]

And... mathlib is now using lean 3.11.0 :tada: