Skip to content

Commit

Permalink
#380: reduce manual steps for publishing Z3, create copies of library…
Browse files Browse the repository at this point in the history 
… for backwards compatibility.
  • Loading branch information
@kfriedberger
kfriedberger committed Oct 13, 2024
1 parent 2349bae commit 68bab2b
Show file tree
Hide file tree
Showing 3 changed files with 143 additions and 82 deletions.
166 changes: 105 additions & 61 deletions build/build-publish-solvers/solver-z3.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,32 +18,62 @@ SPDX-License-Identifier: Apache-2.0
<property name="z3.project.name" value="Java Bindings for Z3"/>
<property name="z3.javadoc.dir" value="Javadoc-z3"/>

<target name="package-z3" depends="get-z3-version, package-z3-sources, package-z3-javadoc">
<!-- Copy Z3 binaries to the root folder along with the version postfix.
This package provides the JNI for direct usage. -->
<target name="check-z3-path">
<fail unless="z3.path">
Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin` directory).
The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and can be relative or absolute.
Note that shell substitutions do not work.
Please provide all releases (Linux, MacOS, and Windows for x64 architecture) together in the same root directory,
e.g., copy the releases (especially the content of their `bin` directories) together into one directory.
The only overlap between those releases is the JAR file, which should be equal anyway.
Additionally, make the Java sources available in this directory.
This can be done by:
- copying the content of sources-zip into the current directory (or vice versa)
- executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required.
</fail>
<fail unless="z3.pathArm64">
Please specify the path to Z3 (ARM64 version) with the flag -Dz3.pathArm64=/path/to/z3 (e.g. `bin` directory).
The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and can be relative or absolute.
Note that shell substitutions do not work.
Please provide all releases (Linux, MacOS, and Windows for ARM64 architecture) together in the same root directory,
e.g., copy the releases (especially the content of their `bin` directories) together into one directory.
The only overlap between those releases is the JAR file, which should be equal anyway.
INFO
Please specify the path to Z3 sources directory with the flag '-Dz3.path=/path/to/z3/z3-unpacked-sources'.
The path should contain directories like './src/' and './scripts/', and can be relative or absolute.
Please provide all unpacked releases (Linux, MacOS, and Windows for x64 and arm64
architecture) in the same parent directory './../' above the 'z3.path'.
This script does not expect other z3-related files or directories in the parent directory.
For example, the directory structure can look like this:

z3/ // &lt;-- parent directory
|-- z3-4.13.2-arm64-glibc-2.34/ // &lt;-- unpacked release artifact
|-- z3-4.13.2-arm64-osx-11.0/
|-- z3-4.13.2-arm64-win/
|-- z3-4.13.2-x64-glibc-2.35/
|-- z3-4.13.2-x64-osx-12.7.6/
|-- z3-4.13.2-x64-win/
|-- z3-z3-4.13.2/ // &lt;-- sources directory as 'z3.path'

This can be achieved by:
- download all artifacts (Linux, MacOS, and Windows for x64 and arm64 architecture)
from the Z3 release webpage (https://github.com/Z3Prover/z3/releases)
- create an empty directory 'z3/' and unpack all artifact into it.
- in the sources directory execute `python scripts/mk_make.py --java` to generate all
Java related files (required for JavaDoc). Executing `make` is not required.
</fail>
<exec executable="readelf" dir="${z3.path}" outputproperty="z3.elf_details" logError="true" failonerror="true">
</target>

<target name="package-z3" depends="check-z3-path,get-z3-version, package-z3-sources, package-z3-javadoc">
<!-- collect all files -->
<!-- TODO: Z3 forgot to include Java bindings into its Linux-ARM64 release in 4.13.2,
so we ignore those files currently. See https://github.com/Z3Prover/z3/issues/7406 -->
<copy todir="./" flatten="true" verbose="true">
<fileset dir="${z3.path}/../">
<include name="z3-*-x64-glibc-*/bin/com.microsoft.z3.jar"/>
</fileset>
</copy>
<copy todir="x64/" flatten="true" verbose="true">
<fileset dir="${z3.path}/../">
<include name="z3-*-x64-glibc-*/bin/libz3*.so"/>
<include name="z3-*-x64-osx-*/bin/libz3*.dylib"/>
<include name="z3-*-x64-win/bin/**/*z3*.dll"/>
</fileset>
</copy>
<copy todir="arm64/" flatten="true" verbose="true">
<fileset dir="${z3.path}/../">
<!-- <include name="z3-*-arm64-glibc-*/bin/libz3*.so"/> -->
<include name="z3-*-arm64-osx-*/bin/libz3*.dylib"/>
<include name="z3-*-arm64-win/bin/**/*z3*.dll"/>
</fileset>
</copy>

<!-- check for properties of Z3 for Linux -->
<exec executable="readelf" dir="./" outputproperty="z3.elf_details" logError="true" failonerror="true">
<arg value="-d"/>
<arg value="libz3.so"/>
<arg value="x64/libz3.so"/>
</exec>
<fail>
<condition>
Expand All @@ -53,64 +83,78 @@ SPDX-License-Identifier: Apache-2.0
Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'.
</fail>

<mkdir dir="x64"/>
<mkdir dir="arm64"/>
<!-- Linux files -->
<copy file="${z3.path}/libz3.so" tofile="x64/libz3-${z3.version}.so"/>
<copy file="${z3.path}/libz3java.so" tofile="x64/libz3java-${z3.version}.so"/>
<copy file="${z3.pathArm64}/libz3.so" tofile="arm64/libz3-${z3.version}.so"/>
<copy file="${z3.pathArm64}/libz3java.so" tofile="arm64/libz3java-${z3.version}.so"/>
<move file="x64/libz3.so" tofile="x64/libz3-${z3.version}.so" verbose="true"/>
<move file="x64/libz3java.so" tofile="x64/libz3java-${z3.version}.so" verbose="true"/>
<!-- <move file="arm64/libz3.so" tofile="arm64/libz3-${z3.version}.so"/> -->
<!-- <move file="arm64/libz3java.so" tofile="arm64/libz3java-${z3.version}.so"/> -->
<!-- Windows files -->
<copy file="${z3.path}/libz3.dll" tofile="x64/libz3-${z3.version}.dll"/>
<copy file="${z3.path}/libz3java.dll" tofile="x64/libz3java-${z3.version}.dll"/>
<copy file="${z3.pathArm64}/libz3.dll" tofile="arm64/libz3-${z3.version}.dll"/>
<copy file="${z3.pathArm64}/java/z3java.dll" tofile="arm64/libz3java-${z3.version}.dll"/>
<move file="x64/libz3.dll" tofile="x64/libz3-${z3.version}.dll" verbose="true"/>
<move file="x64/libz3java.dll" tofile="x64/libz3java-${z3.version}.dll" verbose="true"/>
<move file="arm64/libz3.dll" tofile="arm64/libz3-${z3.version}.dll" verbose="true"/>
<move file="arm64/z3java.dll" tofile="arm64/libz3java-${z3.version}.dll" verbose="true"/>
<!-- MacOS files -->
<copy file="${z3.path}/libz3.dylib" tofile="x64/libz3-${z3.version}.dylib"/>
<copy file="${z3.path}/libz3java.dylib" tofile="x64/libz3java-${z3.version}.dylib"/>
<copy file="${z3.pathArm64}/libz3.dylib" tofile="arm64/libz3-${z3.version}.dylib"/>
<copy file="${z3.pathArm64}/libz3java.dylib" tofile="arm64/libz3java-${z3.version}.dylib"/>
<move file="x64/libz3.dylib" tofile="x64/libz3-${z3.version}.dylib" verbose="true"/>
<move file="x64/libz3java.dylib" tofile="x64/libz3java-${z3.version}.dylib" verbose="true"/>
<move file="arm64/libz3.dylib" tofile="arm64/libz3-${z3.version}.dylib" verbose="true"/>
<move file="arm64/libz3java.dylib" tofile="arm64/libz3java-${z3.version}.dylib" verbose="true"/>
<!-- common Java file, Java is platform independent -->
<copy file="${z3.path}/com.microsoft.z3.jar" tofile="com.microsoft.z3-${z3.version}.jar"/>
<move file="com.microsoft.z3.jar" tofile="com.microsoft.z3-${z3.version}.jar"/>

<!--
We additionally provide x64-files without arch-attribute for backwards compatibility,
such that applications can load dependencies without changing their Ivy configuration.
Those files are not part of any direct configuration, but will be resolved if the
arch-attribute is not used.
-->
<copy todir="./" flatten="true" verbose="true">
<fileset dir="x64/"/>
</copy>
</target>

<target name="get-z3-version" unless="z3.version">
<fail unless="z3.path">
Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin` directory).
The path has to point to the root Z3 folder and can be relative or absolute.
Note that shell substitutions do not work.
Please provide all releases (Linux, MacOS, and Windows) together in the same root directory,
e.g., copy the releases (especially the content of their `bin` directories) together into one directory.
The only overlap between those releases is the JAR file, which should be equal anyway.
Additionally, make the Java sources available in this directory.
This can be done by:
- copying the content of sources-zip into the current directory (or vice versa)
- executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required.
</fail>
<target name="get-z3-version" unless="z3.version" depends="check-z3-path">
<echo>Option -Dz3.version=... not specified. Trying to determine z3.version from git repository. This will fail if git repository is not available.</echo>
<exec executable="git" dir="${z3.path}" outputproperty="z3.version" failonerror="true">
<arg value="describe" />
<arg value="describe"/>
</exec>
</target>

