## Stream: general

### Topic: lean and codespaces

#### Johan Commelin (Nov 05 2020 at 17:39):

Seems interesting!

#### Eric Wieser (Nov 05 2020 at 17:40):

Github has a very similar codespaces feature

#### Eric Wieser (Nov 05 2020 at 17:41):

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 (Nov 05 2020 at 17:46):

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 (Nov 05 2020 at 18:30):

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

#### Eric Wieser (Nov 05 2020 at 18:32):

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 (Nov 05 2020 at 18:42):

Johan Commelin said:

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

#### Gabriel Ebner (Nov 05 2020 at 18:59):

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 (Nov 05 2020 at 19:02):

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 (Nov 05 2020 at 19:02):

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

#### Kevin Lacker (Nov 05 2020 at 19:03):

what is the "collaboration" issue?

#### Adam Topaz (Nov 05 2020 at 19:03):

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

#### Adam Topaz (Nov 05 2020 at 19:03):

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

#### Gabriel Ebner (Nov 05 2020 at 19:04):

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 (Nov 05 2020 at 19:05):

@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 (Nov 05 2020 at 19:07):

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 (Nov 05 2020 at 19:08):

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.

#### Johan Commelin (Nov 05 2020 at 19:08):

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

Both can type

#### Kevin Lacker (Nov 05 2020 at 19:08):

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 (Nov 05 2020 at 19:08):

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 (Nov 05 2020 at 19:08):

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

#### Johan Commelin (Nov 05 2020 at 19:09):

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

#### Matthew Ballard (Nov 05 2020 at 19:10):

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

#### Johan Commelin (Nov 05 2020 at 19:11):

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 (Nov 05 2020 at 19:11):

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

#### Kevin Lacker (Nov 05 2020 at 19:12):

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

#### Matthew Ballard (Nov 05 2020 at 19:12):

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 (Nov 05 2020 at 19:14):

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

No.

#### Matthew Ballard (Nov 05 2020 at 19:14):

I too-literally followed the steps here.

#### Matthew Ballard (Nov 05 2020 at 19:14):

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

#### Matthew Ballard (Nov 05 2020 at 19:16):

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

#### Bhavik Mehta (Nov 05 2020 at 20:54):

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 (Nov 05 2020 at 20:56):

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 (Nov 05 2020 at 20:56):

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

#### Johan Commelin (Nov 05 2020 at 21:04):

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

#### Matthew Ballard (Nov 05 2020 at 21:05):

Johan Commelin said:

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

collab mode?

#### Johan Commelin (Nov 05 2020 at 21:05):

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

#### Johan Commelin (Nov 05 2020 at 21:05):

Same as what you did: just login twice

#### Matthew Ballard (Nov 05 2020 at 21:06):

Wondering if I missed something.

#### Johan Commelin (Nov 05 2020 at 21:06):

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 (Nov 05 2020 at 21:06):

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

#### Johan Commelin (Nov 05 2020 at 21:08):

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

#### Johan Commelin (Nov 05 2020 at 21:09):

Well, CoCalc managed to, somehow

#### Johan Commelin (Nov 05 2020 at 21:09):

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

#### Adam Topaz (Nov 05 2020 at 21:09):

cocalc runs in a docker container (or something)

#### Adam Topaz (Nov 05 2020 at 21:09):

you can do the same on your server

#### Matthew Ballard (Nov 05 2020 at 21:09):

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

#### Kevin Lacker (Nov 05 2020 at 21:10):

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

#### Adam Topaz (Nov 05 2020 at 21:10):

I bet you can use firejail also

#### Adam Topaz (Nov 05 2020 at 21:11):

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

#### Adam Topaz (Nov 05 2020 at 21:16):

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

#### Johan Commelin (Nov 05 2020 at 21:19):

/me has never used docker before

#### Adam Topaz (Nov 05 2020 at 21:20):

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

#### Reid Barton (Nov 05 2020 at 21:22):

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

#### Adam Topaz (Nov 05 2020 at 21:23):

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

#### Johan Commelin (Nov 05 2020 at 21:23):

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 (Nov 05 2020 at 21:24):

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

#### Matthew Ballard (Nov 05 2020 at 21:24):

Though I think containers are definitely more fashionable.

#### Jannis Limperg (Nov 06 2020 at 12:33):

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.

Last updated: May 13 2021 at 18:26 UTC