A Collaborative Cloud-Based IDE for Lean 4

Stream: general

[Joachim Breitner]

In response to
#announce > A Collaborative Cloud-Based IDE for Lean 4

Impressive!

[Joachim Breitner]

Is it sufficient for people to contribute to mathlib exclusively on that system? (E.g. can it use lake exec cache, can you create PRs from it and do the necessary git merged)

[Alissa Tung]

@Joachim Breitner

Not yet, sorry, in the ideal case, contributors should be able to fork seamlessly, edit, run CI, benchmarks, linters, etc., all within the system. However, at the moment the workflow is still more manual: 1. Users need to fork the repository on GitHub themselves 2. Import the project from GitHub into the system 3. Sync with GitHub 4. Open PRs manually on GitHub

So there is still a lot of room for improvement. Contributing to mathlib typically requires running CI, benchmarks, linters, and other checks, and review, and we are still quite far from making mathlib contributions fully smooth and end-to-end inside the system.

This entire workflow is on our roadmap. Our team includes several mathlib contributors, and in their spare time they can help review and iterate on improvements to better support this use case. If we can integrated all pipeline including the PR review comments, I think it might be nice

[Joachim Breitner]

(Also, https://reaslab.io/ doesn’t work, cloudflare error. Not sure if there should be something there, I was just curious)

[Alissa Tung]

@Joachim Breitner

(Also, https://reaslab.io/ doesn’t work, cloudflare error. Not sure if there should be something there, I was just curious)

At this time, only with prove. prefix has DNS. ( https://prove.reaslab.io/ ). Let me add redirection from reaslab.io to prove.reaslab.io later

update: done

[Notification Bot]

8 messages were moved here from #new members > A Collaborative Cloud-Based IDE for Lean 4 by Kevin Buzzard.

[Snir Broshi]

The IDE does not look based on VSCode, did you build your own integration with Lean?
Also, is it Monaco or CodeMirror? Does it have a dark theme?
Beautiful font choice btw, looks similar to JetBrains Mono

[Robin Carlier]

I cannot find the data and privacy policy on the webpage.

[Patrick Massot]

Isn’t “Join thousands of mathematicians, students, and researchers already using ReasLab IDE” a little bit exaggerated?

[Patrick Massot]

And the Lean 3 liquid tensor experiment project is described as “A Lean 4 library for liquid tensor experiments, which are a new way to study quantum field theories.”…

[Bbbbbbbbba]

How do I use Mathlib in a project I create with the web UI?

[Alissa Tung]

Patrick Massot said：

Isn’t “Join thousands of mathematicians, students, and researchers already using ReasLab IDE” a little bit exaggerated?

Yes, I am sorry, that was a review mistake on my part. My colleague and I are updating the site to remove that claim and make it more accurate.

The current number of registered users for public preview and internal use is 500+, (which I know does not reflect actual active users, as some people may have signed up out of curiosity). Sorry for the confusion, and thanks for pointing this out.

[Gavin Zhao]

Is there no dark mode for the playground :pleading_face:

[Alissa Tung]

Patrick Massot said：

And the Lean 3 liquid tensor experiment project is described as “A Lean 4 library for liquid tensor experiments, which are a new way to study quantum field theories.”…

Yes, the description of the project is completely wrong. This happened because the initial templates were put together by my non-math background classmate who helped with the project, and I failed to review them carefully before publishing. I apologize for the confusion. Thank you for pointing this out. It was my responsibility to review these descriptions. :cry: I will fix this, sorry

[Patrick Massot]

In this particular case you should simply remove this item, unless your infrastructure indeed supports the completely obsolete Lean 3.

[Alissa Tung]

Robin Carlier said：

I cannot find the data and privacy policy on the webpage.

Sorry for that we don't currently have a published privacy policy. This project started as a side product from some Lean seminars we ran, and we haven't yet write these documents. We're drafting them now and will have legal help to review them.

If you have any data deletion or privacy requests, please contact me. If there is questions about data privacy I'll respond promptly to any concerns publicly. That is our responsibility, sorry.

[Alissa Tung]

Bbbbbbbbba said：

How do I use Mathlib in a project I create with the web UI?

Currently this does not work. We recently switched to a custom modified Lean language server for performance reasons, as running upstream Lean was too resource intensive for multiple user scenarios.

However, this modified version doesn't yet support modifying project dependencies through the web UI. This is a regression we're aware of and working on.

As a workaround, you can import existing projects that already include Mathlib as a dependency, such as FLT. We're working on restoring this functionality.

[Alissa Tung]

Gavin Zhao said：

Is there no dark mode for the playground :pleading_face:

Oh, you're right! We missed this. Working on it now.

[Alissa Tung]

Snir Broshi said：

The IDE does not look based on VSCode, did you build your own integration with Lean?
Also, is it Monaco or CodeMirror? Does it have a dark theme?

Yes, it's not based on VS Code. We built this using CodeMirror 6 and React. Dark theme is currently available in the projects editor, but not yet in the playground or other parts of the UI. Working on fix this.

Initially, we built our own Infoview renderer, but it became incompatible as Lean evolved. We now use a modified version of the one from the official Lean 4 VS Code extension. There is a plan to switch back to use custom renderer because we are adding some features to it.

I initially tried to modify the open source version of VS Code but couldn't make it work. I think this is because I don't have much frontend experience initially at that time. My background is in compilers.

I chose CodeMirror over Monaco because writing extensions in CodeMirror is easier and it has more documentation. Without much frontend experience at the time, debugging Monaco was difficult for me.

[Joachim Breitner]

Alissa Tung schrieb:

We now use a modified version of the one from the official Lean 4 VS Code extension

People have tried that and then failed to keep up with changes. Do you think you’ll be able to? (Ok, loaded question. No need to answer, this is more a friendly warning than a question :-))

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Alissa Tung said:

We recently switched to a custom modified Lean language server for performance reasons, as running upstream Lean was too resource intensive for multiple user scenarios.

Are you able to give any more detail about this? What kind of performance issues were you running into? What modifications did you make?

[Alissa Tung]

Joachim Breitner said：

Alissa Tung schrieb:

We now use a modified version of the one from the official Lean 4 VS Code extension

People have tried that and then failed to keep up with changes. Do you think you’ll be able to? (Ok, loaded question. No need to answer, this is more a friendly warning than a question :-))

I think the Lean server RPC API is relatively stable now compared to earlier versions. I've spent much time reading through the Lean server source code, and I have a better understanding of React, so I feel technically prepared for this. (To be honest though, my concern is I'm hoping I can balance this with my coursework and not get overwhelmed. But I think the current timing is right to build something.)