<target name="publish-z3" depends="package-z3, load-ivy"
description="Publish Z3 binaries to Ivy repo.">
<ivy:resolve conf="solver-z3,solver-z3-x64,solver-z3-arm64,sources,javadoc" file="solvers_ivy_conf/ivy_z3.xml"/>
<publishToRepository solverName="Z3" solverVersion="${z3.version}"/>

<!--
We additionally provide x64-files without arch-attribute for backwards compatibility,
such that applications can load dependencies without changing their Ivy configuration.
Those files are not part of any direct configuration, but will be resolved if the
arch-attribute is not used.
-->
<echo>
Lets copy the files for architecture x64 into main directory, for backwards compatibility.
Afterwards, please execute the SVN command from above.
</echo>
<copy todir="repository/${ivy.organisation}/${ivy.module}/" verbose="true">
<fileset dir="repository/${ivy.organisation}/${ivy.module}/x64/">
<include name="*-${z3.version}.*"/>
</fileset>
</copy>
</target>

<target name="check-z3-sources">
<!-- check for prepared Java sources -->
<available file="${z3.path}/../src/api/java/Expr.java" property="isZ3NativeExprAvailable" />
<fail unless="isZ3NativeExprAvailable" message="The sources of Z3 (Java bindings) can not be found." />
<available file="${z3.path}/../src/api/java/Native.java" property="isZ3NativeApiFileAvailable" />
<fail unless="isZ3NativeApiFileAvailable" message="The sources of Z3 are not yet prepared. Please execute `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required." />
<available file="${z3.path}/src/api/java/Expr.java"
property="isZ3NativeExprAvailable"/>
<fail unless="isZ3NativeExprAvailable" message="The sources of Z3 (Java bindings) can not be found."/>
<available file="${z3.path}/src/api/java/Native.java"
property="isZ3NativeApiFileAvailable"/>
<fail unless="isZ3NativeApiFileAvailable" message="The sources of Z3 are not yet prepared. Please execute `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required."/>
</target>

