(interactive) conv mode

Stream: mathlib4

[Jakob von Raumer]

Hi all, I'm considering posing the porting of conv and the creation of a more interactive "code action" for the Lean Info View widget (in which you could just select the focussed subterm with a mouse click) as a Bachelor's thesis. Do you think this is a good idea? What's the current status of conv in mathlib4?

[Mario Carneiro]

conv mode already exists in lean 4 core in some form, but I'm not sure about the widget support

[Mario Carneiro]

example (h : ∀ x, x = 0) : (fun x : Nat => (x + x) + x - x - x) = id := by
  conv =>
    arg 1
    enter [i, 1, 1, 1]
    rw [h i]
  trace_state

[Jakob von Raumer]

Yes, just dicovered that, seems to work pretty well actually! :)

[Mario Carneiro]

I'm not so sure about the choice of |- for the goal sigil; in lean 3 it was | but that might not be super clear either

[Jakob von Raumer]

It should be distinguishable at least

[Jakob von Raumer]

image.png

[Jakob von Raumer]

It always shows Prop for the "root" term

[Gabriel Ebner]

Ooh, this is a bug in two ways: it should be Nat instead of Prop, and it should be @OfNat.ofNat ... instead of 2.

[Wojciech Nawrocki]

Oh, fun! In fact, @Edward Ayers and I have been considering prototyping exactly this (subterm selection to work with conv and rw) on the widgets side but the work had not begun in earnest. Since we would have to focus on the infrastructure, having a student around to write some of the user-facing parts would certainly help :)

[Jakob von Raumer]

The student has since decided to go for another project unfortunately :( But maybe @Sebastian Ullrich and I will get some interested students out of our course in the summer term.

[Tomas Skrivan]

I would totally love to have an interactive conv, in particular have commands simplify, factor, expand etc. like in Mathematica. The you could select a term in some ring and transform it to desirable form.

Also I'm working on symbolic differentiation in Lean and this would be super useful for more user friendly experience.

[Kevin Buzzard]

To turn a term of a ring into a required form in Lean 3 I usually use rw (show current_term = required_form, by ring). No conv needed!

[Tomas Skrivan]

But for example if I want to turn polynomial to its Horner form. I do not know what the final coefficients are. I want the computer to figure that out i.e. scenarios where you do not know the explicit required_form or it is too long to type.

[Alex J. Best]

In mathlib3 ring_nf would do this for you, I'm not sure how far Mathlib4's has progressed yet though

[Jakob von Raumer]

Wojciech Nawrocki said:

Oh, fun! In fact, Edward Ayers and I have been considering prototyping exactly this (subterm selection to work with conv and rw) on the widgets side but the work had not begun in earnest. Since we would have to focus on the infrastructure, having a student around to write some of the user-facing parts would certainly help :)

What's the status of this, @Edward Ayers and @Wojciech Nawrocki ? I do now have an interested student to work on it :)

[Edward Ayers]

We've got all the infrastructure set up for Lean to send javascript to and from the infoview. We need to get that merged in to vscode-lean4 and also release a utility library. We haven't done any work on the actual interactive conv mode yet so now would be a great time for the interested student to start working on it :smile:

[Jakob von Raumer]

Sounds great!

[Jakob von Raumer]

Is there any infrastructure to modify the document syntax tree yet? (To insert the appropriate congr and skip calls)

[Wojciech Nawrocki]

@Jakob von Raumer On the typescript side, we have insertText. On the server side, there is LSP's applyEdit. We do not currently have Syntax-aware infrastructure, i.e. an ability to modify files at the AST level and then have the edited text be pretty-printed AST, which would be safer (i.e. it wouldn't be as easy to insert nonsensical text that doesn't parse). Developing this could be a part of the project, but it could also probably get away with just direct string manipulation (Lean 3 just does this).

Do you have a timeline for when the project would be happening? We are currently working to release an MVP of the necessary APIs and some documentation.

[Jakob von Raumer]

Bachelor projects have duration of 3mo usually but it's possible to stretch it a bit. Getting it to work is definitely more important than hygiene

[Jakob von Raumer]

He's starting next week, but he's first gonna get into the codebase and into Lean as a programming language itself

[Jakob von Raumer]

Can you give us starting points in vscode-lean4 and Lean itself? What are the directories we should be looking at first?

[Wojciech Nawrocki]

Probably the easiest entry point at the moment is this demo branch. It contains examples of user widgets with the UI written in Typescript (widget/ folder) and the server-side implemented using an @[rpc] attribute. Note that for the UI to work, you need to install the .vsix from the root folder which contains a custom build of vscode-lean4 (from this branch; we will PR it eventually, but for now installing that is the way to go). You can also try it in Gitpod.

[Jakob von Raumer]

Thanks a bunch, that's super useful to us :smile: :octopus: /cc @Robin Böhne