Isabelle : 다른 컴퓨터에서 sledgehammer를 실행 한 다음 Isabelle/jEdit가 실행되는 내 일반 PC

Question

랩탑에서 Isabelle/jEdit으로 작업하고 있습니다.

노트북에는 4 개의 코어 즉 4 개의 CPU가 있습니다. 그러나 나는 또한 다음 방에 서버 컴퓨터를 가지고있다. 서버에는 20 개 이상의 CPU가 있습니다.

일반적으로 시도 결과가 sledgehammer 자체가 실패한 슬레지 해머 결과를 제공하기 때문에 sledgehammer과 try을 병렬로 실행합니다 (my other question on this 참조).

그래서 나는 병렬로 실행할 수있는 프로세스가 꽤 있다고 생각합니다.

그러나 서버가 '헤드리스'이므로 Isabelle/jEdit를 사용하거나 사용할 수 없으므로 X 또는 창 관리자가 설치되어 있지 않습니다.

그래서 내 labtop에서 내 서버로 sledgehammer 호출을 보내고 거기에 sledgehammer를 실행하려면 Isabelle/jEdit 세션이 필요합니다. 내 자신의 종류와 같은 TPTP 시스템.

설정이 가능하고 쉽게 할 수 있습니까?

Answer 1

사용자 수준에서이를 달성하는 쉬운 방법은 없습니다.

1. 당신은 "SRC/HOL/도구/ATP/스크립트/remote_atp"를 수정할 수, 대신 슈퍼아요 서버를 사용, SystemOnTPTP 회담 스크립트 :하지만, 여기에 몇 가지 아이디어입니다.

2. 그러면 주요 문제는 병렬 처리입니다. jeadit에서 Sledgehammer 패널은 스레드 중 일부가 대부분 원격으로 실행 중이더라도 컴퓨터가 처리 할 수 ​​있다고 생각하는 것보다 더 많은 스레드를 동시에 실행할 수 없습니다. "Sledgehammer"명령을 사용하여 Sledgehammer를 수동으로 호출하면 제한 사항을 해결할 수 있지만 확실하지는 않습니다.

덧붙여서, 4 명 또는 5 명을 초과하는 실행자는 성공률에 매우 미미한 영향을 미칩니다.

Answer 2

본인은 본 적이 없지만 올바르게 이해하고 사용하도록 Isabelle을 구성한 경우 사용하려는 외부 보호 기능을 사용하는 서버에만 sledgehammer를 설치할 필요가 없습니다.