[Alissa Tung]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said：

Alissa Tung said:

We recently switched to a custom modified Lean language server for performance reasons, as running upstream Lean was too resource intensive for multiple user scenarios.

Are you able to give any more detail about this? What kind of performance issues were you running into? What modifications did you make?

The main performance issue is similar to running multiple Lean projects simultaneously on a regular computer. As the number of concurrent users increases, server resource consumption up.

As for the specific modifications, I'm not ready to share the details yet because there are still much restriction, and which is not neat. I'm currently running a larger experiment related to this, and I'd prefer to write a proper technical blog post once I have more results and the approach is more stable.

[Snir Broshi]

Alissa Tung said:

I chose CodeMirror over Monaco because writing extensions in CodeMirror is easier and it has more documentation. Without much frontend experience at the time, debugging Monaco was difficult for me.

As a datapoint: non-Monaco is a nonstarter for me, CodeMirror slows me down significantly (like Overleaf :sob:) since it lacks many code-editing features. Is there any chance you'll switch in the future?

If this is open source I can try to help, I've integrated Monaco to a few projects. I don't know if my preference is the majority though, maybe others like CodeMirror.

Also, a VSCode extension can be adjusted to support VSCode-web, so maybe this can even use the official extension?

[Alissa Tung]

@Snir Broshi

Oh, that makes sense! I'm an Emacs user, so I definitely understand the importance of good editing features. May I ask are the editing features in Monaco built-in, or do they come from extensions?

And thank you for feedback and helping, currently there is no soon plan about open source, since I think there is a lot room to improvement before build with community.

I have tried to use things like Monaco VS Code services override. But I find they are not easy to debug, and there are many undocumented assumption in different override, and the source code is not very easy to read. Hence I refactored all codebase to build around CodeMirror.

[Snir Broshi]

Alissa Tung said:

May I ask are the editing features in Monaco built-in, or do they come from extensions?

Mostly built-in (multiple selections is the most important), but some extensions such as Error Lens (shows errors/warnings right next to the code) save a lot of time. AFAIK CodeMirror does not properly support multiple selections (it seems to have rudimentary support using the mouse for some reason).

[Miguel Marco]

Do you plan to publish the code under a free license?

[Alissa Tung]

Snir Broshi said：

Mostly built-in

That's good news! I'm trying to add VS Code style key maps first and test it myself. If that doesn't work, we can add an alternative editor later.

Adding key maps is faster because there's already a package @replit/codemirror-vscode-keymap. I'm currently figuring out conflicts after integrating it with our key map system (multi-cursor selection isn't working yet, still reading through the source code to see if the package provides it). Adding an alternative editor would take longer, and I don't have an estimated timeline for that yet.

[Alissa Tung]

Miguel Marco said：

Do you plan to publish the code under a free license?

We're still discussing our licensing strategy. Some reusable components will likely be open sourced first, but still need to clean up the codebase to a shareable quality before meet the community. As for the platform itself is still under consideration.

[Snir Broshi]

Keymaps can't add features, they'll only map keys. If you're investing time in adding such a thing, maybe add Vim/Emacs modes instead? They're somewhat supported by CodeMirror.

[Malvin Gattinger]

Is this multi-user IDE working for anyone at the moment? :thinking: I tried it out just now in Firefox and Chromium but the suggested templates only give me empty files and also after creating or importing my own project/files I cannot get any Lean server feedback besides "No info found." Logging in also seems buggy, I was immediately logged out and redirected to the home page the first time.

[Malvin Gattinger]

Oh wait, while writing my complaint it started to work in some files. This needs a progress or "please wait" indicator :wink:
And in more complicated / "later" files in the import hierarchy I now get Error updating: Error fetching goals: Rpc error: undefined: [unknown] HTTP 500. [Try again.]().