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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and