Isabelle: запустить кувалду на другой машине, тогда мой обычный компьютер, где работает Isabelle/jEdit

Question

Я работаю с Isabelle/jEdit на моей лаборатории.

У моего ноутбука 4 ядра, то есть 4 процессора. Но у меня также есть серверный компьютер в соседней комнате. Сервер имеет более 20 процессоров.

Обычно я бег sledgehammer и try параллельно, а иногда и результаты Try дают результаты кувалды, где сама кувалда терпит неудачу (см my other question on this).

Итак, я думаю, что существует немало процессов, которые могут работать параллельно.

Однако я не могу использовать или запускать Isabelle/jEdit на моем сервере, так как сервер «безголовый», поэтому не установлен X или оконный менеджер.

Так что мне понадобится моя сессия Isabelle/jEdit, чтобы отправить вызовы кувалды с моего labatop на мой сервер, выполнить там кувалду. Сортировка моего собственного TPTP как система.

Возможно ли это и легко настроить?

Answer 1

Нет простого способа достичь этого с пользовательского уровня. Но вот несколько идей:

1. Вы можете изменить «SRC/HOL/Инструменты/АТП/скрипты/remote_atp», сценарий, который разговаривает с SystemOnTPTP, чтобы использовать супер-пупер-сервер вместо этого.

2. Основная проблема заключается в параллелизме. В jEdit панель Sledgehammer не может запускать больше потоков одновременно, чем думает, что ваша машина может работать, хотя некоторые из потоков в основном работают удаленно. Если вы вызываете Sledgehammer вручную, используя команду «кувалда», вы можете обойти это ограничение, но я не уверен.

Кстати, при запуске более 4 или 5 датчиков очень мало влияет на скорость успеха.

Answer 2

Я никогда не делал этого, но вам не нужно устанавливать кувалду на свой сервер только внешние прожекторы, которые вы хотите использовать, если я правильно понимаю, а затем настрою Изабель использовать их.