Lean 3.7.0 released!

Stream: general

[Gabriel Ebner]

It is my great pleasure to announce the crowning pinnacle of the latest release cycle of the Lean community fork, Lean 3.7.0. This release focused on bringing new and exciting features to the C++ codebase, including:

• simp can now rewrite in subsingletons (@Anne Baanen)
• (+) now unifies with (λ x y, x + y) (@Anne Baanen)
• the apply tactic now synthesizes type class arguments in the right order (@Reid Barton)
• touch **/*.olean is finally a thing of the past (@Wojciech Nawrocki)
• metaprogramming API for protected definitions (@Simon Hudon)
• metaprogramming API for persistent attributes (@Simon Hudon)
• fixed coercion from parser to tactic(original PR from @Floris van Doorn)
• typeclass arguments for instances are resolved right-to-left (like in Lean 4)
• typeclass resolution skips instances that have already been assigned via unification
• simp no longer fails if an exception occurs during type class resolution

[Gabriel Ebner]

The accompanying mathlib PR is also ready: #2106

[Reid Barton]

Thanks for all your work on this!

[Patrick Massot]

Congratulations! What is the parser to tactic thing?

[Gabriel Ebner]

Lean tactics can specify a parser for their arguments (this is how the left-arrows etc. work). Inside a parser, you can call a tactic. Previously you would get a VM exception if this tactic failed. So mathlib included a parser.of_tactic' function as a workaround. Now this workaround is no longer necessary (and removed in #2106).

[Kevin Buzzard]

The typeclass changes look very interesting.

[Sebastien Gouezel]

Does it mean we should revert #877?

[Gabriel Ebner]

I'm not sure if they are a completely positive change, the mathlib build time has increased by a few minutes with the change to 3.7.0 (but this might also be to the other changes). But they fix some real issues: for example issue #1561 about the has_scalar ℝ (ℝ → ℝ) instance now works as expected after the change.

[Gabriel Ebner]

Sebastien Gouezel said:

Does it mean we should revert #877?

Yes!

[Gabriel Ebner]

But the underlying issue is exactly the same as before: the instances need to be in the right order. In Lean <=3.6, this meant that the most specific instance should come first. In Lean >=3.7, the most specific instance should come last.

[Bryan Gin-ge Chen]

@Wojciech Nawrocki After https://github.com/leanprover-community/lean/pull/140 does Lean now require the .lean files to be around in addition to the .olean files for imports to work?

[Bryan Gin-ge Chen]

@Edward Ayers and I have been trying to get to the bottom of some issues with the web editor with Lean 3.7.0 and we're running into some trouble which I think is related to that PR. After we add the .lean files to the library.zip bundle, the Lean server seems to work on the first run, but making edits or hovering leads to a bunch of errors (like "Error: ENOENT: No such file or directory., '/init.lean'").

I take it Lean 3.7.0 has been working fine in VS Code? @Gabriel Ebner

[Gabriel Ebner]

Well, yes, that's how I ported mathlib. I didn't check, but your suspicion seems plausible. What happens if you include the *.lean files in library.zip?

[Bryan Gin-ge Chen]

We did include the .lean files in library.zip, but then we ran into this other error (where it tries to look for /init.lean).

[Gabriel Ebner]

Ah I missed that, sorry.

[Bryan Gin-ge Chen]

If you clone https://github.com/bryangingechen/lean-web-editor, run

npm install
./node_modules/.bin/webpack-dev-server

and then unzip dist.zip into the dist/ folder before opening localhost:8080 you should be able to reproduce what we've been seeing.

[Gabriel Ebner]

I'll leave this to @Wojciech Nawrocki.

[Edward Ayers]

Hold fire with this. I think it's more likely I didn't build the wasm properly.

[Wojciech Nawrocki]

I did absolutely assume .lean files would exist when making that change - I'll fix this ASAP, sorry! However, it's not currently clear to me why it would fail even if they are present. I'll try to always test changes with the web editor as well from now on, since the CI doesn't cover it (could it?).

[Bryan Gin-ge Chen]

Yeah, I'm not sure what happened when we included the .lean files and I haven't yet tried using the official 3.7.0 browser builds, so it's possible that it's due to some issue with Ed's build.

[Bryan Gin-ge Chen]

OK, I just tried out the browser build of Lean 3.7.0c from the releases page with the Lean web editor and it works, provided I include the .lean files in the library.zip. If I don't include the .lean files then it fails to import init.

[Wojciech Nawrocki]

Okay! I'll PR a fix to read .oleans even if no source files are present, so that they don't have to exist in the web bundle.

[Bryan Gin-ge Chen]

@Wojciech Nawrocki Just tried the browser build of Lean 3.7.1c and it works perfectly without .lean files in the ZIP! Thanks so much for the quick fix!

[Wojciech Nawrocki]

Great! np