Re: [isabelle] Isabelle2013-2-RC3 ATP e_par acid test



On 12/4/2013 8:38 PM, Gottfried Barrow wrote:
4) I delete the "r" in "Sledgehammer".
5) The processes keep running much long than what I'm willing to wait. (I have waited up to 15 minutes to see if they would terminate, and they didn't.)

I don't actually have to terminate the Sledgehammer command. This worked three times in a row:

1) Log out and back into my Windows account.
2) Run the command I showed with max_threads set to 4.
3) It gets to where "leo" and 12 "eprover.exe" processes are running, and they don't timeout like they should.

I think it's related to the number of threads, but not completely. I can change max_threads to 3, and e_par times out like it should. I change it back to 4, and it can time out like it should.

I did the log out/log in sequence with max_threads set to 3, and it did like with 4, except "leo" wasn't running, but it didn't do it twice in a row. The number 4 seems worse, but 3 fails, and every computer might be different.

Regards,
GB




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.