Lean web editor

Stream: general

[Mohamamd Awheeo]

Hello, I am creating an application to test a concept I am working on. That requires me to include simple version of lean editor in a web/desktop application. the idea I am trying to test is based on lean 3, I have taken found the( lean-client-js-browser library) . however I did not find much information on how to use it. is there a resource that I can use to build a incorporate a simple lean editor in a web application? something similar to the natural number game

[Alex J. Best]

I think you'd be much better off starting with https://github.com/leanprover-community/lean4game by @Jon Eugster as it is still actively maintained unlike much of the lean 3 stuff

[Martin Dvořák]

If you want editor like https://lean.math.hhu.de/ ask @Alexander Bentkamp.

[Alexander Bentkamp]

The code of the web editor is here: https://github.com/leanprover-community/lean4web

[Jon Eugster]

One caveat is that these web application communicate with lean running normally in a docker container on our server. Nobody has written anytjing yet to run lean4 in js in the browser directly, and some people suggest that would be hard.

But depending on your usage you could take inspiration from either of our projects linked above.
Also happy to dm about any specific questions/ideas you have :blush:

[Jon Eugster]

but thats all lean4, if you are specifically asking about lean3, then I've got no clue

[Mohamamd Awheeo]

Jon Eugster said:

One caveat is that these web application communicate with lean running normally in a docker container on our server. Nobody has written anytjing yet to run lean4 in js in the browser directly, and some people suggest that would be hard.

But depending on your usage you could take inspiration from either of our projects linked above.
Also happy to dm about any specific questions/ideas you have :blush:

Thanks!

[Jon Eugster]

Could I ask for a favour from some Windows people, as I don't yet have a VM set up to test? According to @Eric Wieser, the updated version at lean.math.hhu.de does not work on Windows, in particular the infoview newer starts up. Could you please try and confirm? Is there anything suspicious in the browser console (besides one warning labelled TODO:, which shouldn't be relevant)?

Especially, could you tell me here if it (a) does work on your Windows machine or (b) does NOT work on a Mac/Linux computer...

[Yaël Dillies]

Indeed, I'm on Windows and the infoview has now been loading for two minutes

[Johan Commelin]

/me :penguin: :check:

[Floris van Doorn]

Can confirm that the infoview doesn't load on Windows.
In Firefox I get the following console messages

Preferences: Loading. index-CgY3Gf0L.js:1867:17741
Preferences: Set dark theme. index-CgY3Gf0L.js:1867:18100
width: 1069 index-CgY3Gf0L.js:1867:18324
Restarting Editor! index-CgY3Gf0L.js:1867:18460
socket url: wss://lean.math.hhu.de/websocket/mathlib-demo index-CgY3Gf0L.js:1867:18596
editor is ready index-CgY3Gf0L.js:1869:423
content changed index-CgY3Gf0L.js:1869:245
Successfully compiled asm.js code (total compilation time 4ms) webview.js
Object { "@leanprover/infoview": "/infoview/index.production.min.js", react: "/infoview/react.production.min.js", "react/jsx-runtime": "/infoview/react-jsx-runtime.production.min.js", "react-dom": "/infoview/react-dom.production.min.js" }
webview.js:1:39499
TODO: catch JSON.parse failure:  SyntaxError: JSON.parse: unexpected character at line 1 column 1 of the JSON data
    <anonymous> https://lean.math.hhu.de/infoview/webview.js:1
webview.js:1:39093
TODO: data which is not JSON:
Array(7) [ "esms", true, true, false, false, false, false ]
webview.js:1:39144
09:14:54.820 - [InfoProvider] initInfoView got null client. index-CgY3Gf0L.js:1125:13673
Source map error: Error: URL constructor:  is not a valid URL.
Resource URL: wasm:https://lean.math.hhu.de/infoview/webview.js
Source Map URL: null

On Chrome I get the following

Preferences: Loading.
index-CgY3Gf0L.js:1867 Preferences: Set dark theme.
index-CgY3Gf0L.js:1867 width: 958
index-CgY3Gf0L.js:1867 Restarting Editor!
index-CgY3Gf0L.js:1867 socket url: wss://lean.math.hhu.de/websocket/mathlib-demo
index-CgY3Gf0L.js:1869 editor is ready
index-CgY3Gf0L.js:1869 content changed
 [object Object]
 TODO: catch JSON.parse failure:  SyntaxError: Unexpected token 'e', "esms,true,"... is not valid JSON
(anonymous) @ webview.js:1
 TODO: data which is not JSON:  esms,true,true,false,false,false,false
index-CgY3Gf0L.js:1125 09:16:22.449 - [InfoProvider] initInfoView got null client.
index-CgY3Gf0L.js:1867 width: 150
index-CgY3Gf0L.js:1867 Restarting Editor!
index-CgY3Gf0L.js:1867 socket url: wss://lean.math.hhu.de/websocket/mathlib-demo
index-CgY3Gf0L.js:1869 editor is ready
index-CgY3Gf0L.js:1869 content changed
webview.js:1 {@leanprover/infoview: '/infoview/index.production.min.js', react: '/infoview/react.production.min.js', react/jsx-runtime: '/infoview/react-jsx-runtime.production.min.js', react-dom: '/infoview/react-dom.production.min.js'}@leanprover/infoview: "/infoview/index.production.min.js"react: "/infoview/react.production.min.js"react-dom: "/infoview/react-dom.production.min.js"react/jsx-runtime: "/infoview/react-jsx-runtime.production.min.js"[[Prototype]]: Object
webview.js:1 TODO: catch JSON.parse failure:  SyntaxError: Unexpected token 'e', "esms,true,"... is not valid JSON
    at JSON.parse (<anonymous>)
    at webview.js:1:39061
(anonymous) @ webview.js:1
postMessage
(anonymous) @ VM39:1
Promise.then
(anonymous) @ VM39:1
s @ webview.js:1
(anonymous) @ webview.js:1
(anonymous) @ webview.js:1
Promise.then
(anonymous) @ webview.js:1
(anonymous) @ webview.js:1
(anonymous) @ webview.js:1
webview.js:1 TODO: data which is not JSON:  (7) ['esms', true, true, false, false, false, false]
index-CgY3Gf0L.js:1125 09:16:28.606 - [InfoProvider] initInfoView got null client.