<target name="package-z3-sources" depends="get-z3-version, check-z3-sources">
<jar destfile="com.microsoft.z3-${z3.version}-sources.jar" whenmanifestonly="fail">
<zipfileset dir="${z3.path}/../src/api/java" includes="**/*.java" prefix="com/microsoft/z3"/>
<zipfileset dir="${z3.path}/../" includes="LICENSE.txt" prefix="META-INF"/>
<zipfileset dir="${z3.path}/src/api/java" includes="**/*.java" prefix="com/microsoft/z3"/>
<zipfileset dir="${z3.path}/" includes="LICENSE.txt" prefix="META-INF"/>
<manifest>
<attribute name="Implementation-Title" value="${z3.project.name}"/>
<attribute name="Implementation-Version" value="${z3.version}"/>
Expand All @@ -133,7 +177,7 @@ SPDX-License-Identifier: Apache-2.0
failonwarning="false"
overview="doc/javadoc_overview.html"
>
<fileset dir="${z3.path}/../src/api/java">
<fileset dir="${z3.path}/src/api/java">
<include name="**/*.java"/>
</fileset>
<link href="https://docs.oracle.com/en/java/javase/11/docs/api/"/>
Expand All @@ -147,8 +191,8 @@ SPDX-License-Identifier: Apache-2.0

