Lean 3.10

Stream: general

[Gabriel Ebner]

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]

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]

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

[Gabriel Ebner]

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]

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

[Patrick Massot]

Or ping @Rob Lewis

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

Very little. The builds are already running: #2587

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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]

Which was not part of 3.9. :smile:

[Gabriel Ebner]

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]

/me was only joking :stuck_out_tongue_wink:

[Sebastien Gouezel]

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

[Gabriel Ebner]

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