Remote Collaborative Editing of Coq Files

Problem

2 or more people in different parts of the world want to collaboratively edit Coq file(s) in an IDE like setting (syntax highlighting, coqtop queries, jump to definition etc. should work). Below are different ways to achieve this.

emacs+company-coq console mode over a tmux shared terminal over SSH

Among the participants, one person should decide to be the host, and others will be guests. All the guests needs is an SSH client (X support not needed). Requirements for the host:

1. The host should be a participant whose computer has the Coq files and can open them in emacs+company-coq IDE.
2. All guests should be able to SSH into the computer of the host (possibly as a "guest" user with minimal privileges and no access to the Coq files).
3. The host computer should have tmux installed. Should be available in your distro's package manager.

Initial Setup Steps:

1. Arrange for guests to SSH into hosts. This is simple if the guests and hosts are in the same local area network or VPN. Usually, this is not the case. Perhaps the simplest approach in such cases is to choose as host a participant that has a public IP. Most wired internet service providers (ISPs) provide public IPs by default. The public IP must either be static (rare for non-business ISP accounts) or be bound some static public hostname (say phname) using a dynamic DNS service. There are many free dynamic DNS services like duckdns.org. Below, phname will be used for ssh connections, but you can use a static public IP instead. The public IP is typically assigned to the router WAN interface. Some port, say wanport, on the router's public IP interface needs to be forwarded to the host computer's port 22 (or whatever port the SSH server is running on the host's computer). Obviously, the host needs to install an SSH server. Each guest needs to add the following to their ~/.ssh/config:

Host coqedithost
       HostName [phname]
       Port [wanport]
       User guest
       IdentityFile [/path/to/private/key]

/path/to/private/key is the private key the guest uses for ssh logins.

At this point, each guest can do the following in a terminal and get "permission denied (public key)":

ssh coqedithost

2. Create a guest user account in host's computer To prevent guests from inadvertently messing up the host's computer, it is recommended that the guests login with a "guest" account with almost no privileges, not even access to the Coq files being edited. The host needs to do the following:

sudo useradd -m guest
sudo passwd guest

Each guest needs to send the host their public key (corresponding to the /path/to/private/key) chosen in the previous step. The host needs to add them to /home/guest/.ssh/authorized_keys At this point, each guest can do the following in a terminal and get succeed in logging in as the guest user on the host's computer:

ssh coqedithost

3. Set up scripts. The host should create a script, say tmuxStartHostServer.sh in the home directory of their account, say /home/host/, not /home/guest:

tmux -S /tmp/socket new -d
tmux -S /tmp/socket send-keys "chmod 777 /tmp/socket" Enter
tmux  -S /tmp/socket attach

The host should su guest and create the following script /home/guest/joinTmux.sh

tmux -S /tmp/socket attach

Usage

The host logs into their account and executes ~/tmuxStartHostServer.sh. The guests then do:

ssh coqedithost
./joinTmux.sh

At this point, the host and the guest have a shared terminal that they can both control. The size of the terminal is the minimum size of all participants. So all participants should maximize/enlarge their terminal window (e.g. gnome-terminal/Konsole etc). To collaboratively edit files, you can use any console-mode editor, e.g. emacs -nw or vim. If you have company-coq and proof general installed, you can use emacs to collaborately edit Coq files. To exit the session, the host need to enter the command exit at the terminal prompt. Until the exit, the guests can execute any command in the hosts terminal as the host's user account, although this will be noticed by everyone paying attention to the shared session. The host may not want to leave the session unattended. Guests should not use exit to leave the session as this will kill the tmux session for everyone. Guests should use Ctrl+B d (release Ctrl before pressing d) to leave the session.

optional emacs/proof-general/company-coq customizations for console mode

All features supported in windowed mode are also supported in console mode. In console mode, the coq-checked part is underlined, which may be somewhat inconvenient as it hides _:

You can change the text attributes of the coq-checked part by customizing proof-general. For example, the following lines in /home/host/.emacs remove underlining and make the coq-checked part red (as background color):

(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(default ((t (:family "Bitstream Vera Sans Mono" :foundry "Bits" :slant normal :weight normal :height 173 :width normal))))
 '(proof-locked-face ((t (:background "#ff0000")))))

Be careful with colors though: the colors that guests sees may be different based on the theme they have color chosen for their terminal program (e.g. Konsole/gnome-terminal) in which they are running their SSH client.

By default, hosts and guests can only use keyboard to navigate in Coq file in emacs console mode. To enable navigation by mouse clicks (or touches on touchscreens/phones) for both hosts and guests, the host can add the following to /home/host/.emacs:

(xterm-mouse-mode)

After this change the old behavior of right-click is mapped to shift+right-click.

Pros/Cons:

Pros

1. works well over low-bandwith connections
2. clients don't need to install any software: just ssh client is needed
3. no third party gets to track the session

Cons/Limitations

1. emacs console mode is slightly harder to use than windowed mode.
2. Instead of emacs, some Coq users may want to use vscode or other editors that don't support console mode. This method only supports editors that support console mode.
3. host cannot dynamically control who gets non-read-only access to the terminal