## Stream: general

### Topic: Lean 3.10

#### 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)

#### 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"?

#### Patrick Massot (May 02 2020 at 09:52):

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

#### 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!

#### 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)

#### Patrick Massot (May 02 2020 at 09:56):

Or ping @Rob Lewis

#### 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.

#### Patrick Massot (May 02 2020 at 09:58):

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

#### Rob Lewis (May 02 2020 at 10:00):

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

#### Johan Commelin (May 02 2020 at 10:29):

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

#### Johan Commelin (May 02 2020 at 10:29):

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

#### Gabriel Ebner (May 02 2020 at 10:30):

Very little. The builds are already running: #2587

#### Patrick Massot (May 02 2020 at 10:33):

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

#### Patrick Massot (May 02 2020 at 10:33):

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

#### 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?

#### 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.

#### Gabriel Ebner (May 02 2020 at 10:35):

Which was not part of 3.9. :smile:

#### 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.

#### Johan Commelin (May 02 2020 at 10:39):

/me was only joking :stuck_out_tongue_wink:

#### Sebastien Gouezel (May 02 2020 at 19:09):

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

#### 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