Zulip Chat Archive

Stream: general

Topic: Lean 3.16.0


view this post on Zulip 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)
  • 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:

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jun 10 2020 at 14:20):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jun 10 2020 at 14:25):

Ah, I see. I can be patient :)

view this post on Zulip Patrick Massot (Jun 10 2020 at 14:30):

Not necessarily, it seems Ed is connected right now.

view this post on Zulip Patrick Massot (Jun 10 2020 at 14:30):

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

view this post on Zulip Edward Ayers (Jun 10 2020 at 14:50):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 10 2020 at 19:28):

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

view this post on Zulip Gabriel Ebner (Jun 10 2020 at 20:24):

The tactic should be collapsed by default now.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 10 2020 at 20:34):

Clicking on Tactic state to uncollapse it is very tempting.

view this post on Zulip Patrick Massot (Jun 10 2020 at 20:35):

highlighting persistence is still totally random too

view this post on Zulip Patrick Massot (Jun 10 2020 at 20:36):

Peek.gif

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 20:47):

This gif would be really good with a banging techno soundtrack

view this post on Zulip Gabriel Ebner (Jun 10 2020 at 21:07):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 12 2020 at 08:59):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 12 2020 at 09:01):

Oh we also lost the "click Try this" feature

view this post on Zulip 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(); }
                }
            }),

view this post on Zulip 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)

view this post on Zulip Edward Ayers (Jun 13 2020 at 18:31):

lean-0.15.15.vsix

view this post on Zulip Patrick Massot (Jun 13 2020 at 18:33):

Does it assume a very recent Lean?

view this post on Zulip Edward Ayers (Jun 13 2020 at 18:35):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 13 2020 at 18:41):

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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 13 2020 at 18:43):

Yeah should I change the decoration or just remove it?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Edward Ayers (Jun 13 2020 at 18:48):

Ok I've just removed it

view this post on Zulip Patrick Massot (Jun 13 2020 at 18:50):

I mean
Peek.gif

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Jun 13 2020 at 18:55):

I'm sorry to disappoint you.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 13 2020 at 19:05):

Of course now it behaves correctly.

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 13 2020 at 19:11):

lean-0.15.15.vsix

view this post on Zulip 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

view this post on Zulip Edward Ayers (Jun 13 2020 at 19:15):

maybe the win message should be customisable

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 13 2020 at 19:24):

Ah yes that's a good idea

view this post on Zulip Edward Ayers (Jun 13 2020 at 19:25):

I forgot you could override an override.

view this post on Zulip Gabriel Ebner (Jun 13 2020 at 19:32):

IIRC the functions tactic_state_widget and term_goal_widget are not overriden anywhere.

view this post on Zulip Edward Ayers (Jun 13 2020 at 22:29):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 15:12):

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

view this post on Zulip Rob Lewis (Jun 17 2020 at 15:20):

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

view this post on Zulip Scott Morrison (Jun 17 2020 at 15:26):

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

view this post on Zulip Edward Ayers (Jun 17 2020 at 15:32):

What platforms are you using?

view this post on Zulip Rob Lewis (Jun 17 2020 at 15:38):

I'm on Ubuntu.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jun 17 2020 at 16:22):

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

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Jun 17 2020 at 16:30):

@Edward Ayers Are you also running a debug build?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Jun 17 2020 at 20:57):

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

view this post on Zulip 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."

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 17 2020 at 22:46):

Basically the Error updating: Try again is always flickering.

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 18 2020 at 09:37):

lean-0.15.15.vsix

view this post on Zulip 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 :/

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 09:40):

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

view this post on Zulip Rob Lewis (Jun 18 2020 at 09:41):

Gabriel Ebner said:

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

Yep.

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 09:42):

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

view this post on Zulip 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

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

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 09:45):

Oh, I know what happened with the holes.

view this post on Zulip Rob Lewis (Jun 18 2020 at 09:45):

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

view this post on Zulip Rob Lewis (Jun 18 2020 at 09:45):

But probably not recently.

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 09:53):

lean#343

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 10:29):

7^3

view this post on Zulip Johan Commelin (Jun 18 2020 at 14:26):

Also 342 + 1... :stuck_out_tongue_wink:


Last updated: Oct 01 2022 at 06:36 UTC