avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
authorblanchet
Sat Dec 15 21:26:10 2012 +0100 (2012-12-15)
changeset 50558a719106124d8
parent 50557 31313171deb5
child 50559 89c0d2f13cca
avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Dec 15 19:57:12 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Dec 15 21:26:10 2012 +0100
     1.3 @@ -746,7 +746,8 @@
     1.4                  |> seconds |> SOME
     1.5                | NONE => NONE
     1.6              val generous_slice_timeout =
     1.7 -              Option.map (curry Time.+ atp_timeout_slack) slice_timeout
     1.8 +              if mode = MaSh then NONE
     1.9 +              else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
    1.10              val _ =
    1.11                if debug then
    1.12                  quote name ^ " slice #" ^ string_of_int (slice + 1) ^