search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.41k stars 1.47k forks source link

Community maintained Linux packages for Z3 #345

Closed delcypher closed 4 years ago

delcypher commented 8 years ago

Hi,

I spent the weekend trying to package Z3 4.4.1 for Arch Linux and Ubuntu (12.04LTS and 14.04LTS) using the OpenSUSE build service (OBS) and I'd like to show the results so far and suggest future directions to take this. OBS is a free packaging service that can build packages for multiple Linux distributions (e.g. Debian, Ubuntu, Arch Linux, Red Hat, Fedora, OpenSUSE).

What I have so far

You can find information about the builds here

https://build.opensuse.org/package/show/home:delcypher:z3/z3

and if you go here

http://software.opensuse.org/download.html?project=home%3Adelcypher%3Az3&package=z3

you get handy instructions on how to add the repository and install the packages.

The packages are "split packages" for both Arch Linux and Ubuntu which means there is not a single z3 package with everything in it. Instead the packages are split into smaller packages, you can find out what they are by looking at

There are binding packages for the python bindings (python 2 and 3), Java and ".NET". I'm not very happy with the Java package as it isn't following the debian packaging guidelines at all (http://www.debian.org/doc/packaging-manuals/java-policy/x110.html), I should fix that at some point but as I don't use the Java bindings I may not be the best person to do this.

Arch Linux doesn't do debug packages but for Ubuntu there are separate -dbg packages which should contain the debug symbols.

Note these packages are for Z3 4.4.1, but are patched with #338, #340 , #344 and a fix that I haven't upstreamed yet (https://build.opensuse.org/package/view_file/home:delcypher:z3/z3/0003-Python-35.patch?expand=1). The patch I haven't upstreamed isn't suitable as it only works for python 3 so it needs to be reworked.

Directions to take this work

What I think would be very useful is for a top level z3 project (i.e. not inside home:delcypher) to be set up on the OBS (they need to be manually requested) which can either be considered/advertised as

OR

depending on how much @wintersteiger @leodemoura would like to be involved. Either way if this route is taken I think it needs to be one of the project leads who asks for an official project to be setup on OBS.

Whilst that's going on it would probably be good to iterate on the packages (to get them in good shape) and also add Fedora/RedHat/OpenSUSE/Debian builds so that we can cover more distributions?

@jirislaby I saw you doing some packaging stuff in older PRs. I also seem to recall you adding packaging support for the STP SMT solver for rpm based distros, would you be interested in adding support for building rpm packages?

delcypher commented 8 years ago

I've reworked the Python3 fix that I previously mentioned so that it now works with Python 2. I've sent this upstream, see PR #350

NikolajBjorner commented 8 years ago

Can we close as pull request was merged a while ago?

delcypher commented 8 years ago

@NikolajBjorner

Can we close as pull request was merged a while ago?

No. Not until the question I actually asked is addressed.

This issue is about having proper packages for various distributions. The (now accepted) PRs that were required to implement packages are an implementation detail that I just mentioned for completeness. This issue (#345) is asking if the Z3 team would like to have

wintersteiger commented 8 years ago

Clear statement: We want community maintained packages. We don't have the bandwidth to support all package systems, so we decided to treat all of them equally by not publishing any packages. That will have to be done by the people who are in the respective communities and therefore know much better what makes sense there and what doesn't.

Of course, it must always be clear who the maintainer is and they must be able to respond to issues in a timely manner. If a maintainer can't maintain the packages any longer, they will have to either find someone else or pull the packages. There'll be no catch-all from us, as we don't even have access of whatever levels of access are required from the respective package system.

Not sure about the highlighted "proper packages", I assume all packages will be of "proper" quality.

delcypher commented 8 years ago

@wintersteiger Thank you for the clarification. I've asked the OpenSUSE build service team for the "z3" project name on their service.

I'm happy to maintain them for now. When they are set up and in a good state would it be possible to have a small link in the README or somewhere (e.g. the wiki) that points to where users can get these "community" packages?

jirislaby commented 8 years ago

@delcypher I intended to use devel:tools:statica but failed to get z3 in shape there :(. So if you have somthing working, please submit there and I will fwd to factory.

https://build.opensuse.org/package/show/devel:tools:statica/z3

delcypher commented 8 years ago

@jirislaby I didn't know about devel:tools:statica. I don't have anything working for OpenSUSE. I just have Ubuntu and Arch Linux right now. The build system is quite heavily patched too (those things are now in master) but I wanted it to basically be a stable release.

The OBS admins just got back to me asked if I wanted science:z3. What should we do?

By the way what do you mean by "I will fwd to factory"?

jirislaby commented 8 years ago

@delcypher Feel free to use whatever project you want. science:z3 makes sense too, especially if you want a separate project dedicated solely to z3. And if it was built for debian, ubuntu and others, it would be the right thing.

factory is something like debian unstable. So it would mean adding z3 to openSUSE distribution.

delcypher commented 7 years ago

Well it took a while. But the we now have https://build.opensuse.org/project/show/science:z3

There's nothing there right now. I intend to package something when I have time.

jirislaby commented 7 years ago

On 02/28/2017, 02:25 PM, Dan Liew wrote:

Well it took a while. But the we now have https://build.opensuse.org/project/show/science:z3

There's nothing there right now. I intend to package something when I have time.

We actually have devel:tools:statica with z3, stp, klee and other good stuff in there :).

https://build.opensuse.org/project/show/devel:tools:statica

-- js

jirislaby commented 7 years ago

Sorry, I am repeating myself, I thought I am replying to a different issue.

All in all -- z3 is packaged in devel:tools:statica for quite some time, so you can link it from there. Note that z3 is in openSUSE too. Klee, stp and minisat is pending legal review and will be in openSUSE in few weeks. I tried to use metasmt in klee with z3 and stp support, but klee currently requires boolector (non-free). So I have to persuade klee to not require boolector when built with metasmt...

Smattr commented 5 years ago

Of relevance to this issue, Fabian Wolff has recently started packaging Z3 4.8.4 for Debian: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=935900. My understanding is that this will eventually propagate through to Ubuntu (via Debian unstable, testing, etc).

NikolajBjorner commented 5 years ago

The newest 4.8.6 would be better (fixes a bunch of bugs around optimization, PB, so clearly not mainstream features but they get hit).

The pip package z3-solver is now built with releases directly in the Azure DevOps pipline.

XVilka commented 4 years ago

Should be this closed then? Z3 is now quite updated almost everywhere: https://repology.org/project/z3/versions

NikolajBjorner commented 4 years ago

Impressive. I learned something new today. Some of the Unix versions I used in the late 80s still exist.

NikolajBjorner commented 4 years ago

This is a candidate to create a GitHub "discussion" when it comes out. As an issue it is probably too open ended and what there exists now is well beyond the state when the issue was filed. If there are features that can be added to our releases/nightly on useful Linux variants it mainly takes a suitable docker setup and the other parts of the pipelines are fairly easy to adapt. Looking at a random package in the link I see some patches to some cmake files in z3. If these changes can be integrated in main it is welcome.