[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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 
application.

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 
versions.

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.


 	Makarius