On Sun, 29 Jun 2014, Cezary Kaliszyk wrote:
Hi Makarius,
On Thu, Jun 26, 2014 at 11:08 PM, Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
