## Stream: general

### Topic: Lean 3.16.0

#### Gabriel Ebner (Jun 10 2020 at 14:03):

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)
• 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:

#### Rob Lewis (Jun 10 2020 at 14:19):

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 (Jun 10 2020 at 14:20):

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

#### Patrick Massot (Jun 10 2020 at 14:23):

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 (Jun 10 2020 at 14:25):

Ah, I see. I can be patient :)

#### Patrick Massot (Jun 10 2020 at 14:30):

Not necessarily, it seems Ed is connected right now.

#### Patrick Massot (Jun 10 2020 at 14:30):

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

#### Edward Ayers (Jun 10 2020 at 14:50):

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

#### Bryan Gin-ge Chen (Jun 10 2020 at 14:54):

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 (Jun 10 2020 at 19:28):

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

#### Gabriel Ebner (Jun 10 2020 at 20:24):

The tactic should be collapsed by default now.

#### Gabriel Ebner (Jun 10 2020 at 20:25):

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 (Jun 10 2020 at 20:34):

Clicking on Tactic state to uncollapse it is very tempting.

#### Patrick Massot (Jun 10 2020 at 20:35):

highlighting persistence is still totally random too

Peek.gif

#### Kevin Buzzard (Jun 10 2020 at 20:47):

This gif would be really good with a banging techno soundtrack

#### Gabriel Ebner (Jun 10 2020 at 21:07):

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

#### Gabriel Ebner (Jun 10 2020 at 21:27):

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

#### Patrick Massot (Jun 12 2020 at 08:59):

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

#### Patrick Massot (Jun 12 2020 at 09:00):

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

#### Patrick Massot (Jun 12 2020 at 09:01):

Oh we also lost the "click Try this" feature

#### Gabriel Ebner (Jun 12 2020 at 10:01):

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 (Jun 12 2020 at 16:03):

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

Bug fixes:

Features:

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 (Jun 13 2020 at 18:31):

lean-0.15.15.vsix

#### Patrick Massot (Jun 13 2020 at 18:33):

Does it assume a very recent Lean?

#### Edward Ayers (Jun 13 2020 at 18:35):

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

#### Edward Ayers (Jun 13 2020 at 18:37):

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

#### Patrick Massot (Jun 13 2020 at 18:37):

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

#### Patrick Massot (Jun 13 2020 at 18:40):

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

#### Patrick Massot (Jun 13 2020 at 18:41):

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

#### Patrick Massot (Jun 13 2020 at 18:42):

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 (Jun 13 2020 at 18:43):

Yeah should I change the decoration or just remove it?

#### Edward Ayers (Jun 13 2020 at 18:47):

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 (Jun 13 2020 at 18:47):

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 (Jun 13 2020 at 18:48):

Ok I've just removed it

I mean
Peek.gif

#### Patrick Massot (Jun 13 2020 at 18:53):

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

#### Patrick Massot (Jun 13 2020 at 18:55):

I'm sorry to disappoint you.

#### Gabriel Ebner (Jun 13 2020 at 18:56):

@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 (Jun 13 2020 at 18:58):

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 (Jun 13 2020 at 19:02):

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 (Jun 13 2020 at 19:05):

Of course now it behaves correctly.

#### Patrick Massot (Jun 13 2020 at 19:06):

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

#### Edward Ayers (Jun 13 2020 at 19:11):

lean-0.15.15.vsix

#### Edward Ayers (Jun 13 2020 at 19:13):

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 (Jun 13 2020 at 19:15):

maybe the win message should be customisable

#### Gabriel Ebner (Jun 13 2020 at 19:23):

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 (Jun 13 2020 at 19:24):

Ah yes that's a good idea

#### Edward Ayers (Jun 13 2020 at 19:25):

I forgot you could override an override.

#### Gabriel Ebner (Jun 13 2020 at 19:32):

IIRC the functions tactic_state_widget and term_goal_widget are not overriden anywhere.

#### Edward Ayers (Jun 13 2020 at 22:29):

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

#### Rob Lewis (Jun 17 2020 at 11:33):

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 (Jun 17 2020 at 15:05):

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 (Jun 17 2020 at 15:12):

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

#### Rob Lewis (Jun 17 2020 at 15:20):

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

#### Scott Morrison (Jun 17 2020 at 15:26):

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

#### Edward Ayers (Jun 17 2020 at 15:32):

What platforms are you using?

I'm on Ubuntu.

#### Edward Ayers (Jun 17 2020 at 15:39):

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 (Jun 17 2020 at 15:42):

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 (Jun 17 2020 at 15:45):

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

#### Rob Lewis (Jun 17 2020 at 16:21):

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

#### Rob Lewis (Jun 17 2020 at 16:22):

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

#### Gabriel Ebner (Jun 17 2020 at 16:24):

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 (Jun 17 2020 at 16:30):

@Edward Ayers Are you also running a debug build?

#### Edward Ayers (Jun 17 2020 at 16:31):

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 (Jun 17 2020 at 20:57):

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

#### Rob Lewis (Jun 17 2020 at 20:58):

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 (Jun 17 2020 at 22:44):

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 (Jun 17 2020 at 22:46):

Basically the Error updating: Try again is always flickering.

#### Patrick Massot (Jun 17 2020 at 22:48):

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

#### Edward Ayers (Jun 18 2020 at 09:37):

lean-0.15.15.vsix

#### Edward Ayers (Jun 18 2020 at 09:40):

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 (Jun 18 2020 at 09:40):

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

#### Rob Lewis (Jun 18 2020 at 09:41):

Gabriel Ebner said:

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

Yep.

#### Gabriel Ebner (Jun 18 2020 at 09:42):

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

#### Edward Ayers (Jun 18 2020 at 09:42):

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

#### Gabriel Ebner (Jun 18 2020 at 09:45):

Oh, I know what happened with the holes.

#### Rob Lewis (Jun 18 2020 at 09:45):

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

#### Rob Lewis (Jun 18 2020 at 09:45):

But probably not recently.

lean#343

7^3

#### Johan Commelin (Jun 18 2020 at 14:26):

Also 342 + 1... :stuck_out_tongue_wink:

Last updated: Jan 31 2023 at 21:29 UTC