rfc: three suggestions to improve the web editor

Stream: lean4

[Kenny Lau]

I frequently use the web editor to make and review mathlib PR's because, well, it takes 2 minutes to download mathlib cache and sometimes my vscode lean just gets stuck for no reason (I think it's because I have too many files open), so I've noticed three ways that the web editor maybe can be improved:

1. If I have a long file open and I edit the first part, every edit seems to be processed separately and each edit has to be processed before the next edit is processed, which effectively means that the entire file afterwards is updated for 20 times before everything starts working again, and ironically hitting the refresh button and letting it start again is faster. I have no clue actually how easy or hard this is to address.
2. To make it more like mathlib, maybe we can enable a feature where it will stop automatically accept unprovided vavriables, and also unspecified universe. (See example below)
3. Right-clicking an existing theorem and clicking "Go to definition" brings me to the doc page, which is helpful, but it doesn't bring me to the section automatically, because the anchorings are done differently between the editor (by line) and the doc pages (by name). (See example below)

[Kenny Lau]

Example for 2:

theorem foo (α : Type u) : x = x := rfl
-- This would not be accepted in Mathlib because `u` and `x` are not defined.
-- So this should throw an error in the web editor.

Example for 3:

import Mathlib.Logic.Function.Defs
#check Function.Bijective -- right click -> go to definition

[Henrik Böving]

1. To make it more like mathlib, maybe we can enable a feature where it will stop automatically accept unprovided vavriables, and also unspecified universe. (See example below)

Add set_option autoImplicit false to the top if you want that.

[Kenny Lau]

thanks!

[Eric Wieser]

Regarding 3, is there any hope of making the "peek definition" functionality work? Right now it shows a box with the filename and line number, but it's unable to load the actual file content

image.png

[Henrik Böving]

I think that should definitely be doable in theory yes.

[Kenny Lau]

Kenny Lau said:

1. each edit has to be processed before the next edit is processed

so I assume 1 is impossible?

[Shreyas Srinivas]

One can get all this with mathlib by opening it in codespaces or Ona (formerly gitpod). I hope the web editor stays as it is; as a scratchpad where one can use all Lean features by default including autoImplicits. The third point is worth filing a bug report about I guess.

[Eric Wieser]

Arguably import Mathlib is not any more a Lean feature than defaulting to autoImplicit false; both are a lakefile decision

[Kenny Lau]

Shreyas Srinivas said:

I hope the web editor stays as it is

for 2 i explicitly said "enable a feature", so like a button on the top that say "☐ mathlib mode"

[Eric Wieser]

Which I guess would also turn on the mathlib linters?

[Kenny Lau]

Actually, we can implement 2 today! it's via the example feature

image.png

we can just put an example that says "mathlib mode"

[Eric Wieser]

We could also implement it in the "latest mathlib" drop-down, since each choice is essentially choosing a lakefile

[Kenny Lau]

and that will change the whole file to:

import Mathlib

set_option autoImplicit false

universe u

-- code goes here...

#lint

[Eric Wieser]

That doesn't turn on the mathlib style linters

[Kenny Lau]

ah, the 'syntax linters', right

[Kenny Lau]

yeah i guess have an option on the bottom of the list that says "latest mathlib + mathlib mode"

[Jon Eugster]

Kenny Lau said:

3. Right-clicking an existing theorem and clicking "Go to definition" brings me to the doc page, which is helpful, but it doesn't bring me to the section automatically, because the anchorings are done differently between the editor (by line) and the doc pages (by name). (See example below)

I remember when I implemented that I gave up on the jumping to the right section because, I think monaco only exposed something line "file X, line 77" instead of the declaration name and the doc-gen pages didn't have any api to open "whatever is on line 77 of that file".

Regarding "peek definitons", there might be a chance to get that working if all bugs in the part which translates URIs to file names on disk are eliminated, but that's a rather fiddly matter, I think.

[Jon Eugster]

1. I would make a guess that there might be some RPC-calls/notifications which might need to be called to interrupt the Lean server. Maybe these need to be triggered explicitely by the monaco editor?

[Jon Eugster]

2. Feel free to PR any examples, it should be as easy as just adding a .lean file to the "mathlib" project. There are instructions on the lean4web repo.

In theory each project should also respect the options set in it's lakefile, so one could disable autoimplicits there just like mathlib does. However, that part is as fiddly as what's mentioned before, so it's likely broken again (basically some part of the lean4-vscode extension or lake does require that a file exists on disk without much reason. It will still work if the file doesn't exist, its just been decided that in that case no options from the lakefile will be applied).

(side note: Also, I personally think disabling auto-imolicits is a bad choice, they are an deliberate feature of Lean. And especially since that feature got added where autoimplicits are displayed by vscode/monaco its also easier to spot them)