Re: [isabelle] sledgehammer in RC4



On Sun, 10 Nov 2013, Jasmin Blanchette wrote:

Earlier versions of Sledgehammer ran at most 2 local ATPs (for a 2-CPU system) + a number of remote ATPs in that case, since remote ATPs do not put a heavy load on the local machine.

It would be possible to have different defaults for Proof General and jEdit, but Sledgehammer already has too many modes, so I'd rather not go that way.

The situation is indeed at a point where it is unclear to me what really happens internally. The Proof General legacy is a heavy burden, sucks up maintenance resources, and reduces possibilities to get it right by clear and simple means.

We have already > 2 years of official stable releases of Isabelle/jEdit (Isabelle2011-1, Isabelle2012, Isabelle2013, Isabelle2013-1). These are in fact 4 generations of Prover IDE implementations: the steps between each of them are quite substantial.

People who are still using Proof General should say more explicitly what are the reasons for it, apart from old habits.


	Makarius




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