Stream: General

Topic: Proof checking on remote server


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Aug 03 2023 at 05:20):

Yes it is possible, but there is work to do which was not done by anybody so far

view this post on Zulip Hanno Becker (Aug 03 2023 at 05:21):

Hmm, that's a shame.

view this post on Zulip Hanno Becker (Aug 03 2023 at 05:25):

I'll ping the mailing list for some more perspectives and increased awareness :-)

view this post on Zulip Hanno Becker (Aug 03 2023 at 05:28):

Does jEdit itself support a cli/srv model, so one could run the graphic frontend locally, but the 'backend' (and, with it, Isabelle) remotely?

view this post on Zulip Mathias Fleury (Aug 03 2023 at 05:29):

Hanno Becker said:

I'll ping the mailing list for some more perspectives and increased awareness :-)

oh dear, I remember Makarius rants on that (but cannot find them)

view this post on Zulip Hanno Becker (Aug 03 2023 at 05:29):

... What's there to rant about?

view this post on Zulip Mathias Fleury (Aug 03 2023 at 05:31):

I found this message which was just ignored: https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Working.20remotely/near/325180372

view this post on Zulip Mathias Fleury (Aug 03 2023 at 05:32):

Hanno Becker said:

... What's there to rant about?

you are doing it wrong, you have a computer that is too slow, …

view this post on Zulip Hanno Becker (Aug 03 2023 at 05:33):

...

Thanks for digging up the message. I'll ping the ML anyway.

view this post on Zulip Hanno Becker (Aug 03 2023 at 05:38):

Done -- bracing myself now :-) Anyway, thanks for your thoughts as always!

view this post on Zulip Mathias Fleury (Aug 03 2023 at 05:51):

Hanno Becker said:

Done -- bracing myself now :-) Anyway, thanks for your thoughts as always!

For the sake of documentation:
https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Isabelle.2FjEdit.3A.20Remote.20continuous.20proof.20checking/near/381361328


Last updated: Oct 13 2024 at 01:36 UTC