Re: [isabelle] z3 on a mac
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)"
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.
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:
> I hope this helps. Please let us know if it doesn't, so we can iron out these issues once and for all.
This archive was generated by a fusion of
Pipermail (Mailman edition) and