Zulip Chat Archive

Stream: general

Topic: Lean 3.10


view this post on Zulip Gabriel Ebner (May 02 2020 at 09:20):

I am happy to announce the latest release of our community fork, Lean 3.10.0. Thank to all contributors to this release: @Bryan Gin-ge Chen, @Anne Baanen, @Scott Morrison, @Johan Commelin, @Jannis Limperg! Please be patient, the binaries are still in the oven and will be ready soon! Excerpt from the changelog:

Features:

- by calc ... is now equivalent to by refine calc ... (lean#203)
- Flag to use out-of-date oleans (lean#208)
- Order notation by priority in pretty-printer (lean#207)
- Improve congruence lemmas for coe_fn (lean#209)
- Port rename tactic from mathlib (lean#205)

Bug fixes:

- simp [← foo] avoids looping if foo is already in the simp set (lean#198)

Changes:

- init.category has been renamed to init.control (lean#202)
- string.has_decidable_eq is now implemented by foot (lean#204)

view this post on Zulip Patrick Massot (May 02 2020 at 09:51):

Gabriel Ebner said:

Bug fixes:

- simp [← foo] removes foo from the simp set (lean#198)

This lines is hard to read. Am I right to think it misses something like "in addition to doing what you think it should do"?

view this post on Zulip Patrick Massot (May 02 2020 at 09:52):

Because right now it reads like: make sure simp [← foo] == simp [-foo]

view this post on Zulip Gabriel Ebner (May 02 2020 at 09:54):

Yes, it does what you think it does. English is not my first language, so PRs to improve the wording are always welcome!

view this post on Zulip Patrick Massot (May 02 2020 at 09:55):

It's not mine either. Let's wait until America wakes up (or hope it's daytime in Mario's own timezone)

view this post on Zulip Patrick Massot (May 02 2020 at 09:56):

Or ping @Rob Lewis

view this post on Zulip Rob Lewis (May 02 2020 at 09:57):

Before, simp [← foo] would do what you expect (add foo as a right-to-left rewrite rule). But if foo was already in the simp set as a left-to-right rule, it wasn't always removed properly. So simp would loop.

view this post on Zulip Patrick Massot (May 02 2020 at 09:58):

Yes, this is what I mean. Now we are looking for a proper changelog line

view this post on Zulip Rob Lewis (May 02 2020 at 10:00):

"simp [← foo] avoids looping if foo is already in the simp set"?

view this post on Zulip Johan Commelin (May 02 2020 at 10:29):

@Gabriel Ebner Do you expect a lot of trouble with moving mathlib to 3.10?

view this post on Zulip Johan Commelin (May 02 2020 at 10:29):

(Btw, with the current rate of releases, we can expect lean pi somewhere in July (-;)

view this post on Zulip Gabriel Ebner (May 02 2020 at 10:30):

Very little. The builds are already running: #2587

view this post on Zulip Patrick Massot (May 02 2020 at 10:33):

I thought we already had more than two decimals of pi in mathlib

view this post on Zulip Patrick Massot (May 02 2020 at 10:33):

(I've always been very confused by version numbers like 3.10 > 3.2)

view this post on Zulip Johan Commelin (May 02 2020 at 10:34):

I guess this should have been called 3.a? and we could go on till 3.deadbeef?

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

Congratulations! I don't believe I made any commits that landed in 3.10c though. The last commit I made was compiling a changelog for 3.9c.

view this post on Zulip Gabriel Ebner (May 02 2020 at 10:35):

Which was not part of 3.9. :smile:

view this post on Zulip Gabriel Ebner (May 02 2020 at 10:39):

Johan Commelin said:

I guess this should have been called 3.a?

To me, 3.a sounds like an alpha release and I would expect that 3.a < 3.0.

view this post on Zulip Johan Commelin (May 02 2020 at 10:39):

/me was only joking :stuck_out_tongue_wink:

view this post on Zulip Sebastien Gouezel (May 02 2020 at 19:09):

The linter says that simp has become much more powerful. Good news, I guess!

view this post on Zulip Gabriel Ebner (May 02 2020 at 19:34):

Yes, thanks for the bug report! In one case I could replace rw A, assume v, simp, unfold_coes, simp by just simp [A].


Last updated: May 14 2021 at 05:20 UTC