Zulip Chat Archive

Stream: general

Topic: Lean 4 talk on Zoom


view this post on Zulip Mario Carneiro (Jun 18 2020 at 11:34):

There is a Lean 4 presentation by Leo & Sebastian in about 90 minutes at PLDI: https://pldi20.sigplan.org/track/pldi-2020-sponsors?date=Thu%2018%20Jun%202020#program . There is a meeting password but I will PM it to anyone who voices an interest if I can.

view this post on Zulip Patrick Massot (Jun 18 2020 at 11:35):

Aarg, I have another meeting. Will it be recorded?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 11:35):

no word yet

view this post on Zulip Patrick Massot (Jun 18 2020 at 11:36):

Could you record it?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 11:38):

All the main conference presentations have been livestreamed on youtube, but these sponsored talks are only on zoom for some reason

view this post on Zulip Mario Carneiro (Jun 18 2020 at 11:39):

It's a big and well organized conference so I'd rather not do anything without approval here

view this post on Zulip Chris Hughes (Jun 18 2020 at 11:57):

Can I have a password?

view this post on Zulip Ashvni Narayanan (Jun 18 2020 at 12:11):

Can I have the password?

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 12:36):

Leo and Sebastian are already here. The password is also included on the PLDI conference website link, BTW.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 12:39):

If you mean the pwd=... in the link, I don't believe so

view this post on Zulip Mario Carneiro (Jun 18 2020 at 12:40):

if you try it you will get a password request from Zoom

view this post on Zulip Mario Carneiro (Jun 18 2020 at 12:40):

or at least I did

view this post on Zulip Reid Barton (Jun 18 2020 at 12:40):

well it worked for me somehow

view this post on Zulip Reid Barton (Jun 18 2020 at 12:40):

I took the obvious step at that point

view this post on Zulip Ashvni Narayanan (Jun 18 2020 at 12:40):

Worked for me too

view this post on Zulip Mario Carneiro (Jun 18 2020 at 12:40):

Ah, that's great then

view this post on Zulip Mario Carneiro (Jun 18 2020 at 13:00):

It looks like Leo will be recording it, so with any luck it will appear on youtube later

view this post on Zulip Reid Barton (Jun 18 2020 at 13:03):

@Sebastian Ullrich Could you mute your mic while typing

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

This is the zoom link: https://us02web.zoom.us/j/85379682400?pwd=c3kzbTZidXk1UENMR1Y0ZlhqTXJWZz09

view this post on Zulip Kenny Lau (Jun 18 2020 at 13:13):

Something went wrong
The server encountered an internal error and was unable to process your request.
Error Code:3000

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

That link is public: from the webpage that Mario linked.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 13:20):

Slides: http://leanprover.github.io/talks/LeanPLDI.pdf

view this post on Zulip Yury G. Kudryashov (Jun 18 2020 at 14:06):

Did I hear correctly "release by the end of the summer"?

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 14:44):

Did he say which summer?

view this post on Zulip Chris Hughes (Jun 18 2020 at 14:45):

This one.

view this post on Zulip Chris Hughes (Jun 18 2020 at 14:46):

And 99% of porting mathlib will be automatic.

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

Will the release include VS Code support?

view this post on Zulip Chris Hughes (Jun 18 2020 at 14:47):

But someone has to write a version of simp in Lean 4 that behaves exactly the same as Lean 3 simp.

view this post on Zulip Chris Hughes (Jun 18 2020 at 14:47):

@Bryan Gin-ge Chen i don't remember that being discussed.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 14:49):

99% of what? Obviously not 99% of human effort by definition

view this post on Zulip Rob Lewis (Jun 18 2020 at 14:50):

Chris Hughes said:

And 99% of porting mathlib will be automatic.

In some vague sense yes. The non-meta part can be dumped into a Lean 4 environment to be used, but you don't get ported source code. I don't remember anything said about automated translation.

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 14:50):

Obviously 99% of the effort is changing mathlib to use the new NamingConvention.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 14:50):

wasn't something like that written for lean 4 already?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 14:50):

for the core library

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 14:51):

Yes, which makes porting mathlib almost effortless!

view this post on Zulip Mario Carneiro (Jun 18 2020 at 14:51):

@Sebastian Ullrich Does the lean 4 emacs mode use any LSP extensions? What are the plans for the goal view?

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 14:51):

@Sebastian Ullrich Have you seen @Edward Ayers's work on the widgets?

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 15:05):

We want the LSP basics without extensions working first, but an extension for ITP-specifc parts like the goal view will likely be necessary, yes. I've seen a bit of talk and commits about the widgets, but from the toy examples it wasn't clear to me what the goal here is. We were planning on having inspectable and interactive error messages, but not arbitrary UI elements. But I don't think this will be part of the first release anyway.

view this post on Zulip Marc Huisinga (Jun 18 2020 at 15:05):

as the person responsible for the lean 4 server, i'll chime in.

the lean 4 emacs mode currently shows only errors.
i'm still working on getting lsp and most useful features up and running, but i should have a lot more time for lean4 towards the end of the summer, so that i can tackle the goal view :)

i'm aware of the widget extension.

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

The endgoal of widgets is things like:

  • interactively inspecting terms
  • highlighting a variable also highlights the other instances of that variable
  • being able to hover over subterms in the tactic state, click on them and see available rewrites for that subterm
  • a list of tactics available for a given goal that can be activated and pushed to the sourcetext with a button
  • custom visualisations of structures like matrices and graphs
  • support for rendering latex expressions in the goal view
  • interactively filtering hypotheses

Giving Lean a UI system means that all of these become possible from within Lean without having to modify C++, Lean and javascript and push to lean-client-js, vscode-lean and lean.

view this post on Zulip Marc Huisinga (Jun 18 2020 at 15:19):

some of these things should already be possible via regular LSP (once these features are implemented), while we might need to extend LSP for others. i'll definitely keep this in mind, thanks for the list!

view this post on Zulip Edward Ayers (Jun 18 2020 at 15:21):

The point I'm trying to make is not really about specific UI features though. Allowing arbitrary, interactive UI in the output window makes for a much more compelling tool, particularly for beginners, and opens up a large space of creative uses of lean.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 15:24):

Is this cross editor supported though? It seems like this is just exposing vscode functionality to lean

view this post on Zulip Mario Carneiro (Jun 18 2020 at 15:25):

replicating this if someone wants to write a lean mode for their favorite editor seems pretty hard

view this post on Zulip Mario Carneiro (Jun 18 2020 at 15:26):

which kind of defeats the point of using LSP (not completely, but largely)

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

afaik LSP doesn't support any kind of goal view ootb, so you already need to go beyond LSP to implement a good lean client. In principle you could include the widgets client code in any editor with the capability to support a web browser frame, so I admit that you would need to open a separate web-browser window for a terminal-based editor like emacs and vim. But the text-based goal view would still be there in any case.

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 15:49):

Mario Carneiro said:

Is this cross editor supported though? It seems like this is just exposing vscode functionality to lean

Yeah, that would my concern, too. I guess pushing HTML to the client would be perfect for VS Code, but as a (then former?) Emacs user I would feel a little sad. But that's the insignificant minority of users of course.

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 15:49):

Doesn't emacs have a web browser?

view this post on Zulip Edward Ayers (Jun 18 2020 at 15:51):

Maybe a better way to do it would be that you keep LSP, but also the lean server opens a local port that you can point your browser at to see the fancy UI stuff. So all of the widget-rendering code becomes completely independent of the editor

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 15:54):

Gabriel Ebner said:

Doesn't emacs have a web browser?

Yes, but it's not exactly pretty... https://en.wikipedia.org/wiki/Eww_(web_browser)#/media/File:Eww_GNU_Emacs_24.4.png. But maybe that's sufficient, I don't know.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 15:59):

lol who names their browser "eww"?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 15:59):

not exactly confidence-inspiring

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 16:00):

"Emacs Web Wowser"

view this post on Zulip Bhavik Mehta (Jun 18 2020 at 16:01):

"So this Monday, I came up with the name of the browser while half-asleep: eww! I don’t quite know what the second w is supposed to stand for (Emacs Web Wowser?), but now that I had a name I just had to start programming."

view this post on Zulip Reid Barton (Jun 18 2020 at 16:04):

I was definitely expecting to see Sebastian test the webserver demo with an emacs web browser

view this post on Zulip Edward Ayers (Jun 18 2020 at 16:05):

I don't want to rain on the text based editor parade too much and I don't want to kick them out. But I believe that to get mass adoption of ITP by non-programmers, there needs to be a move away from representing proof state as non-interactive tiles of unicode.

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 16:06):

It looks like emacs has a fairly extensible HTML renderer: https://github.com/emacs-mirror/emacs/blob/717b0341aafb9ae9b93395dba1192b12c4459f0c/lisp/net/shr.el It might be feasible to render widgets in emacs, as long as the markup is written carefully.

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 16:44):

Ok, personally speaking I can very much see something like this being the future of ITP UIs. If it doesn't support Emacs very well, too bad for the Emacs users. So how much of this would actually have to be built into Lean 4? Would it be sufficient that plugins can customize the error/goal output and/or register custom LSP extensions?

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 16:48):

E.g. the Lean 4 elaborator supports embedding terms into messages. I don't think this would have to be generalized because inside the elaborator I don't see us having to report arbitrary widgets or anything. The bells and whistles can be added when the elaborator is done, when composing the response to the client.

view this post on Zulip Edward Ayers (Jun 18 2020 at 16:49):

