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



> 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).

Jasmin





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