Difficulties building Z3 with Julia binding

[JeffreySarnoff]

Members of the Julia Community are quite excited to work with Z3 in Julia, and develop uses that benefit from Julia and its ecosystem. We are having difficulty building Z3 with the Julia interface (see here and we know of this closed issue). It would be a great help to us if you were to add more detail (explicit step-by-step instructions known to work, and detailed expectations about environment and location of whatever files are sought). Our large binary resource maintainers have asked me to request a new release of Z3 when the Julia API is more accessible, and directions are clearer.

Thank you for the consideration.

[NikolajBjorner]

we currently build on every commit for the MacOS. The build script is here:

z3/azure-pipelines.yml

Line 183 in 6088da5

- script: brew cask install julia

@ahumenberger prepared the script and also created the bindings. He uses a MacOS, so it was easier to create the script for this environment. I am very happy to include CI builds on other platforms, but similar to you, figuring out the magic dependencies is going to take some arm-twisting. If you (or others) can see what should be done for other platforms, say Ubuntu, based on the MacOS script a pull request with an update to the CI pipeline is very welcome. In this way we can build on every push.
If there are other issues, that are orthogonal to this, that hold you back, feel welcome to add context on what will help you.

[JeffreySarnoff]

That it is available for MacOS is good news. We need to support it on vanilla Linux and Windows for Z3 to become part of Julia designer's capabilities. I will see what others may decipher for those platforms and let you know. Thanks.

[ahumenberger]

The Julia bindings sit on top of the C++ API and use CxxWrap.jl. I'm basically waiting for a new Z3 release which then includes the Julia bindings, and then I would update z3_jll such that also the Julia bindings are built. The Julia package Z3.jl will then use z3_jll.

[JeffreySarnoff]

more detailed info from @ahumenberger partially paraphrased

There is currently a Z3 pull request pending which updates the Julia bindings to libcxxwrap 0.7. After that is merged, we need a new release of Z3 (so we can, in turn, update our z3_jll). The package ahumenberger/Z3.jl could then use this updated z3_jll and that should allow Z3 with the Julia bindings to work with Mac, Linux and Windows. (Right now, ahumenberger/Z3.jl builds an older version of Z3 on the fly. Updating the package to use z3_jll (once we have new Z3 release) should be easy.)

[NikolajBjorner]

I would like to add Julia to the ubuntu and Windows builds.
For ubuntu, I am not sure how to even install Julia reliably for newest versions.
Ubuntu users certainly have something as simple as 'brew cask'?

root@nikolaj-sl2:~/z3/build# sudo apt-get update
Hit:1 http://archive.ubuntu.com/ubuntu bionic InRelease
Hit:2 http://archive.ubuntu.com/ubuntu bionic-updates InRelease
Hit:3 http://archive.ubuntu.com/ubuntu bionic-backports InRelease
Hit:4 https://packages.microsoft.com/ubuntu/16.04/prod xenial InRelease
Ign:5 http://ppa.launchpad.net/staticfloat/julia-deps/ubuntu bionic InRelease
Hit:6 http://security.ubuntu.com/ubuntu bionic-security InRelease
Ign:7 http://ppa.launchpad.net/staticfloat/juliareleases/ubuntu bionic InRelease
Err:8 http://ppa.launchpad.net/staticfloat/julia-deps/ubuntu bionic Release
  404  Not Found [IP: 91.189.95.83 80]
Err:9 http://ppa.launchpad.net/staticfloat/juliareleases/ubuntu bionic Release
  404  Not Found [IP: 91.189.95.83 80]
Reading package lists... Done
E: The repository 'http://ppa.launchpad.net/staticfloat/julia-deps/ubuntu bionic Release' does not have a Release file.
N: Updating from such a repository can't be done securely, and is therefore disabled by default.
N: See apt-secure(8) manpage for repository creation and user configuration details.
E: The repository 'http://ppa.launchpad.net/staticfloat/juliareleases/ubuntu bionic Release' does not have a Release file.
N: Updating from such a repository can't be done securely, and is therefore disabled by default.
N: See apt-secure(8) manpage for repository creation and user configuration details.
root@nikolaj-sl2:~/z3/build# sudo apt-get install julia
Reading package lists... Done
Building dependency tree
Reading state information... Done
Package julia is not available, but is referred to by another package.
This may mean that the package is missing, has been obsoleted, or
is only available from another source

