lean and codespaces

Stream: general

[Johan Commelin]

I just found https://www.youtube.com/watch?v=D0ZpG1k_7gs
Seems interesting!

[Eric Wieser]

Github has a very similar codespaces feature

[Eric Wieser]

It would be neat if we could add the necessary config to the mathlib repo so that the code-space is autopopulated with lean, elan, the vs-code extension, etc

[Bryan Gin-ge Chen]

Neat! However, GitHub codespaces seems to be in beta right now: https://docs.github.com/en/free-pro-team@latest/github/developing-online-with-codespaces

[Johan Commelin]

I haven't looked into this closely, but might this also finally solve the "collaboration" issue?

[Eric Wieser]

My impressions is that this just gives us a way to combine the lean web editor with an interface that also lets us PR against mathlib (and any project using git) - and not that it makes it any easier to share a lean editor between multiple users

[Adam Topaz]

Johan Commelin said:

I haven't looked into this closely, but might this also finally solve the "collaboration" issue?

Please please please please please let's figure out a way to solve this issue!

[Gabriel Ebner]

I can't tell if multiple users can access the same codespace. If so, this would be the ultimate solution for collaboration. Even if only a single user can access it, it would be the ultimate replacement for the web editor.

[Matthew Ballard]

The open-source version of the Github version is https://github.com/cdr/code-server. Lean extension works perfectly.
https://github.com/cdr/code-server/blob/v3.6.2/doc/FAQ.md#how-is-this-different-from-vs-code-codespaces

[Johan Commelin]

But you have to pay. (After 12 months of free trial, if I understand correctly.)

[Kevin Lacker]

what is the "collaboration" issue?

[Adam Topaz]

vscode live share doesn't behave well with the goal window

[Adam Topaz]

I think that's the "collarboration" issue...

[Gabriel Ebner]

Matthew Ballard said:

The open-source version of the Github version is https://github.com/cdr/code-server. Lean extension works perfectly.
https://github.com/cdr/code-server/blob/v3.6.2/doc/FAQ.md#how-is-this-different-from-vs-code-codespaces

This looks really interesting!

[Matthew Ballard]

@Adam Topaz asked me to test code-server re:collab. A 5 second test from two machines was encouraging. Everything is visible and updates propagated quickly enough.

[Matthew Ballard]

https://medium.com/@ow/its-finally-possible-to-code-web-apps-on-an-ipad-pro-90ad9c1fb59a I wanted to conference/travel focused laptop (ie tablet) but with moderate texing capabilities. I ended up at an iPad. So far it's fine. A little buggy but not annoyingly so.

[Johan Commelin]

Matthew Ballard said:

Adam Topaz asked me to test code-server re:collab. A 5 second test from two machines was encouraging. Everything is visible and updates propagated quickly enough.

Wow... more details please!

[Johan Commelin]

Can both machines type code, or is one of them read only?

[Matthew Ballard]

Both can type

[Kevin Lacker]

why would multiple people want to share a lean editor? instead of just working off the same branch. are you entering code into the same place at the same time?

[Adam Topaz]

Kevin Lacker said:

why would multiple people want to share a lean editor? instead of just working off the same branch. are you entering code into the same place at the same time?

pair programming, for example

[Matthew Ballard]

You are accessing through a browser if you expose it over the internet.

[Johan Commelin]

So both can also execute terminal commands, I guess? Which might be a security issue (depending on who/what/where/when...)

[Matthew Ballard]

Oh yeah. There is a password to reach the server but yeah the terminal is there.

[Johan Commelin]

So, was there anything you did to enable collab? Because a quick inet search seemed to say that code-server didn't have collab features

[Matthew Ballard]

No. I just navigated to the url from two different browsers and typed.

[Kevin Lacker]

has anyone tried https://www.codetogether.com/ ? i've heard some good things but not in the context of Lean

[Matthew Ballard]

Like I said it was a 5 second test so I didn't try anything other than entering a word or two and seeing how it propagated/looked.

[Adam Topaz]

Does code-share's install script automatically set up nginx and all that?

[Matthew Ballard]

No.

[Matthew Ballard]

I too-literally followed the steps here.

[Matthew Ballard]

https://github.com/cdr/code-server/blob/v3.6.2/doc/guide.md

[Matthew Ballard]

I used the caddy option.

[Matthew Ballard]

Some people just travel around it with on a raspberry pi. Apparently.

[Bhavik Mehta]

Johan Commelin said:

I haven't looked into this closely, but might this also finally solve the "collaboration" issue?

By the way there's a partial solution to this, by no means ideal but sometimes good enough: in VSCode with liveshare, if the collaborator (that is, non-host) disables lean checking, then any messages in the project are reported in the problems window, which is just about good enough for the collaborator to figure out the active goal state. You can't look at the goal state at cursor or anything like that, but using focus blocks you can see what's left on any unsolved goals

[Johan Commelin]

I couldn't even get the liveshare extension to work... it ought to work with a github account, but I couldn't get it working

[Johan Commelin]

I now have my own code-server running. Seems like it works quite well

[Johan Commelin]

I can confirm that "collab" mode seems to work.

[Matthew Ballard]

Johan Commelin said:

I can confirm that "collab" mode seems to work.

collab mode?

[Johan Commelin]

I guess I should run the server under a separate unix user, because otherwise you can browse my entire home directory

[Johan Commelin]

Same as what you did: just login twice

[Matthew Ballard]

Wondering if I missed something.

[Johan Commelin]

Everyone that's logged in sees the same version of a file, if they open the same file. But you aren't force to have the same files open. You can work on separate folders if you want.

[Johan Commelin]

In particular, I can't even notice if another user is hacking around in a terminal, or something like that.

[Matthew Ballard]

Good or bad?

[Johan Commelin]

I guess you can't really avoid it...

[Johan Commelin]

Well, CoCalc managed to, somehow

[Johan Commelin]

But anyway, under a fresh unix user, I don't think much damage can be done.

[Adam Topaz]

cocalc runs in a docker container (or something)

[Adam Topaz]

you can do the same on your server

[Matthew Ballard]

You can run this in a container also. I think.

[Kevin Lacker]

just dont keep your bitcoin wallet on the same machine you use for sharing lean sessions

[Adam Topaz]

I bet you can use firejail also

[Adam Topaz]

Or, if you're running bsd for some reason, bsd-jails

[Adam Topaz]

@Johan Commelin If you get a docker file set up for this, it would be GREAT if you could share it!

[Johan Commelin]

/me has never used docker before

[Adam Topaz]

/me hasn't either... that's why he wants help :)

[Reid Barton]

User home directories are usually world-readable by default on Linux

[Adam Topaz]

but not from a docker container, I don't think

[Johan Commelin]

Reid Barton said:

User home directories are usually world-readable by default on Linux

Hmm, good point. But at least my private keys aren't

[Matthew Ballard]

I use a virtual machine dedicated to this. If someone takes it over, eh.

[Matthew Ballard]

Though I think containers are definitely more fashionable.

[Jannis Limperg]

Worth noting that Docker runs as root by default (the rootless mode is 'experimental'), so you have to trust the Docker daemon to properly enforce the sandbox. A VM is probably harder to attack. Then again, your collaborator who gets a bit too nosey but isn't an NSA agent probably won't get out of either.