Isabelle: run sledgehammer on a different machine then my normal PC where Isabelle/jEdit runs

Question

I am working with Isabelle/jEdit on my labtop.

My laptop has 4 cores, i.e. 4 CPUs. But I also have a server computer in the next room. The server has more than 20 CPUs.

Usually I run sledgehammer and try in parallel, as sometimes the try results gives sledgehammer results where sledgehammer itself fails (see my other question on this).

So I guess there are quite a few processes that can run in parallel.

However, I cannot use or run Isabelle/jEdit on my server as the server is 'headless', thus there is no X or window manager installed.

So I would need my Isabelle/jEdit session to send the sledgehammer calls from my labtop to my server, execute sledgehammer there. Sort of my own TPTP like system.

Is this possible and easy to set up?

Answer 1

There's no easy way to achieve this from the user level. But here are a couple of ideas:

1. You could modify "src/HOL/Tools/ATP/scripts/remote_atp", the script that talks to SystemOnTPTP, to use your super-duper server instead.

2. The main issue then is parallelism. In jEdit, the Sledgehammer panel cannot run more threads simultaneously than it thinks your machine can handle, even though some of the threads are mostly running remotely. If you invoke Sledgehammer manually, using the "sledgehammer" command, you might be able to work around the restriction, but I'm not sure.

Incidentally, running more than 4 or 5 provers has a very modest effect on the success rate.

Answer 2

I never did this, but you need not install sledgehammer on your server only the external provers you want to use, if I understand correctly and then configure Isabelle to use them.