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!