Re: [isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress



On 22.08.2014 12:32, Jasmin Christian Blanchette wrote:
>> As far as I understand sledgehammer it should use normal future forks (via Par_List.map) and thus participate in the global worker thread pool.
> With the Sledgehammer panel, all threads should participate in the global worker thread pool, with the potential exception of a single MaSh learning thread (occasionally -- e.g. the first time you launch Sledgehammer and MaSh has no accumulated state) -- the MaSh threads are managed using the old "asynchronous manager" mechanism, that is also used when invoking the "sledgehammer" command from the proof text.
>
> It would be useful to know if the problem also occurs when (1) MaSh is not run and (2) no proofs are found (and hence no proof minimization etc. and hence no "Par_List" operations, IIRC). Adding
>
>     sledgehammer_params [mepo]
>
> at the top of your theory should take care of (1).
When I add "sledgehammer_params [mepo]" before the place where I call
sledgehammer, the problem persists. Also, all provers timed out, so the
problem occurs also with (2).




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