Lean 3.16.0

Stream: general

[Gabriel Ebner]

It's been almost two weeks, which means it's about time for a new release! The latest version of the community edition of Lean has been released, say welcome to Lean 3.16.0! Thanks to @Edward Ayers, Mosè Giordano, and @Reid Barton!

Features:

• Add docstrings for cc_state primitives (lean#295)
• Use BUILD_TESTING to enable or disable building tests (lean#292)
• Additional meta constants (lean#294)
• Add @[pp_nodot] (lean#297)
• Make widget look more like current tactic state (lean#303)
• Show term-proof goals as widgets (lean#304, lean#306)
• Add holes for underscores (lean#307)

Bug fixes:

• Fix case of header files for building on case-sensitive filesystems (lean#290)
• Remove useless setting of _GLIBCXX_USE_CXX11_ABI with MinGW (lean#293)
• Fix guards to make it possible to build for BSD systems (lean#291)
• Rename tactic.tactic.run_simple -> tactic.run_simple (lean#298)
• Use instance instead of semireducible transparency in type-class synthesis (lean#300)
• Widget events contain position (lean#301)
• Server: do not cancel info queries, etc. (lean#308)

Changes:

• Lower precedence of unary - (lean#287)

Server protocol changes:

• The widget field in the info response has now two new fields: line and column. You need to use these in the update_widget request.

Mathlib PR:

• already queued: #3016

[Rob Lewis]

So, I've never seen a widget before. Have I forgotten to update something or are they not in production yet? The demo looked super cool and I'd love to play around with them sometime.

[Bryan Gin-ge Chen]

There's a lot of work in progress on leanprover/vscode-lean#159.

[Patrick Massot]

Rob, if you want to play with widgets you need to ask Ed to send you a test build of the VScode extension.

[Rob Lewis]

Ah, I see. I can be patient :)

[Patrick Massot]

Not necessarily, it seems Ed is connected right now.

[Patrick Massot]

Maybe he already sent you a link. I got one last week.

[Edward Ayers]

Patrick was the only one who got a vsix, sorry if anyone else got FOMO.

[Bryan Gin-ge Chen]

They're easy enough to create though. Here's one assuming the flurry of commits to the PR are done for today: lean-0.15.15.vsix

[Patrick Massot]

I'm still seeing duplicated information as in
image.png

[Gabriel Ebner]

The tactic should be collapsed by default now.

[Gabriel Ebner]

Maybe it would be better to have a button/checkbox to switch between the two so that you don't see both at the same time.

[Patrick Massot]

Clicking on Tactic state to uncollapse it is very tempting.

[Patrick Massot]

highlighting persistence is still totally random too

[Patrick Massot]

Peek.gif

[Kevin Buzzard]

This gif would be really good with a banging techno soundtrack

[Gabriel Ebner]

Are these trippy effects on 3.16? I haven't seen them lately.

[Gabriel Ebner]

Ok, I just tried again and I see the trippy effects as well. I'll let @Edward Ayers look into this.

[Patrick Massot]

New bug report: I frequently loose tactic state while typing.
Peek.gif

[Patrick Massot]

Note how I finish typing a line with t, and don't get tactic state before wiggling the cursor.

[Patrick Massot]

Oh we also lost the "click Try this" feature

[Gabriel Ebner]

Oh yeah, the current info view auto-updates while the server is updating:

            this.server.statusChanged.on(async () => {
                if (this.displayMode === DisplayMode.OnlyState) {
                    const changed = await this.updateGoal();
                    if (changed) { this.rerender(); }
                }
            }),

[Gabriel Ebner]

We've just had another patch release after two days (3.16.2):

Bug fixes:

• Stop scanning after #exit (lean#318, fixes lean#309)
• Allow variables (A B : Type*) (lean#319, fixes lean#29)
• Escape names using French quotes by default (lean#320, fixes lean#114)
• Fix lean --deps (lean#323)
• Selection disco issue in tactic state widget (lean#324)

Features:

• Add get_widget server request (lean#314)
• Allow namespaces inside sections (lean#317, fixes lean#315)

Server protocol changes:

• The info request no longer returns the widget HTML. Instead it returns an id field in addition to line and column. The get_widget request now returns the HTML. The widget_event request also requires an id argument. (lean#314)

Mathlib PR:

• submitted by @Bryan Gin-ge Chen (#3053)

[Edward Ayers]

lean-0.15.15.vsix

[Patrick Massot]

Does it assume a very recent Lean?

[Edward Ayers]

It should work well with 3.16.2. Still some issues with older versions.

[Edward Ayers]

With older versions it sometimes gives 'interupted' errors when it shows the info view. Hopefully @Gabriel Ebner can swoop in.

[Patrick Massot]

Ok, I'll try (I removed the previous version yesterday because the tactic state disappearances really made it unusable)

[Patrick Massot]

It's still a bit disorienting that you can keep clicking forever to display more and more identical popups

[Patrick Massot]

It also seems that the big red background is coming back.

[Patrick Massot]

It can't be right that indicating where the tactic state is looking at looks much more error-like than the squiggly underline that indicate actual errors.

[Edward Ayers]

Yeah should I change the decoration or just remove it?

[Edward Ayers]

Patrick Massot said:

It's still a bit disorienting that you can keep clicking forever to display more and more identical popups

Do you mean identical in terms of decoration appearance? They should have different content in right? Eg you can click up a type hierarchy.

[Patrick Massot]

I would remove it, but making it a soft blue of something like this would already be much better (I don't know how to handle the diversity of color themes however).

[Edward Ayers]

Ok I've just removed it

[Patrick Massot]

I mean
Peek.gif

[Patrick Massot]

And I still see a lot of no info found at while typing proofs (in tactic mode of course).

[Patrick Massot]

I'm sorry to disappoint you.

[Gabriel Ebner]

@Patrick Massot Can you point me to a concrete example where the current vscode-lean version shows a tactic state, but the widget edition doesn't?

[Edward Ayers]

Patrick Massot said:

I mean...

ok so my opinion on this is that is correct and desirable behaviour, because each time you are getting information on the same term

[Edward Ayers]

Gabriel Ebner said:

Patrick Massot Can you point me to a concrete example where the current vscode-lean version shows a tactic state, but the widget edition doesn't?

I think that it happens just after typing a new character when the parser hasn't finished yet, so the info response is just empty.

[Patrick Massot]

Of course now it behaves correctly.

[Patrick Massot]

Something very disappointing that should be very easy to fix: goals accomplished is written in tiny font size.

[Edward Ayers]

lean-0.15.15.vsix

[Edward Ayers]

Patrick Massot said:

Something very disappointing that should be very easy to fix: goals accomplished is written in tiny font size.

This needs a change to the widget in lean core. I'll bump up the size and make it bold

[Edward Ayers]

maybe the win message should be customisable

[Gabriel Ebner]

This UI bikeshedding does not necessarily need to happen in core. All of the expression (and tactic state) rendering happens in a single, 200-line long file---interactive_expr.lean---which we can copy to mathlib today and use vm_override to override the version in core. I think it's faster to iterate this in mathlib than waiting for a core release for every font size tweak.

[Edward Ayers]

Ah yes that's a good idea

[Edward Ayers]

I forgot you could override an override.

[Gabriel Ebner]

IIRC the functions tactic_state_widget and term_goal_widget are not overriden anywhere.

[Edward Ayers]

I think to do it you would override tactic.save_info again

[Rob Lewis]

I'm getting periodic segfaults that I can't reproduce. Using
Edward Ayers said:

lean-0.15.15.vsix

if it's relevant. Is anyone else experiencing this? Sorry for the unhelpful bug report, but I can't consistently trigger the problem.

[Edward Ayers]

Hi Rob, thanks for reporting this, could you try again with this newer version and see if you still get the issue? Thanks. lean-0.15.15.vsix

[Kevin Buzzard]

Can I play with this bleeding edge stuff? Does it involve losing access to mathlib?

[Rob Lewis]

Okay, I've switched, will let you know if I still see it happening!

[Scott Morrison]

I was getting lots of crashes too, and reverted back to the mainline VS Code extension.

[Edward Ayers]

What platforms are you using?

[Rob Lewis]

I'm on Ubuntu.

[Edward Ayers]

Kevin Buzzard said:

Can I play with this bleeding edge stuff? Does it involve losing access to mathlib?

Hi Kevin, you can install the above extension by going to the extensions panel in vscode and clicking the '...' and then 'install from VSIX'. Since the underlying version of lean and mathlib doesn't change it should all keep working (mod these segfaults) and you should be able to revert back to the mainline extension by right clicking on the lean extension in the extensions panel and clicking 'install another version'. Switching back and forth should be as painless as a vscode reload.

[Edward Ayers]

Rob Lewis said:

I'm on Ubuntu.

Ok I'm on linux too so I'm a bit worried that I'm not seeing these segfaults...
When do you typically get the segfaults? Is it when working on mathlib? Is it while typing a lot or clicking on the infoview etc?

[Bryan Gin-ge Chen]

Speaking generally and not specifically about the extension, the segfault that I run into most frequently is lean#85.

[Rob Lewis]

I don't think I'm doing anything abnormal. Maybe I'm typing a lot? Nothing special with the infoview.

[Rob Lewis]

Pretty certain it's not lean#85, but not 100% sure...

[Gabriel Ebner]

Bug lean#85 is not a segfault, at least for me it's just error messages in the output tab. (Oh, that's because I'm running a debug build.)

[Johan Commelin]

@Edward Ayers Are you also running a debug build?

[Edward Ayers]

I'm running release 3.16.2 and I get the lean#85 segfaults. But I don't see segfaults with the new extension when I'm just leaning.

[Rob Lewis]

I haven't seen any segfaults yet since switching to the new version you posted!

[Rob Lewis]

But, I'm seeing bad behavior with hole commands. (Not sure this is new with the new extension.)

import tactic.interactive
structure foo := (a b : ℕ)
example : foo :=
_

Clicking on "generate a skeleton for the structure under construction" gives me an error "unknown hole command."

[Patrick Massot]

Also, I can't see any error without unfolding the All messages part, and there are very distracting oscillations like in Peek-18-06-2020-00-43.gif

[Patrick Massot]

Basically the Error updating: Try again is always flickering.

[Patrick Massot]

And of course I meant x ∈ closure t, for those who try to follow the math in the above GIF.

[Edward Ayers]

lean-0.15.15.vsix

[Edward Ayers]

Rob Lewis said:

But, I'm seeing bad behavior with hole commands. (Not sure this is new with the new extension.)

import tactic.interactive
structure foo := (a b : ℕ)
example : foo :=
_

Clicking on "generate a skeleton for the structure under construction" gives me an error "unknown hole command."

I get this problem on the older version of vscode as well :/

[Gabriel Ebner]

Is it also there if you use {!!} for the hole?

[Rob Lewis]

Gabriel Ebner said:

Is it also there if you use {!!} for the hole?

Yep.

[Gabriel Ebner]

Ok, then it's not a regression on any dimension.

[Edward Ayers]

Patrick Massot said:

Also, I can't see any error without unfolding the All messages part, and there are very distracting oscillations like in Peek-18-06-2020-00-43.gif

Sorry about this Patrick this should be fixed now in the version I posted above

[Gabriel Ebner]

Oh, I know what happened with the holes.

[Rob Lewis]

I mean, I've used this hole command before, so something regressed at some point.

[Rob Lewis]

But probably not recently.

[Gabriel Ebner]

lean#343

[Kevin Buzzard]

7^3

[Johan Commelin]

Also 342 + 1... :stuck_out_tongue_wink: