Zulip Chat Archive

Stream: general

Topic: Lean 4 talk on Zoom

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.

Patrick Massot (Jun 18 2020 at 11:35):

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

Mario Carneiro (Jun 18 2020 at 11:35):

no word yet

Patrick Massot (Jun 18 2020 at 11:36):

Could you record it?

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

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

Chris Hughes (Jun 18 2020 at 11:57):

Can I have a password?

Ashvni Narayanan (Jun 18 2020 at 12:11):

Can I have the password?

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.

Mario Carneiro (Jun 18 2020 at 12:39):

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

Mario Carneiro (Jun 18 2020 at 12:40):

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

Mario Carneiro (Jun 18 2020 at 12:40):

or at least I did

Reid Barton (Jun 18 2020 at 12:40):

well it worked for me somehow

Reid Barton (Jun 18 2020 at 12:40):

I took the obvious step at that point

Ashvni Narayanan (Jun 18 2020 at 12:40):

Worked for me too

Mario Carneiro (Jun 18 2020 at 12:40):

Ah, that's great then

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

Reid Barton (Jun 18 2020 at 13:03):

@Sebastian Ullrich Could you mute your mic while typing

Edward Ayers (Jun 18 2020 at 13:10):

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

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

Edward Ayers (Jun 18 2020 at 13:14):

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

Mario Carneiro (Jun 18 2020 at 13:20):

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

Yury G. Kudryashov (Jun 18 2020 at 14:06):

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

Kevin Buzzard (Jun 18 2020 at 14:44):

Did he say which summer?

Chris Hughes (Jun 18 2020 at 14:45):

This one.

Chris Hughes (Jun 18 2020 at 14:46):

And 99% of porting mathlib will be automatic.

Bryan Gin-ge Chen (Jun 18 2020 at 14:46):

Will the release include VS Code support?

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.

Chris Hughes (Jun 18 2020 at 14:47):

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

Mario Carneiro (Jun 18 2020 at 14:49):

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

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.

Gabriel Ebner (Jun 18 2020 at 14:50):

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

Mario Carneiro (Jun 18 2020 at 14:50):

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

Mario Carneiro (Jun 18 2020 at 14:50):

for the core library

Gabriel Ebner (Jun 18 2020 at 14:51):

Yes, which makes porting mathlib almost effortless!

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?

Gabriel Ebner (Jun 18 2020 at 14:51):

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

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.

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.

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.

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!

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.

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

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

Mario Carneiro (Jun 18 2020 at 15:26):

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

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.

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.

Gabriel Ebner (Jun 18 2020 at 15:49):

Doesn't emacs have a web browser?

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

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.

Mario Carneiro (Jun 18 2020 at 15:59):

lol who names their browser "eww"?

Mario Carneiro (Jun 18 2020 at 15:59):

not exactly confidence-inspiring

Gabriel Ebner (Jun 18 2020 at 16:00):

"Emacs Web Wowser"

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."

Reid Barton (Jun 18 2020 at 16:04):

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

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.

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.

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?

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.

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.

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

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

Edward Ayers (Jun 18 2020 at 16:52):

Is MetaM the new tactic?

Johan Commelin (Jun 18 2020 at 16:52):

You mean the new TactiC? :camel:

Sebastian Ullrich (Jun 18 2020 at 16:52):

It's basically the old type_context

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.

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

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.

Edward Ayers (Jun 18 2020 at 17:25):

I think descend is doing this right?

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

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]?

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])

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...