Add Homebrew installation instructions

[carlocab]

stp is now in Homebrew/core: Homebrew/homebrew-core#75877

Not sure if this is something you'd like to advertise in your README, but opening this just in case it is.

[aytey]

Thanks, @carlocab for getting this into Homebrew! I guess it would be worth making it clear that this is "quick install" for macOS (we can't trust users won't try silly stuff).

W.r.t. Homebrew/homebrew-core#75877: this is built with Python but doesn't have any Python tests; should we add some?

[carlocab]

In theory it should be a quick install for Linux too, as Homebrew runs on Linux as well. However, that'll only work when stp has made its way to Linuxbrew, which should happen in the next day or so. I've double-checked that it builds and tests fine in a Docker container.

It won't get bottled (packaged as a pre-built binary) right away, but if you or one of your users opens an issue at Linuxbrew to request a bottle the Linuxbrew maintainers usually get one set up relatively quickly. (Or I can try to nudge one of the maintainers myself, but I think it'll be more convincing coming from someone who actually plans to use it on Linux.)

Re the Python module: I didn't actually check that the works... I only set it up since cryptominisat already had a Python dependency, so it seemed there was very little lost in setting it up to build the Python module too. We can add a test if you like.

[aytey]

However, that'll only work when stp has made its way to Linuxbrew,

Oh, I just didn't know that being in Homebrew "immediately" meant it was enabled in Linuxbrew -- that's pretty awesome, and definitely reduces the importance of my comment!

Can you let us know here when STP is in Linuxbrew? That makes it much more appealing to get this PR merged (not that it isn't appealing currently, it just makes it more appealing once it addresses macOS and Linux!).

I only set it up since cryptominisat already had a Python dependency

@msoos is the main author of CMS (and also a maintainer of STP), so he can confirm this, but I wasn't aware that Python was a hard dependency of CMS.

We can add a test if you like.

What's the status of running ctest as part of brew install? STP has a bunch of tests (where Python is tested if Python built-in) via ctest -- that's probably nicer than home-rolling a load of STP's tests into the Homebrew formula, if we can do that.

[carlocab]

Can you let us know here when STP is in Linuxbrew? That makes it much more appealing to get this PR merged (not that it isn't appealing currently, it just makes it more appealing once it addresses macOS and Linux!).

Sure, will do.

I only set it up since cryptominisat already had a Python dependency

@msoos is the main author of CMS (and also a maintainer of STP), so he can confirm this, but I wasn't aware that Python was a hard dependency of CMS.

Oh, I am pretty sure CMS doesn't need Python. It just so happens that the Homebrew CMS formula declares a Python dependency. It was there when the formula was first added to Homebrew/core, so I guess whoever contributed it wanted the Python bindings.

We can add a test if you like.

What's the status of running ctest as part of brew install? STP has a bunch of tests (where Python is tested if Python built-in) via ctest -- that's probably nicer than home-rolling a load of STP's tests into the Homebrew formula, if we can do that.

We don't run unit tests, unfortunately. (With a handful of exceptions for security-sensitive software: gnupg, etc.) We package a lot of software and have limited CI resources. The tests are mostly there to catch linkage failures (e.g. when one of its dependencies is updated), and to make sure nothing's broken by brew's relocation code.

[aytey]

Just so I know: is your comment on #353 because you tried to get this working? I only ask as, if you're trying to do it, I don't need to 🤗

[carlocab]

stp is now in Linuxbrew.

Just so I know: is your comment on #353 because you tried to get this working? I only ask as, if you're trying to do it, I don't need to 🤗

Oh, my comment there was because I had faced a similar difficulty (trying to install STP using brew without having set PYTHON_LIB_INSTALL_DIR first will fail, because CMake will try to write somewhere it's not allowed to). It didn't look to me like there was a solution in that thread, so I shared the one I found and put in the STP Homebrew formula.

I haven't been able to test the Python module yet, but I imagine I'll get to it in the next few days.

[carlocab]

Ran into a little hiccup:

>>> import stp
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/usr/local/lib/python3.9/site-packages/stp/__init__.py", line 23, in <module>
    from .stp import Expr, Solver, stp, add, bitvec, bitvecs, check, model
  File "/usr/local/lib/python3.9/site-packages/stp/stp.py", line 45, in <module>
    from library_path import PATHS
ModuleNotFoundError: No module named 'library_path'

However, this small modification to stp.py fixes it:

--- stp.py.old	2021-04-26 19:27:13.000000000 +0100
+++ stp.py	2021-04-26 19:27:49.000000000 +0100
@@ -42,7 +42,7 @@
 if Py3:
     long = int
 
-from library_path import PATHS
+from stp.library_path import PATHS
 
 for path in PATHS:
     if not os.path.exists(path):

Seems to be working perfectly fine after that.

[msoos]

Sorry for my late response here. Yep, CMS doesn't need python, in fact it barely needs anything on base setup :) Also, this is amazing work, I am so amazed at the community sometimes! So much work. It's incredible to see. Anyway, this looks amazing.

Wanna merge @andrewvaughanj ?

[carlocab]

Very little work was needed on my end -- it was all made easy by other people's work (including yours!).

I opened #401 for the fix I suggest in #400 (comment) because I think it's something you'd want to apply more generally.

[aytey]

All good! Thanks, @carlocab!