Zulip Chat Archive

Stream: general

Topic: lean and codespaces


view this post on Zulip Johan Commelin (Nov 05 2020 at 17:39):

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

view this post on Zulip Eric Wieser (Nov 05 2020 at 17:40):

Github has a very similar codespaces feature

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 18:30):

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

view this post on Zulip 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

view this post on Zulip 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?

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 19:02):

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

view this post on Zulip Kevin Lacker (Nov 05 2020 at 19:03):

what is the "collaboration" issue?

view this post on Zulip Adam Topaz (Nov 05 2020 at 19:03):

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

view this post on Zulip Adam Topaz (Nov 05 2020 at 19:03):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

Wow... more details please!

view this post on Zulip Johan Commelin (Nov 05 2020 at 19:08):

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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:08):

Both can type

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:08):

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

view this post on Zulip 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...)

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:10):

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

view this post on Zulip 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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:11):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 05 2020 at 19:14):

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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:14):

No.

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:14):

I too-literally followed the steps here.

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:14):

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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:15):

I used the caddy option.

view this post on Zulip Matthew Ballard (Nov 05 2020 at 19:16):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 20:56):

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

view this post on Zulip Johan Commelin (Nov 05 2020 at 21:04):

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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 21:05):

Johan Commelin said:

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

collab mode?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 21:05):

Same as what you did: just login twice

view this post on Zulip Matthew Ballard (Nov 05 2020 at 21:06):

Wondering if I missed something.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthew Ballard (Nov 05 2020 at 21:07):

Good or bad?

view this post on Zulip Johan Commelin (Nov 05 2020 at 21:08):

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

view this post on Zulip Johan Commelin (Nov 05 2020 at 21:09):

Well, CoCalc managed to, somehow

view this post on Zulip Johan Commelin (Nov 05 2020 at 21:09):

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

view this post on Zulip Adam Topaz (Nov 05 2020 at 21:09):

cocalc runs in a docker container (or something)

view this post on Zulip Adam Topaz (Nov 05 2020 at 21:09):

you can do the same on your server

view this post on Zulip Matthew Ballard (Nov 05 2020 at 21:09):

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

view this post on Zulip Kevin Lacker (Nov 05 2020 at 21:10):

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

view this post on Zulip Adam Topaz (Nov 05 2020 at 21:10):

I bet you can use firejail also

view this post on Zulip Adam Topaz (Nov 05 2020 at 21:11):

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

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Nov 05 2020 at 21:19):

/me has never used docker before

view this post on Zulip Adam Topaz (Nov 05 2020 at 21:20):

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

view this post on Zulip Reid Barton (Nov 05 2020 at 21:22):

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

view this post on Zulip Adam Topaz (Nov 05 2020 at 21:23):

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

view this post on Zulip 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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 21:24):

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

view this post on Zulip Matthew Ballard (Nov 05 2020 at 21:24):

Though I think containers are definitely more fashionable.

view this post on Zulip 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