<target name="package-z3-javadoc" depends="z3-javadoc">
<jar jarfile="com.microsoft.z3-${z3.version}-javadoc.jar" whenmanifestonly="fail">
<zipfileset dir="${z3.path}/../" includes="LICENSE.txt" prefix="META-INF"/>
<fileset dir="${z3.javadoc.dir}" />
<zipfileset dir="${z3.path}/" includes="LICENSE.txt" prefix="META-INF"/>
<fileset dir="${z3.javadoc.dir}"/>
</jar>
</target>
</project>
36 changes: 25 additions & 11 deletions doc/Developers-How-to-Release-into-Ivy.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,19 +50,32 @@ please build from source only if necessary (e.g., in case of an important bugfix

To publish Z3, download the **Linux**, **Windows**, and **OSX** binary (for both, x64 and ARM64 architecture)
and the sources (for JavaDoc) for the [latest release](https://github.com/Z3Prover/z3/releases) and unzip them.
In the unpacked sources directory, prepare Java sources via `python scripts/mk_make.py --java`.
For simpler handling, we then copy the files together into two directories:
- use the source directory as `Z3_DIR`.
- from the three `*x64*/bin` directories together into directory `$Z3_DIR`,
- from the three `*arm64*/bin` directories together into another directory `Z3_DIR_ARM64`.
For example, the directory structure can look like this:

```
z3/ // <-- parent directory
|-- z3-4.13.2-arm64-glibc-2.34/ // <-- unpacked release artifact
|-- z3-4.13.2-arm64-osx-11.0/
|-- z3-4.13.2-arm64-win/
|-- z3-4.13.2-x64-glibc-2.35/
|-- z3-4.13.2-x64-osx-12.7.6/
|-- z3-4.13.2-x64-win/
|-- z3-z3-4.13.2/ // <-- sources directory used as 'z3.path'
```

In the unpacked sources directory, prepare Java sources via `python3 scripts/mk_make.py --java`.
Then execute the following command in the JavaSMT directory,
where `$Z3_DIR` is the absolute path of the unpacked Z3 directory
and `$Z3_VERSION` is the version number:
where `$Z3_DIR` is the path of the sources directory and `$Z3_VERSION` is the version number:
```
ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.pathArm64=$Z3_DIR_ARM64/bin -Dz3.version=$Z3_VERSION
ant publish-z3 -Dz3.path=$Z3_DIR -Dz3.version=$Z3_VERSION
```
Example:
```
ant publish-z3 -Dz3.path=/workspace/solvers/z3/z3-z3-4.13.2 -Dz3.version=4.13.2
```
Finally, follow the instructions shown in the message at the end.


#### Optional (from source for Linux target with older GLIBC)
This step is for the following use case:
Newer releases of Z3 depend on newer versions of GLIBC (>=v2.35),
Expand All @@ -73,15 +86,16 @@ in which the following build command can be run in the unpacked source directory
```
python3 scripts/mk_make.py --java && cd build && make -j 2
```
Afterwards copy the native libraries for Linux (`libz3.so` and `libz3java.so`) from the directory `./build` into `./bin`.
Afterwards copy the native libraries for Linux (`libz3.so` and `libz3java.so`) from the directory
`./build` into `./bin` (if needed, adjust the directory to match the x64 or arm64 path for Linux).
Then perform as written above with adding the additional pre-compiled binaries for other operating systems,
and publish the directory `./bin` with an ant command like the one from above:
```
ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION-glibc_2.27
ant publish-z3 -Dz3.path=$Z3_DIR -Dz3.version=$Z3_VERSION-glibc_2.27
```


#### Optional (outdated: from source for Linux target)
#### Optional (from source for Linux target) (Info: this step is outdated and no longer used for releases of JavaSMT)
To publish Z3 from source, [download it](https://github.com/Z3Prover/z3) and build
it with the following command in its directory on a 64bit Ubuntu 16.04 system:
```
Expand Down
Loading

0 comments on commit 68bab2b

Please sign in to comment.