User error on running saw with no parameters

[daniel-vainsencher]

Just running saw (or, also, running saw ff_llvm.saw) causes:

---

/ *|/ _' | | | |
* \ (| | | | |
|/,|,_/ version 0.2 (012a784)

Loading module Cryptol
saw: z3: runInteractiveProcess: runInteractiveProcess: exec: does not exist (No such file or directory)

I installed from [1]. z3 isn't supposed to be an implicit dependency, right?

[1] https://github.com/GaloisInc/saw-script/releases/download/v0.2/saw-0.2-2016-04-12-Ubuntu14.04-64.tar.gz

[atomb]

Z3 actually is a strict dependency (because it's used in the type checker for Cryptol, which is a core component of SAW). I'm going to treat this ticket as a reminder to update the text on saw.galois.com to mention that.

It would also be good to improve that error message.

In principle, it might be possible to make some uses of SAW work without Z3. Much of the functionality wouldn't be available, but some features could be.

[daniel-vainsencher]

Thanks, I would expect to see this mentioned in Downloads, and possibly
also in the tutorial. Speaking of which, having found the tutorial on the
web, it is not obvious that the code directory is under doc, might be worth
removing that paper cut.

On Fri, Apr 15, 2016 at 11:39 AM, Aaron Tomb [email protected]
wrote:

Z3 actually is a strict dependency (because it's used in the type checker
for Cryptol, which is a core component of SAW). I'm going to treat this
ticket as a reminder to update the text on saw.galois.com to mention that.

It would also be good to improve that error message.

In principle, it might be possible to make some uses of SAW work without
Z3. Much of the functionality wouldn't be available, but some features
could be.

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub
#128 (comment)

[tiziano88]

I was also confused by this and could not get things up and running out of the box. Would be good to mention this dependency somewhere.

[atomb]

With the latest updates to saw.galois.com and the README in this repo, I think this issue is resolved.