Re: [isabelle] z3 on a mac



Hello,
Thanks for all the help.  The Isabelle community is amazing. The
updates worked with two small tweaks.
  - The script on the webpage uses 'Wine Files/drive_c/Program
Files/Microsoft Research/Z3/bin/z3.exe'.  On my machine z3 installs
with the same path except Z3-2.19 instead of just Z3.
  - I still needed to edit contrib/z3/etc/settings and uncomment
Z3_NON_COMMERCIAL="yes" for it to work. I don't know if it is
intentionally left uncommented in your tar file. It took me some
digging to initially find that option last week; perhaps  an explicit
comment on the website would be helpful to others?

A couple of bizarre things happened when trying to get it to work
today. I note these in case someone else experiences them.
 - When I started up wine today it asked to self-update. I said yes.
/Applications/Wine.appContents/MacOS/startwine went away. Reinstalling
wine from the dpkg fixed. .
 - The [[smt_trace]] option is really cool. I didn't know about that widget.
 - z3 seems to be successfully invoked. The first time I ran it to prove:

lemma reallysimple : "(a \<and> b)= (b \<and> a)"
using [[smt_trace]]
sledgehammer [provers=z3,verbose=true,debug=true]

z3 didn't produce a solution. However, it has reliably since then.
I'm not sure why, but it's worked reliably since then. I'm chalking it
up to first time initialization tasks.


Take care,
-David


On Fri, Jul 1, 2011 at 9:40 AM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> Hi David,
>
> Am 30.06.2011 um 16:32 schrieb David Brumley:
>
>> Anyone run into this? I looked at the z3 documentation, but couldn't
>> find an error 109 on the list.
>
> I was able to get an error 109 on the Mac as well, even after following Sascha's online instructions. To investigate this, try adding
>
>    declare [[smt_trace]]
>
> at the beginning of the .thy file, and send us the trace output.
>
> SMT: Solver:
>  /Users/blanchet/isabelle/contrib/z3-2.15/x86-darwin/z3: line 11: winepath: command not found
>  fixme:heap:HeapSetInformation 0x0 1 0x0 0
>  Error: input file was not specified.
>  For usage information: z3 /h
>
> If this is also your problem (and it probably is), either (1) make sure "/Applications/Wine.app/Contents/Resources/bin" is in your "PATH" before you launch Proof General or jEdit, or (2) update your "z3" script with the very latest version from Sascha's web page:
>
>    http://www4.in.tum.de/~boehmes/z3/mac/z3
>
> I hope this helps. Please let us know if it doesn't, so we can iron out these issues once and for all.
>
> Cheers,
>
> Jasmin
>
>





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