Load SAT libs from dir relative to exe using linker flags

[bpfoley]

This allows us to remove the LD_LIBRARY_PATH code from the
wrapper scripts (step 1 of removing the scripts altogether).

On macOS, this requires us to prefix @rpath/ to libraries'
install_names.

Then on macOS and Linux respectively, we can link with
-rpath @executable_path/../../lib/SAT and $ORIGIN/../../lib/SAT
respectively.

While here, fix up the file naming for the stub libyices on macOS:
It was using the Linux shared library names.

[bpfoley]

For some context, these are the linker mechanisms used on macOS and Linux:

https://www.mikeash.com/pyblog/friday-qa-2009-11-06-linking-and-install-names.html
https://blogs.oracle.com/dipol/dynamic-libraries,-rpath,-and-mac-os

This addresses #10.

[quark17]

Prior to this change, the only place that needs to know the relative path of the wrapper/binary to the BLUESPECDIR is the wrapper script. This change now requires an additional file (src/comp/Makefile) to also be kept in sync with any changes in the directory structure. I'm willing to accept that, but another possibility is: we don't link with the SAT libraries at all when building, but instead have BSC use dlopen. (This also has the advantage that stub libraries are no longer needed, when you don't want to build/ship STP/Yices, because BSC could handle the case when dlopen fails to find the library -- rather than assume it's always being linked and test whether the linked library was a stub.)

FYI, I note that Yices is also installing a static archive (libyices.a) that gets into the release's SAT directory. Can we avoid building/installing that?

[bpfoley]

Prior to this change, the only place that needs to know the relative path of the wrapper/binary to the BLUESPECDIR is the wrapper script. This change now requires an additional file (src/comp/Makefile) to also be kept in sync with any changes in the directory structure.

Not an additional file, just a different one. The wrapper script no longer knows about lib/SAT.

I'm willing to accept that, but another possibility is: we don't link with the SAT libraries at all when building, but instead have BSC use dlopen. (This also has the advantage that stub libraries are no longer needed, when you don't want to build/ship STP/Yices, because BSC could handle the case when dlopen fails to find the library -- rather than assume it's always being linked and test whether the linked library was a stub.)

Cool. If we only use a small number of functions from the shared libraries, that's probably viable. But that doesn't really remove the need for something to know about the relative paths, does it? Now we've just moved it from the Makefile into some bit of Haskell code.

FYI, I note that Yices is also installing a static archive (libyices.a) that gets into the release's SAT directory. Can we avoid building/installing that?

Yes. I've a separate patch in progress to clean that up, but I was waiting for the existing yices change to land first because they conflict.

[quark17]

I think you misunderstand what I'm talking about.

Yes, there is directory structure under BLUESPECDIR which various places need to know about, to find their files. For example, the knowledge that the SAT libraries can be found in ${BLUESPECDIR}/SAT/. That's not what I'm talking about.

Separate from that is how BLUESPECDIR is computed in the first place. Right now, only the wrapper script computes BLUESPECDIR, relative to the location of the wrapper (../lib/). With your commit, the wrapper is still computing BLUESPECDIR, but also the Makefile is computing BLUESPECDIR as well, relative to the location of the binary (../../lib/). That's the issue that I'm talking about.

I'd prefer if we could limit the computation of BLUESPECDIR to one place. Right now, that's in the wrapper, but it could eventually be done in the bsc/bluetcl executables. In either case, once BLUESPECDIR is known, then the SAT libraries can loaded with dlopen without having to recompute BLUESPECDIR (but, yes, knowing that the libraries are in a SAT dir relative to the given BLUESPECDIR).

If we only use a small number of functions from the shared libraries

I don't think the number of functions matters. We're already importing every individual function with FFI.

[bpfoley]

I think you misunderstand what I'm talking about.
[...]

I'd prefer if we could limit the computation of BLUESPECDIR to one place. Right now, that's in the wrapper, but it could eventually be done in the bsc/bluetcl executables. In either case, once BLUESPECDIR is known, then the SAT libraries can loaded with dlopen without having to recompute BLUESPECDIR (but, yes, knowing that the libraries are in a SAT dir relative to the given BLUESPECDIR).

Ah, I see, you're right, I missed that point.

And now that I think it through, if FFI has to do all the magic of wrapping up function pointers returned by dlsym() anyway, using dlopen() instead of ld.so probably makes almost no difference to any of the rest of the Haskell code. Yes, that's definitely the better approach. :)