best option for live collaboration?

Stream: Lean for teaching

[Malvin Gattinger]

Is there a current best practice or recommendation for live collaboration with Lean in VS Code?

Last week we tried out three different ways, see below for my quick comparison notes.

The main problem we ran into: No method makes the Lean Infoview available to the guest. As mentioned in other threads here, the "Problems" list is visible to the other person, but it is not as nice as the InfoView.
I think in an ideal collaboration setting it would be good to have InfoViews for each cursor? If that is not possible, then it would be nice to have something like one person at a time "driving" as in CodeTogether, and that cursor determining the InfoView.
I guess corresponding to this is the question whether (as all those tools seem to do) there is only one instance of Lean running on the host or (maybe better?) each participant is running their own Lean instance locally.

In both LiveShare and CodeTogether the InfoView is not shared. Instead, in the guest VS code it fails with "Lean 4 server operating in restricted single file mode. Please open a valid Lean 4 project containing a 'lean-toolchain' file for full functionality."
(This happens when the Lean 4 extension is installed. If not, as in the browser clients, then nothing happens and there is not even syntax highlighting.)

Mircosoft LiveShare

• NICE: easy to join, even in browser
• BAD: no syntax highlighting in BRwoser
• BAD: needs account
• BAD: Not FLOSS, not available in VS Codium by default.
• BAD: No InfoView, see error above.

CodeTogether

• NICE: easy to join, no account needed
• NICE: multiple cursors + "driving" mode
• NICE: audio integration? (not tried)
• BAD: No syntax highlighting when in browser or when not trusted
• BAD: No InfoView, see error above.

Gitpod (sharing the link, ugly)

• BAD: needs (github) account and asks first-time guests job/project questions
• BAD: other cursors not visible, overwriting each others changes
• BAD: gives other person full git rights in your name

other silly ideas :crazy:

• in parallel to LiveShare or CodeTogether, screen-share the InfoView via another tool.
• get something/someone like replit.com to support Lean?
• hack together a combination of https://live.lean-lang.org/ and etherpad

[Kevin Buzzard]

For Lean 3 I thought that CoCalc had a really good attempt. The problem was that they were not able to keep up with the fast paced nature of Lean releases.

[Utensil Song]

CodeTogether seems nice, why can't it show Lean InfoView exactly?

[Malvin Gattinger]

I updated the notes above a bit after trying both again. The error is "Lean 4 server operating in restricted single file mode. Please open a valid Lean 4 project containing a 'lean-toolchain" and I guess it happens when the client starts its own Lean server but does not have a folder with all the files.