Googling “lean web editor”

Stream: general

[Thomas Murrills]

I noticed that if you google “lean web editor” you see a few lean web editor results which are not http://live.lean-lang.org/, which is (to my understanding) the “official” playground. (Is that correct?)

Is there a reason it doesn’t come up? Could it be made to appear in the results somehow? I think it would be useful for it to be discoverable via Google search. :)

[Niels Voss]

For me the top result is: https://leanprover-community.github.io/lean-web-editor/, which is for Lean 3. It might be worth adding a link to the current web editor to it.

[Scott Morrison]

I would suggest we just replace it with a redirect to the Lean 4 editor.

[Scott Morrison]

Unfortunately I can't work out where the redirect even lives. The string lean-web-editor doesn't appear in the lean4 branch of the repository, and only in the master branch in links from the sidebar.

[Heather Macbeth]

Scott Morrison said:

I would suggest we just replace it with a redirect to the Lean 4 editor.

I actually use it more now than I used to: it's the fastest way to refresh my memory on "did X work in Lean 3" without having to get a local copy of Lean 3. Can we keep it (but also have some kind of banner offering the redirect)?

[Scott Morrison]

Sure!

[Scott Morrison]

Do you happen to know where it is hosted? I'm not even sure which repository to look in to add a banner.

[Kevin Buzzard]

My method for
"Did it work in lean 3" is "ask Bhavik or Yael" :-)

[Heather Macbeth]

I think https://github.com/leanprover-community/lean-web-editor ?

[Scott Morrison]

I'm a bit cautious here. The file https://github.com/leanprover-community/lean-web-editor/blob/master/src/index.tsx#L293 contains the string "Live in-browser version", but not "Load .lean from URL", so I'm unconvinced that editing this file will have the desired effect.

[Scott Morrison]

Who used to maintain this?

[Heather Macbeth]

@Bryan Gin-ge Chen I think (thank you Bryan!)

[Jon Eugster]

Thomas Murrills said:

Is there a reason it doesn’t come up? Could it be made to appear in the results somehow? I think it would be useful for it to be discoverable via Google search. :)

I think it also takes google a few weeks to promote new links like that, but if anybody knows what keywords to add where to help the search engines, a PR at lean4web is most welcome

[Yaël Dillies]

Kevin Buzzard said:

My method for
"Did it work in lean 3" is "ask Bhavik or Yael" :-)

My method for replying to Kevin is answer "Yes" :wink:

[Eric Wieser]

Heather Macbeth said:

Bryan Gin-ge Chen I think (thank you Bryan!)

I did some maintenance on it a few months ago, and could add the banner

[Jon Eugster]

I just noticed that the links at https://leanprover-community.github.io/ still point to lean.math.hhu.de, maybe somebody could edit the community website.

And I couldnt find a link on lean-lang.org to the webeditor at all. A more prominent link there would also help google

[Eric Wieser]

I think we can safely move the lean 3 web editor to have "lean3" in the url

[Eric Wieser]

Scott Morrison said:

I'm a bit cautious here. The file https://github.com/leanprover-community/lean-web-editor/blob/master/src/index.tsx#L293 contains the string "Live in-browser version", but not "Load .lean from URL", so I'm unconvinced that editing this file will have the desired effect.

The second string is wrapped across two lines

[Eric Wieser]

Eric Wieser said:

I think we can safely move the lean 3 web editor to have "lean3" in the url

I've moved it, lets see if

example := "this lean3 code"

continues to work.

[Eric Wieser]

(https://github.com/pygments/pygments/pull/2546 will fix the above so that it syntax-highlights)

[Eric Wieser]

Eric Wieser said:

I think we can safely move the lean 3 web editor to have "lean3" in the url

Nope, github pages doesn't set up any redirects, so any links to it break. I'll move it back.

[Bryan Gin-ge Chen]

Thanks Eric! It seems like you've got a handle on things now but let me know if there's anything I can help with.

[Alexander Bentkamp]

Updating the wikipedia article and linking to the web editor might help google to pick it up.

[Eric Wieser]

Changing the title of the editor already helps:

image.png

@Scott Morrison, can you delete https://tqft.net/lean/web-editor/ to remove one item from that list?

[Eric Wieser]

renaming https://github.com/leanprover/lean-web-editor to https://github.com/leanprover/lean3-web-editor (and replacing "lean" with "lean 3" in the description, and archiving it) would help too. That one is no longer hosted anywhere anyway.

[Sebastian Ullrich]

Done, thanks

[Scott Morrison]

Eric Wieser said:

Scott Morrison, can you delete https://tqft.net/lean/web-editor/ to remove one item from that list?

Done!