Zulip Chat Archive

Stream: general

Topic: Lean 3.11.0


Gabriel Ebner (May 08 2020 at 17:40):

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 (May 08 2020 at 17:41):

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

Johan Commelin (May 08 2020 at 17:42):

I hope that the lean_211_pr branch can be merged cleanly

Gabriel Ebner (May 08 2020 at 17:42):

I'll leave the updating PR to somebody else.

Bryan Gin-ge Chen (May 08 2020 at 17:58):

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

Johan Commelin (May 08 2020 at 18:17):

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 (May 08 2020 at 18:27):

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

Bryan Gin-ge Chen (May 08 2020 at 18:28):

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

Bryan Gin-ge Chen (May 08 2020 at 18:29):

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

Bryan Gin-ge Chen (May 08 2020 at 18:30):

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

Johan Commelin (May 08 2020 at 18:30):

Ooops... I wasn't aware of that

Johan Commelin (May 08 2020 at 18:30):

Shall I change the branch name?

Bryan Gin-ge Chen (May 08 2020 at 18:32):

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 (May 08 2020 at 18:37):

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

Johan Commelin (May 08 2020 at 18:37):

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

Johan Commelin (May 08 2020 at 18:39):

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

Johan Commelin (May 08 2020 at 18:39):

And fixing a docstring.... (-;

Johan Commelin (May 08 2020 at 18:39):

Let's see if my build finishes before CI

Johan Commelin (May 08 2020 at 18:56):

~ 50% and still no errors

Johan Commelin (May 08 2020 at 19:08):

A rw error :boom:

Johan Commelin (May 08 2020 at 19:08):

Somewhere deep in data/polynomial

Johan Commelin (May 08 2020 at 19:10):

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

Johan Commelin (May 08 2020 at 20:04):

:fencing: is done :tada:
#2632

Patrick Massot (May 08 2020 at 20:05):

Thanks Johan!

Patrick Massot (May 08 2020 at 20:05):

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

Patrick Massot (May 08 2020 at 20:06):

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

Johan Commelin (May 08 2020 at 20:12):

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 (May 08 2020 at 20:13):

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 (May 08 2020 at 20:13):

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

Gabriel Ebner (May 08 2020 at 20:16):

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 (May 08 2020 at 20:18):

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 (May 08 2020 at 20:19):

Oh nice, I didn't see this.

Patrick Massot (May 08 2020 at 20:20):

Little variation on elaboration results are probably not surprising.

Johan Commelin (May 09 2020 at 03:25):

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 (May 09 2020 at 03:35):

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

Johan Commelin (May 10 2020 at 04:08):

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


Last updated: Dec 20 2023 at 11:08 UTC