haskell-liquid checker problem in emacs plugin

[Tomas Diaz]

Hello, 

I was trying to use the emacs plugin as suggested in the tutorial (https://github.com/ucsd-progsys/liquid-types.el) but for some reason the haskell-liquid checker for flycheck cannot find z3 and prints this error message:

I am working on a Mac OS X Sierra, with GHC 7.10.3 and z3 version 4.5.

I installed LiquidHaskell using cabal, placed the binary for z3 in the same folder and I can run it in my terminal without any error regarding the SMT solver. I specified the location in the variable (as specified here https://github.com/themattchan/flycheck-liquidhs.el) but I keep getting the above mentioned message.

Should I specify the location for the SMT solver somewhere? (I am not very used to emacs... so I may have missed a step?)

Thank you!

Tomás

[Niki Vazou]

Hey Tomas, 

Is z3 visible in your path? That is what is the output of running 

```

which z3

```

in your terminal?

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Niki

[Tomas Diaz]

Yep, it is.

I get $HOME/Library/Haskell/bin which is the same I get if I do it with liquid.

To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Niki

[Ranjit Jhala]

Can you run liquid from the command prompt?

I think the liquid process started from emacs doesn't have access to your Home/library/Haskell/bin
Path; perhaps put the z3 binary somewhere more global?

[Tomas Diaz]

Yes, I can run liquid from the command prompt.

I tried putting it in /usr/local/bin and $HOME/.local/bin but it's still not finding it.