Can't add dependency on Z3 python wrapper

Help
1

Hi!

I’m trying to package manticore, which has a dependency on the Z3 SMT solver.

I tried this expression:

{
  pkgs ? import <nixpkgs> { },
}:

with pkgs.python36Packages;

buildPythonApplication rec {
  pname = "manticore";
  version = "0.2.2";

  propagatedBuildInputs = [ pkgs.python36Packages.z3 ];

  src = fetchPypi {
    inherit pname version;
    sha256 = "03mgw6kzqhghxcdab2kha27gqqw5ykb6vzi7zkw46zh767ifqyxz";
  };
}

But I get

installing
/build/manticore-0.2.2/dist /build/manticore-0.2.2
Processing ./manticore-0.2.2-py3-none-any.whl
Collecting z3-solver (from manticore==0.2.2)
  Could not find a version that satisfies the requirement z3-solver (from manticore==0.2.2) (from versions: )
No matching distribution found for z3-solver (from manticore==0.2.2)
builder for '/nix/store/yyaxnw9pykjv954pk0459zwxg9yqspkq-python3.6-manticore-0.2.2.drv' failed with exit code 1
error: build of '/nix/store/yyaxnw9pykjv954pk0459zwxg9yqspkq-python3.6-manticore-0.2.2.drv' failed

Any idea why the dependency is not detected at build-time?

2

It seems our z3 derivation does not contain any dist-info or egg-info folder, and thus pip and setuptools don’t consider the package installed. We should provide a dist-info folder. I can’t see directly where it goes wrong; whether z3 simply does not create the folder, or whether they do and we’re not moving it to $out.

3

Are we packaging the source from Microsoft or the angr’fork that provided proper packaging as a wheel?

4

We’re packaging upstream. Not sure how in sync the fork is with upstream.

If it is well maintained, maybe it would make sense to package that insteead. Or alternaltively, add the missing bits ourselves?

5

To answer my own question: it doesn’t seem like the angr fork is in sync. Old releases and so on.

Haven’t got any experience packaging Python so can’t really say anything meaningful about how much effort it would take for us to provide the missing pieces.

6

The patch they made was actually quite simple. We make the effort to push this upstream.

7

Can you produce (or point me to how to get) a diff of what they added? Is it a single file, or spread across many?

Also, the fact that they maintain a separate fork makes me wonder if upstream has some issues with merging the Python packaging related work.

8

The patch is actually quite simple: Comparing Z3Prover:db679d702f20b522afff1575e316ddec6cce80dc...angr:master · Z3Prover/z3 · GitHub

9

I sent an email to the maintainer of the angr fork - I think he’s in the best position to tell us what the status is for upstreaming his contributions.

10

Got a response, the fork is not needed anymore, since the patches have been upstreamed already, and that PR should be included in the release we use in nixpkgs, AFAICT.

The question then is, is there something else we need to add?

11

The Z3 version we have in nixpkgs is 4.8.1, which already contains angr’s PR. AFAICT we should build the python bindings separately (using buildPythonPackage which uses the setup.py). Right now, we use the z3 build system which installs the python bindings using this unholy incantation:

        @mkdir -p $(DESTDIR)$(PREFIX)/lib/python3.6/site-packages/z3
        @mkdir -p $(DESTDIR)$(PREFIX)/lib/python3.6/site-packages/z3/lib
        @ln -s ../../../../libz3$(SO_EXT) $(DESTDIR)$(PREFIX)/lib/python3.6/site-packages/z3/lib/libz3$(SO_EXT)
        @cp python/z3/*.py $(DESTDIR)$(PREFIX)/lib/python3.6/site-packages/z3
        @mkdir -p $(DESTDIR)$(PREFIX)/lib/python3.6/site-packages/z3/__pycache__
        @cp python/z3/__pycache__/*.pyc $(DESTDIR)$(PREFIX)/lib/python3.6/site-packages/z3/__pycache__
12

Sorry for not replying here sooner, I don’t track Discourse closely. I’m the maintainer for Z3, though Python support was added later by request (and help from @FRidh as I’m not a Python person)

I think the original problem I had was that my attempts to naively use buildPythonPackage caused the build system to do something else unholy, which was compile a completely separate copy of Z3 and ship that with the python files, too. Or something like that. Although I think the current way we do it requires building a second copy of Z3 anyway since making python2 and python3 bindings requires changing the build inputs, resulting in two compilations. Ideally they would obviously be shared and the Python library would merely load the necessary .so file from the proper store path, and wouldn’t require recompilation…

In any case, I can take a stab at getting this information registered properly, since Z3 is fairly popular and people surely want the python bindings. I’ve had this on a TODO but of course a million other things also come up, as it happens.

1 Like