Homebrew formula improvements

[arthaud]

I looked into the new homebrew formula: https://github.com/ivanperez-keera/homebrew-core/blob/master/Formula/ikos.rb
There are a few things I would like to address:

• Right now, we are effectively installing 2 virtual environments: virtualenv_create creates one and make install creates another one
• We are not following the homebrew guidelines for python virtual envs: https://docs.brew.sh/Python-for-Formula-Authors

This is what I think we should do:

• Use virtualenv_create
• Call cmake with -DINSTALL_PYTHON_VIRTUALENV=OFF and -DPYTHON_VENV_EXECUTABLE=#{libexec}/vendor/bin/python
• After make install, call #{libexec}/vendor/bin/python -m pip install . in build/analyzer/python to install the ikos python package in the homebrew-created virtualenv (or better, https://docs.brew.sh/Python-for-Formula-Authors#installing-bindings)
• Use venv.pip_install resources to install pygments, the same way we did it before

I don't have time to try today but I could try later this week.

[ivanperez-keera]

I haven't had the chance to read https://docs.brew.sh/Python-for-Formula-Authors just yet but I have made the changes you suggested in the formula.

I tried it in a docker image and it works. ikos seems to work well inside (a basic example runs and reports errors in the C code as expected).

[ivanperez-keera]

Btw, I'm holding off on sending a PR or merging the changes into this repo until the release is final.

[ivanperez-keera]

We should also require "python@3.x" here:

homebrew-core/Formula/ikos.rb

Line 18 in cb8061c

depends_on "python"

Why do we put things in libexec/vendor? The only mention of vendor is in:

Dependencies for libraries

Library dependencies must be installed so that they are importable. To minimise the potential for linking conflicts, dependencies should be installed to libexec/ and added to sys.path by writing a second .pth file (named like “homebrew-foo-dependencies.pth”) to the prefix site-packages.

Note that, in the guide, <vendor> has angle brackets, indicating that it's not the literal string vendor. But I admit that it's a bit strange to customize <vendor> for each dependency or something like that.

[ivanperez-keera]

Also, while we are at it, should the license be NOSA?

homebrew-core/Formula/ikos.rb

Line 7 in 24cbcc2

license "MIT"

[ivanperez-keera]

We may not want to fight all of these "battles" for this release. Some of these concerns, even if appropriate, were there before 3.1 and do not prevent us from releasing. IKOS 3.3 will be out 3 months from now, so there's no need to squeeze as many fixes/features as possible in this release.

[ivanperez-keera]

I went through the guide and I could not find anything in the formula that contradicts the guide, apart from the small comment regarding <vendor>.

[ivanperez-keera]

Actually, forget about the vendor thing. First, that was added to the guide as part of a formatting commit (here), but I see nothing in the documentation that reflects that it is meant to mean "us". The parent commit uses libexec/"vendor", and the change is not clearly justified, so I would not be surprised if that was a mistake.

Second, looking through github shows that it's common enough for people to use libexec/"vendor". Since it works and I have no better proposal, let's ignore it altogether.

[arthaud]

Right, it should be NOSA instead of MIT.

Regarding the "vendor" thing, yeah I think this can go away. I see other formulas just do virtualenv_create(libexec, python3)

[ivanperez-keera]

Ok, I'll change all three things: python3, NOSA, and the virtualenv_create.

[ivanperez-keera]

I've made these changes, @arthaud . If nothing else is needed, I'll merge these into master.

If you have a chance to try it, please let me know how it goes.

[ivanperez-keera]

I'll update this with a new version number, and merge tomorrow Thursday if all goes according to plan. If you need to do any last-minute checks, @arthaud , please go ahead.