E: Package 'julia' has no installation candidate

[NikolajBjorner]

Note though, that the Azure self-hosted agents come with Julia 1.4.0 pre-installed.

[JeffreySarnoff]

I have asked that someone with those answers participate here.

[giordano]

For ubuntu, I am not sure how to even install Julia reliably for newest versions.

The easiest way to install Julia is to download the official binary from https://julialang.org/downloads/ and unpack it, that's it. It should just work(TM)

[JeffreySarnoff]

Julia version 1.4.1 is the current stable release.
The 64-bit links on the download page that @giordano highlighted:

mac

linux

windows

For these binaries, there are Platform Specific Installation Instructions

[NikolajBjorner]

Thanks!

[NikolajBjorner]

As a first step I have added automatic builds of Julia bindings to also Ubuntu and Windows, #4199.
The azure-pipeline script should give an idea of how to build the bindings. (as a side note: the script that extracts the library path returns a path to "bin" instead of "lib" on Windows, perhaps this is a platform bug in the Julia package).
This of course takes some dependencies on cmake. It does not (yet) include unit tests (@ahumenberger - do you have some that we can include in the builds?) that would provide additional use-case information.
I am not familiar with downstream package creation process and will have to leave this to experts. For Python, we integrated creation of a pip package thanks to UCSB and Audrey Dutcher's magic. The build process for the pip package uses a CentOS VM, which apparently gives some cross Linux compatibility.

[giordano]

as a side note: the script that extracts the library path returns a path to "bin" instead of "lib" on Windows, perhaps this is a platform bug in the Julia package

I'm not familiar with that package, but usually in Julia we expect libraries to be installed in "bin/", because Windows doesn't have the concept of rpath and only uses the PATH environment variable, which usually points to the "bin/" directory.

I am not familiar with downstream package creation process and will have to leave this to experts. For Python, we integrated creation of a pip package thanks to UCSB and Audrey Dutcher's magic. The build process for the pip package uses a CentOS VM, which apparently gives some cross Linux compatibility.

To build binaries for Julia packages we generally use BinaryBuilder. Versions 4.8.6 and 4.8.7 of z3 are already available at https://github.com/JuliaBinaryWrappers/z3_jll.jl, tarballs for Linux (i686, x86_64, armv7l, aarch64 and powerpc64le), FreeBSD (x86_64), Windows (i686, x86_64) and macOS (x86_64).

[ahumenberger]

This of course takes some dependencies on cmake. It does not (yet) include unit tests (@ahumenberger - do you have some that we can include in the builds?) that would provide additional use-case information.

I would have added tests to the corresponding Julia package Z3.jl which loads the libz3jl library (then available via https://github.com/JuliaBinaryWrappers/z3_jll.jl) via CxxWrap.jl. To be honest, I don't know how to add meaningful tests for just the C++ part of the wrapper. I checked some other project which use CxxWrap/libcxxwrap, but I didn't find tests.

Regarding the use-case information: libz3jl is supposed to be loaded via a one-liner @wrapmodule("path/to/lib") in Z3.jl. wrapmodule then creates all the types/methods exposed in https://github.com/Z3Prover/z3/blob/master/src/api/julia/z3jl.cpp.
That is, Z3.jl provides the information how to use libz3jl. I will update the README of the Z3 repository, once everything is set up on the Julia side (z3_jll.jl, Z3.jl).

[JeffreySarnoff]

@NikolajBjorner as I understand it, now that you have added automatic builds of Julia bindings to also Ubuntu and Windows, the next step is to release a new version of Z3.
With the existence of that new version (incorporating the new automatic builds), people with Julia expertise (particularly with BinaryBuilder.jl) should be able to provide the additional autoprovisioning of Z3. @giordano is this correct?