Proof checking on remote server · General

Stream: General

Topic: Proof checking on remote server

Hanno Becker (Aug 02 2023 at 04:12):

Hi! I am working with a very large code base which gets increasingly slow to continually process on my local machine. I'd therefore like to know if/how it is possible to connect the Isabelle/jEdit IDE to a remote Isabelle server for continuous proof checking.

I saw the documentation on the Isabelle client/server model, but didn't find anything about whether/how this works for continuous proof-checking during interactive proofs.

Mathias Fleury (Aug 02 2023 at 04:41):

With Isabelle/jEdit you can execute things on the remote server with ssh -AYC. I have done it before, but ssh forwarding can be slow (and it is even worse with jEdit)

Mathias Fleury (Aug 02 2023 at 04:48):

Alternatives:

- I think that you can do it with Isabelle/VSCode by mounting the files on the server (see here), but I have never tried it
- I often do this with Isabelle/emacs via tramp (this is my side project, so your mileage may vary whether you want this or not).
- SSH forwarding to open emacs also works and is much less painful than jedit (it even works in the terminal). You can also keep emacs running overnight to avoid restarting it in the morning.

Mathias Fleury (Aug 02 2023 at 04:53):

The client / server is more of a protocol to be able to do it, than a solution to your problem

Mathias Fleury (Aug 02 2023 at 06:09):

(but to add: I have seen very weird things happening with Isabelle (before 2019, so maybe changed know) on a server with lots of RAM: in particular PolyML seems to give up on GCing)

Hanno Becker (Aug 03 2023 at 05:19):

Thanks @Mathias Fleury. I want to keep running jEdit locally, but offload continuous checking to an external server. (How) Can I do that? It does seem like a fairly natural thing to do, and I was hoping Isabelle's cli/srv model would make it possible.