[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Mon Jun 30 13:36:39 CEST 2014
On Sun, 29 Jun 2014, Cezary Kaliszyk wrote:
> Hi Makarius,
> On Thu, Jun 26, 2014 at 11:08 PM, Makarius <makarius at sketis.net> wrote:
>> At the moment (06599233e54e) there are no remaining uses of Proof General to
>> the best of my knowledge. If anybody has counter-examples they should be
>> put on the table for discussion.
> I am using Isabelle via ProofGeneral on a server without X.
> I do not know of a way to run JEdit without X.
> Some of my uses of Isabelle need as much as 100GB memory (and I also
> make use of the parallelization to much more CPUs than my laptop has),
> so I need to work sshed to the server.
There is no way to run jEdit without graphical display: it is a GUI
I remember myself using Proof General Emacs in TTY mode 10-15 years ago,
but stopped that eventually, because it did not display all relevant
information. So I count this mode of working as mere nostalgy.
The actual requirement here is to use a local display with a remote server
machine for the heavy work of the prover. Proof General used to have a
rsh connection for that, but I wonder if it still works in current
Today one would probably make an ssh connection between a local
Isabelle/jEdit front-end and a remote prover process back-end, within
Isabelle/Scala. That is somehow possible, but I avoided spending time on
it so far for lack of practical relevance: hardly anybody ever pointed out
this known omission in the last 5 years. Thus it got close to the bottom
on the TODO list.
Another approach is to use a remote display protocol, and run the full
Prover IDE remotely. This does not quite work for X11, though, since that
protocol is hardly usable for remote displays today, and Java/AWT/Swing
applications are particularly bad.
Since I know 1-2 other people with the same problem, one could spend some
time to work out a solution: a contemporary way to have a remote display
connection that works with a remote Prover IDE.
The main areas to look are RDP or VNC, not X11.
More information about the isabelle-dev