Re: [isabelle] Sledgehammer - Cannot connect to server



Makarius wrote:

> What often helps in such situations are masses of users telling the author of such a tool to release it under a proper open-source license.
> 
> Even the MS empire has eventually done that, and released Z3 in a manner that it could be included in Isabelle2015 for everyone to use freely.

Indeed, I have brought this up on a number of occasions, including at my invited Vampire 2014 talk (pp. 3-4):

    http://www.loria.fr/~jablanch/life.pdf

Andrei and Laura told me they will happily provide binaries to anybody if they ask by email.

Since we now have a good collection of local provers (CVC4, E, SPASS, Z3), we do not need to rely on external provers by default, at least on 4-core machines. I have made a change to that effect in the repository (a9b71c82647b).

Jasmin





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