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



On 12/5/2013 7:59 AM, Makarius wrote:
300 threads are quite a lot, but I suggested to go towards and beyond the limits of what is feasible :-)

I have about 70 processes running normally, and with threads set to 300, only a maximum of about 140 processes are ever running for the "False = True" test. An ATP running as a thread sometimes starts up lots of processes of its own. With threads set to 4, a max of about 90 processes will be running on my computer.

I think I'll try threads set to 12 for a while, even though you've said it should be set to the number of physical cores. One of the new remote ATPs that came with Isablle2013-1 is "remote_agsyhol", which is finding proofs.

I've added that to my "first pass ATPs", so here are the 12 I use for a first pass. Setting threads to 12 lets all of the them start (or maybe it needs to be more than 12), and many of them will sometimes timeout fast:

  remote_vampire  metis  remote_satallax  z3_tptp  remote_e remote_agsyhol
  remote_e_tofof  spass  remote_e_sine    e        z3       yices

A general note on Multithreading.max_threads: changing that in Isabelle/ML might lead to some surprises, because the PIDE protocol will update its value after some change of properties, using the value that is given in Isabelle/Scala, which is the same that you see in Isabelle/jEdit in the dialog "Plugin Options / Isabelle / General / Threads".

ML {* Multithreading.max_threads_value () *} is fine to check what Isabelle/ML is presently using.

Before, I didn't see max_threads_value change after changing "Threads", but now I see that if I save the file, max_threads_value will display what I set "Threads" to in the options.

Does that mean you have a local installation of leo? I've never looked at it myself, and don't know where to get it. It might have once again its very own process management done in OCaml.

Yes. I have a local install. Your colleague must have forgot to mention it to you:

http://www.cl.cam.ac.uk/~lp15/Grants/leo2.html

You may be able to ask him about it in Houston. Texas is big, so they say. You wouldn't want to get lost. With your good English grammar, Texans might not be able to understand you.

http://www.nasaformalmethods.org/?page_id=104

I haven't had to do anything special to keep leo2 running since Isabelle2012, unlike satallax, which doesn't run anymore because I haven't downloaded what's needed for Cygwin.

For anyone interested, there are a number of ATPs which can be run locally, that aren't part of the distribution.

Vampire, http://www.vprover.org/ (The version is up to 3.0, but the downloads haven't been available for a long time, and local vampire won't run on Windows)

Leo2, http://www.ags.uni-sb.de/~leo/ (the link is not responding for me right now)

Satallax, http://www.ps.uni-saarland.de/~cebrown/satallax/

Yices, http://yices.csl.sri.com/download.shtml

Regards,
GB





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