Zulip Chat Archive

Stream: general

Topic: Lean 3.11.0


view this post on Zulip 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!

view this post on Zulip Johan Commelin (May 08 2020 at 17:41):

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

view this post on Zulip Johan Commelin (May 08 2020 at 17:42):

I hope that the lean_211_pr branch can be merged cleanly

view this post on Zulip Gabriel Ebner (May 08 2020 at 17:42):

I'll leave the updating PR to somebody else.

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip Johan Commelin (May 08 2020 at 18:27):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2020 at 18:30):

Ooops... I wasn't aware of that

view this post on Zulip Johan Commelin (May 08 2020 at 18:30):

Shall I change the branch name?

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Johan Commelin (May 08 2020 at 18:37):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2020 at 18:39):

And fixing a docstring.... (-;

view this post on Zulip Johan Commelin (May 08 2020 at 18:39):

Let's see if my build finishes before CI

view this post on Zulip Johan Commelin (May 08 2020 at 18:56):

~ 50% and still no errors

view this post on Zulip Johan Commelin (May 08 2020 at 19:08):

A rw error :boom:

view this post on Zulip Johan Commelin (May 08 2020 at 19:08):

Somewhere deep in data/polynomial

view this post on Zulip Johan Commelin (May 08 2020 at 19:10):

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

view this post on Zulip Johan Commelin (May 08 2020 at 20:04):

:fencing: is done :tada:
#2632

view this post on Zulip Patrick Massot (May 08 2020 at 20:05):

Thanks Johan!

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 08 2020 at 20:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 08 2020 at 20:13):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 08 2020 at 20:19):

Oh nice, I didn't see this.

view this post on Zulip Patrick Massot (May 08 2020 at 20:20):

Little variation on elaboration results are probably not surprising.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (May 09 2020 at 03:35):

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

view this post on Zulip Johan Commelin (May 10 2020 at 04:08):

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


Last updated: May 12 2021 at 22:15 UTC