vs code web extension?

Stream: general

[Matthew Ballard]

I learned recently that if you navigate to a GitHub repo and hit ., a web-based version of VS Code will render. (This also works if you go to github.dev or replace the .com with .dev in the URL of your repo.) This kinda blew my mind.

A main downside is that use of extensions is limited. It only supports web extensions.

How reasonable would it be to make a web extension version of the Lean VS Code extension using the wasm-compiled version of Lean ?

A use case I had in mind would be teaching a course through GitHub classroom.

[Matthew Ballard]

Another use case is currently filled by the Lean web editor

[Bryan Gin-ge Chen]

Based on a (very quick) scan of the web extensions page you linked, hooking up the WASM version of the server to the extension looks like it might be doable, but with a lot of work.

Actually, one thing which looks rather hairy to me is how to deal with the olean files that you would need for projects depending on mathlib or large projects in general. The WASM version of Lean 3 reads olean files from .zip files that are (currently) prepared separately, and we're only building them for the latest commit for mathlib at the moment.

[Bryan Gin-ge Chen]

Even if this is set up, I suspect a gitpod like setup where your browser communicates with Lean running on a remote server will be much more usable than the WASM server, since the WASM compiled Lean runs single threaded.

[Matthew Ballard]

I imagined that speed might be severely comprised.

[Matthew Ballard]

I should say that if you pay for Codespaces then you get the same UX but with a basically full-featured VS Code.

[Matthew Ballard]

Is communicating with a language server over http a bad idea?

[Bryan Gin-ge Chen]

Matthew Ballard said:

Is communicating with a language server over http a bad idea?

I'm not sure! I don't have any experience with language servers going through http, unfortunately.

[Matthew Ballard]

MSFT has this bare-bondes example for web worker based LSP but it still doesn't cover performance issues.

[Matthew Ballard]

Too bad there isn't some educational pricing for Codespaces.

[Arthur Paulino]

Matthew Ballard said:

Is communicating with a language server over http a bad idea?

I suspect a WebSocket might work better in the context of continuous exchange of information over a period of time

[Matthew Ballard]

You are definitely right. They live in the same area of my brain.

[Gabriel Ebner]

If codespaces ever becomes available to you, then it should work out of the box. It's also quite a bit faster to start up than gitpod.

[Matthew Ballard]

Isn't codespaces available to all org's now?

[Gabriel Ebner]

Codespaces is rolling out progressively on August 11th, 2021 and can be enabled in settings by organization owners for Team and Enterprise Cloud plans. For users in individual plans, we’re extending the existing Codespaces beta. For those in the beta, access will remain and we’ll share updates on what’s coming in the near future.

[Eric Wieser]

Is using github classroom with gitpod possible? Lean works quite well with gitpod in browser.

[Matthew Ballard]

Yeah. Integration of gitpod is simple with classroom. The flow is

• instructors create their own template repo for the homework
• they then import that into classroom
• when a student registers for an assignment, a repo is cloned for them with actions included for automated PRs (for feedback) and auto grading

A .gitpod.yml in the template should propagate to each student’s repo.

At a heuristic level, what I am asking for is not realistic: expose GH without exposing git. VS Code allows you to push some buttons to work with git which is better than CLI for a new student.

On a personal level, gitpod has taken upwards of minutes to pull containers so I just stopped using it

[Matthew Ballard]

Also, free is good because most instructors don’t have funding for course technology choices

[Matthew Ballard]

Currently I would probably upgrade my course org to a GH team and use codespaces. Especially for small courses, I can cover the cost with a grant. But this is not possible for everyone. If you want Lean to get a strong foothold in mathematics education, then a no-cost, friction-free, simple flow is required

[Matthew Ballard]

Another aspect: providing custom support for such a product, especially to enterprise, could be a means to fund Lean Mathlib development more broadly.