The main core thing that I needed to change for widgets was modifying the pretty printer so that it also emitted some structural information mapping subexpressions to different parts of the format string, which I am a bit worried will be quite complicated to do with Lean 4 if it's not put in early. The actual UI engine doesn't need to be in core lean.

view this post on Zulip Edward Ayers (Jun 18 2020 at 16:50):

Sebastian Ullrich said:

E.g. the Lean 4 elaborator supports embedding terms into messages. I don't think this would have to be generalized because inside the elaborator I don't see us having to report arbitrary widgets or anything. The bells and whistles can be added when the elaborator is done, when composing the response to the client.

I agree with this

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 16:50):

Without having read your code, something like this :) ? https://github.com/kha/lean4/blob/master/src/Lean/Delaborator.lean#L19-L21

view this post on Zulip Edward Ayers (Jun 18 2020 at 16:52):

Is MetaM the new tactic?

view this post on Zulip Johan Commelin (Jun 18 2020 at 16:52):

You mean the new TactiC? :camel:

view this post on Zulip Sebastian Ullrich (Jun 18 2020 at 16:52):

It's basically the old type_context

view this post on Zulip Edward Ayers (Jun 18 2020 at 16:57):

Sebastian Ullrich said:

Without having read your code, something like this :) ? https://github.com/kha/lean4/blob/master/src/Lean/Delaborator.lean#L19-L21

This looks fab. The Delaborator is the right place to put this. The equivalent modification I made to this is that whenever the main delab is called, it wraps the resulting Syntax in something like tag : expr -> expr.address -> Syntax -> Syntax. Where expr.address is a list of constructor recursive argument names (eg ["app_fn", "app_arg", "lam_body"]) that points to the sub expression's location wrt the original expression.

view this post on Zulip Edward Ayers (Jun 18 2020 at 16:59):

So Syntax would be extended to play the role of tagged_format here: https://github.com/leanprover-community/lean/blob/master/library/init/meta/tagged_format.lean

view this post on Zulip Edward Ayers (Jun 18 2020 at 17:20):

I'm hoping that this can be adapted to get the desired result:

Pretty printer options can be given not only for the whole term, but also
specific subterms. This is used both when automatically refining pp options
until round-trip and when interactively selecting pp options for a subterm (both
TBD). The association of options to subterms is done by assigning a unique,
synthetic Nat position to each subterm derived from its position in the full
term. This position is added to the corresponding Syntax object so that
elaboration errors and interactions with the pretty printer output can be traced
back to the subterm.

view this post on Zulip Edward Ayers (Jun 18 2020 at 17:25):

I think descend is doing this right?

view this post on Zulip Sebastian Ullrich (Jun 19 2020 at 08:15):

Given an Expr and a synthetic Nat position from the delaborator, you should be able to reconstruct such an argument path, yes

view this post on Zulip Yury G. Kudryashov (Jun 19 2020 at 08:19):

I understand that you can't prove anything about an unsafe function. What about functions with @[extern]?

view this post on Zulip Sebastian Ullrich (Jun 19 2020 at 08:22):

It's a regular Lean definition in that aspect, but what you prove about it might not be true for the runtime implementation (the one given by @[extern])

view this post on Zulip James King (Jun 19 2020 at 20:20):

Sebastian Ullrich said:

Gabriel Ebner said:

Doesn't emacs have a web browser?

Yes, but it's not exactly pretty... https://en.wikipedia.org/wiki/Eww_(web_browser)#/media/File:Eww_GNU_Emacs_24.4.png. But maybe that's sufficient, I don't know.

The nice thing about it is that it works around sites which try to block normal browsers from seeing the publicly-searchable content with a special feature that asks for money first...

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 20:19):

https://youtu.be/8plFYifHHsE

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

ACM SIGPLAN have uploaded Leo's talk

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

This is old news, but I recommend watching it for everybody who hasn't already.

view this post on Zulip Lucas Viana (Jun 26 2020 at 02:59):

Sebastian's screen is cropped :oh_no:

view this post on Zulip Sebastian Ullrich (Jun 26 2020 at 08:23):

Oh wow, that's pretty bad

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:25):

Someone should send an anonymous link to an anonymized version of the rogue recording everybody watched.

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 09:10):

Ssh!

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 09:10):

It's not anonymously hosted...

view this post on Zulip Patrick Massot (Jun 26 2020 at 09:10):

That's why I wrote we need an anonymized version.

view this post on Zulip Scott Morrison (Jun 26 2020 at 12:18):

@Sebastian Ullrich, I have a better recording, if you want to offer it to the organisers.

view this post on Zulip Sebastian Ullrich (Jun 26 2020 at 12:19):

@Scott Morrison Yes, I received it! Thanks!

view this post on Zulip Sebastian Ullrich (Jul 01 2020 at 10:14):

Fixed version: https://youtu.be/TgHISG-81wM. Thanks again for the alternative source, @Scott Morrison !


Last updated: May 14 2021 at 03:27 UTC