external dependency at runtime

[patrickaldis]

I have a project that is using the SBV solver library. This requires one of:

• z3
• mathsat
• cvc5

Or a few other SMT solvers.

I'm struggling to add z3 as a dependency to the project. As instructed here, I've tried adding z3 to the extra-libraries section of the cabal file.

This adds z3 to the development shell, however running the result of the nix build from another shell complains that z3 is not on the path. How can I add the executable at runtime?

Thanks for any help

[michaelpj]

I can't clearly tell from the documentation how SBV depends on its solver, but it seems that it does not use it as a library, but rather as an executable, and the user just has to provide it at runtime somehow.

This is somewhere where we can't rely on cabal, since cabal has no way of saying "this executable must be present at runtime". So you'll need to manually add z3 wherever you use it. I'm not sure what the cleanest way to do that is, though.

[patrickaldis]

Ah sure, thanks for the help. That's correct, it only requires it as an executable.

I'm struggling to add it in any respect honesly. I'm still getting used to flakes and I'd consider myself a bit of a nix novice. Any method of doing this would be great

[angerman]

I believe you also asked this on Reddit?

[stale]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Thank you for your contributions.

[quantum9Innovation]

I am also encountering this issue trying to install liquidhaskell, which requires z3 to build. I know what needs to be done (provide z3 in the build environment for the package), but have absolutely no idea how to do this with haskell.nix. Would greatly appreciate any insight into solving this!