Re: [isabelle] provers used by sledgehammer



It is customary to continue maintaining a tool until the replacement is ready
for prime time. Currently jedit is not at the point (and PG still works). I
expect that PG will be kept in a working state until key jedit problems like
"Workaround: Cut/paste larger parts or reload buffer" and the absence of menus
(which force people to remember and type commands) have been eliminated.

Tobias

Am 20/07/2012 13:18, schrieb Makarius:
> On Fri, 20 Jul 2012, Jasmin Blanchette wrote:
> 
>> If you change it through the good old Proof General settings, I think it will
>> do the right thing and remember it across sessions. Otherwise, no: That's what
>> "sledgehammer_params" is for, and it would be tedious to emulate its
>> functionality in "etc/settings" (e.g. to change the default timeout or
>> whatever else...).
> 
> Note again that Isabelle Proof General is umaintained since October 2011, so it
> has reached End-of-Life unless someone else stands forward to continue its
> maintenance.  (Pretty soon I will stop reminding people of this, and then it is
> really dead.)
> 
> 
> Concerning the current Isabelle/Scala and Prover IDE infrastructure, there is
> still no persistent preferences mechanisms, but I am working on it.
> 
> Righ now one can imitate what Proof General did here by hand:
> 
>   ML {* Sledgehammer_Isar.provers := "e spass vampire" *}
> 
> 
>     Makarius





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