Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Release boolector as a PyPi package #49

Closed mballance closed 3 years ago

mballance commented 5 years ago

Hello, I've been using Boolector via the C API, and have recently started using the Python interface. I'd like to have Boolector available via the PyPi package repository (pypi.org), and it doesn't appear to be directly available at the moment. I'm happy to volunteer to put together such a package, but wanted to check if there are concerns about doing so.

Thanks, Matthew

mpreiner commented 5 years ago

Hi Matthew,

Thanks for the offer! Would you be also willing to take care and maintain PyPi releases for new versions of Boolector? As soon as there is a PyPi package users probably expect it to be up-to-date and I'm not sure if we currently have the bandwidth to do it ourselves.

Cheers, Mathias

mballance commented 5 years ago

Hi Mathias, Yes, I'd very much be willing to maintain and update the PyPi release as new versions of Boolector become available.

Best Regards, Matthew

On Thu, Jun 6, 2019 at 8:58 PM Mathias Preiner notifications@github.com wrote:

Hi Matthew,

Thanks for the offer! Would you be also willing to take care and maintain PyPi releases for new versions of Boolector? As soon as there is a PyPi package users probably expect it to be up-to-date and I'm not sure if we currently have the bandwidth to do it ourselves.

Cheers, Mathias

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Boolector/boolector/issues/49?email_source=notifications&email_token=AAKHLBKTJMFS73ZG24PXVNTPZHMHXA5CNFSM4HS5JGHKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODXEY64Q#issuecomment-499748722, or mute the thread https://github.com/notifications/unsubscribe-auth/AAKHLBL5CDHI7G5EQ6JT45DPZHMHXANCNFSM4HS5JGHA .

mpreiner commented 5 years ago

That's great! Thanks! You can go ahead with the PyPi package. Let us know if you need anything from us!

obijywk commented 4 years ago

@mballance any progress on this? I'd be very interested in a PyPI package for Boolector as well.

mballance commented 4 years ago

@obijywk, great to hear that you are also interested in this! This project has been lagging behind a couple of my other projects, but I expect to be able to get an initial version ready in the next week or so. Turns out Python packaging has lots of moving parts -- especially if the package involves native extensions like Boolector does. Just out of curiosity, what is your preferred platform (eg Windows, Linux, OS-X)?

-Matthew

obijywk commented 4 years ago

Yeah, I don't expect this to be trivial to do :-/ let me know if there's anything I can do to help. I'm only interested in Linux.

mballance commented 4 years ago

Okay, I have an initial version that seems to be working. Building a binary package that should work across Linux versions requires using a very old version of Centos, which required a few small patches to the Boolector and Lingeling sources. For now, I'm storing the relevant files (Dockerfile, scripts, setup.py, etc) here: https://github.com/mballance/pyboolector. If anyone is interested in trying this out, you can do the following :

% pip install --index-url https://test.pypi.org/simple pyboolector

Note that the binary packages are Linux-only at the moment, and only on the 'Testing' PyPi site.

obijywk commented 4 years ago

Worked for me! I tried it in https://colab.research.google.com by running the following:

import sys !{sys.executable} -m pip install --index-url https://test.pypi.org/simple pyboolector

so not sure exactly what kind of Linux it's running under, but it worked.

mballance commented 4 years ago

That's great to hear, @obijywk! It's working for me as well, so I guess the next step is to figure out how to get this more-integrated with the CI environment that Boolector uses.

obijywk commented 4 years ago

any progress on getting this into the real PyPI (not the test instance)? looking forward to adding it to requirements.txt for my project.

mballance commented 4 years ago

Yes, actually. I've been working on getting an Azure pipelines project setup within Boolector to automatically build and push a release to PyPi, since I believe that is the right path forward. At the moment, I believe I have everything working on a branch, with a PR to come. You should be able to install directly from PyPi now. As always, feedback is much appreciated!

-Matthew

mballance commented 4 years ago

Here's a link to the updated pull request: https://github.com/Boolector/boolector/pull/72

skochinsky commented 4 years ago

Any chance for Windows support? Currently getting this:

Collecting pyboolector
  Downloading https://files.pythonhosted.org/packages/ec/23/f499c92ddfa1493d23dce0c8bbee2047a3c88b8b6bf3843a4d3ce8b1720a
/PyBoolector-3.2.0.20200301.4.tar.gz
    ERROR: Command errored out with exit status 1:
     command: 'C:\Program Files\Python38\python.exe' -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'C:\\Users\
\Igor\\AppData\\Local\\Temp\\pip-install-thmt_klo\\pyboolector\\setup.py'"'"'; __file__='"'"'C:\\Users\\Igor\\AppData\\L
ocal\\Temp\\pip-install-thmt_klo\\pyboolector\\setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.
read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' egg_info --egg-bas
e pip-egg-info
         cwd: C:\Users\Igor\AppData\Local\Temp\pip-install-thmt_klo\pyboolector\
    Complete output (5 lines):
    Traceback (most recent call last):
      File "<string>", line 1, in <module>
      File "C:\Users\Igor\AppData\Local\Temp\pip-install-thmt_klo\pyboolector\setup.py", line 14, in <module>
        with open(cmakelists_txt, "r") as f:
    FileNotFoundError: [Errno 2] No such file or directory: 'C:\\Users\\Igor\\AppData\\Local\\Temp\\pip-install-thmt_klo
\\CMakeLists.txt'
    ----------------------------------------
ERROR: Command errored out with exit status 1: python setup.py egg_info Check the logs for full command output.

Build on install is unlikely to work with so many dependencies so prebuilt binaries would be appreciated.

skochinsky commented 4 years ago

same story on Mac:

Collecting pyboolector
  Using cached https://files.pythonhosted.org/packages/ec/23/f499c92ddfa1493d23dce0c8bbee2047a3c88b8b6bf3843a4d3c720a/PyBoolector-3.2.0.20200301.4.tar.gz
    Complete output from command python setup.py egg_info:
    Traceback (most recent call last):
      File "<string>", line 1, in <module>
      File "/private/var/folders/12/yvjfpl856hl12y1p90tg7mgw0000gt/T/pip-install-l_38ao0n/pyboolector/setup.py",  14, in <module>
        with open(cmakelists_txt, "r") as f:
    FileNotFoundError: [Errno 2] No such file or directory: '/private/var/folders/12/yvjfpl856hl12y1p90tg7mgw0000/pip-install-l_38ao0n/CMakeLists.txt'
mballance commented 4 years ago

Hi @skochinsky, I agree that both Windows and OS-X support are desirable. Of the two, Windows seems more difficult because Python packaging wants native packages to be compiled with Visual Studio compilers. Unfortunately, Boolector doesn't compile cleanly with VS at the moment. OS-X may be simpler, but I don't have any personal experience here.

Are you able to help with either of these issues?

I would ask the Boolector maintainers whether there is interest/openness to a Visual Studio build of Boolector. Based on my initial investigation I suspect it's quite doable, though it appears it will require a non-trivial number of mostly-trivial changes.

-Matthew

mpreiner commented 3 years ago

Added with https://github.com/Boolector/boolector/pull/72.