Skip to content

Improve the process of releasing into Maven repository #253

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Sep 9, 2021
Merged

Improve the process of releasing into Maven repository #253

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
9a9e28a
Ant build script for Maven release: simplify parameter value.
kfriedberger Sep 8, 2021
63cfb6b
Ant build script for Maven release: refactor redundant code into macro.
kfriedberger Sep 8, 2021
f66a35d
Ant build script: remove outdated comment and never used target.
kfriedberger Sep 8, 2021
9588559
Documentation: split release documentation into separate pages.
kfriedberger Sep 8, 2021
a10f292
Ant build scripts: adding steps to release Yices2 into Maven.
kfriedberger Sep 8, 2021
ff38713
Ant build script: fix classifier for plain jar.
kfriedberger Sep 9, 2021
52a1c4b
update/fix Yices bindings.
kfriedberger Sep 9, 2021
c1b3f6b
update example Maven projects with Yices2.
kfriedberger Sep 9, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 62 additions & 47 deletions build/build-maven-publish.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,68 +35,54 @@ SPDX-License-Identifier: Apache-2.0
</replace>
</target>

<target name="deploy-to-maven-central" depends="dist, gen-pom, jar"
description="deploy snapshot version to Maven snapshot repository">

<artifact:mvn>
<arg value="org.apache.maven.plugins:maven-deploy-plugin:2.6:deploy-file" />
<arg value="-Durl=${ossrh-snapshots-repository-url}" />
<arg value="-DrepositoryId=${ossrh-server-id}" />
<arg value="-DpomFile=pom.xml" />
<arg value="-Dfile=${jar.file}" />
</artifact:mvn>
</target>

<!-- before this, update project version (both build.xml and pom.xml) from SNAPSHOT to RELEASE -->
<!-- before this, please check that the project version is set correctly! -->
<target name="stage" depends="dist, gen-pom, jar, sources" description="deploy release version to Maven staging repository">
<fail message="unexpected filename of jar">
<condition> <!-- see property in build-jar.xml -->
<not><equals arg1="${jar.file}" arg2="${ivy.module}-${version}.jar"/></not>
</condition>
</fail>
<stage-javasmt-file filename="${ivy.module}-${version}" fileending="jar"/>
<stage-javasmt-file filename="${ivy.module}-${version}-sources" fileending="jar" classifier="sources"/>
<stage-javasmt-file filename="${ivy.module}-${version}-javadoc" fileending="jar" classifier="javadoc"/>
</target>

<!-- Sign and deploy the main artifact. -->
<artifact:mvn>
<arg value="org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file" />
<arg value="-Durl=${ossrh-staging-repository-url}" />
<arg value="-DrepositoryId=${ossrh-server-id}" />
<arg value="-DpomFile=pom.xml" />
<arg value="-Dfile=${jar.file}" />
<arg value="-Pgpg" />
</artifact:mvn>

<!-- Sign and deploy the sources artifact -->
<artifact:mvn>
<arg value="org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file" />
<arg value="-Durl=${ossrh-staging-repository-url}" />
<arg value="-DrepositoryId=${ossrh-server-id}" />
<arg value="-DpomFile=pom.xml" />
<arg value="-Dfile=${ivy.module}-${version}-sources.jar" />
<arg value="-Dclassifier=sources" />
<arg value="-Pgpg" />
</artifact:mvn>

<!-- sign and deploy the javadoc artifact -->
<!-- macro for pushing a JavaSMT file into a Maven repository
(push into the staging area, from there manual publication is required afterwards) -->
<macrodef name="stage-javasmt-file">
<attribute name="filename"/>
<attribute name="fileending"/>
<attribute name="filedirectory" default="."/>
<attribute name="classifier" default=""/>
<sequential>
<artifact:mvn>
<arg value="org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file" />
<arg value="-Durl=${ossrh-staging-repository-url}" />
<arg value="-DrepositoryId=${ossrh-server-id}" />
<arg value="-DpomFile=pom.xml" />
<arg value="-Dfile=${ivy.module}-${version}-javadoc.jar" />
<arg value="-Dclassifier=javadoc" />
<arg value="-Pgpg" />
<arg value="org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file" />
<arg value="-Durl=${ossrh-staging-repository-url}" />
<arg value="-DrepositoryId=${ossrh-server-id}" />
<arg value="-DpomFile=pom.xml" />
<arg value="-Dfile=@{filedirectory}/@{filename}.@{fileending}" />
<arg value="-Dclassifier=@{classifier}" />
<arg value="-Pgpg" />
</artifact:mvn>
</target>
</sequential>
</macrodef>

<!-- macro for pushing solvers into a Maven repository
(push into the staging area, from there manual publication is required afterwards) -->
<macrodef name="stage-solver-file">
<attribute name="filename"/>
<attribute name="classifier" default="@{filename}"/>
<attribute name="fileending"/>
<attribute name="filedirectory" default="java/runtime-${stage.solver}"/>
<attribute name="filedirectory" default="lib/java/runtime-${stage.solver}"/>
<attribute name="pomFile" default="solvers_maven_conf/maven_${stage.solver}_pom.xml"/>
<sequential>
<artifact:mvn>
<arg value="org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file" />
<arg value="-Durl=${ossrh-staging-repository-url}" />
<arg value="-DrepositoryId=${ossrh-server-id}" />
<arg value="-DpomFile=solvers_maven_conf/maven_${stage.solver}_pom.xml" />
<arg value="-Dfile=lib/@{filedirectory}/@{filename}.@{fileending}" />
<arg value="-Dclassifier=@{filename}" />
<arg value="-DpomFile=@{pomFile}" />
<arg value="-Dfile=@{filedirectory}/@{filename}.@{fileending}" />
<arg value="-Dclassifier=@{classifier}" />
<arg value="-Dpackaging=@{fileending}" />
<arg value="-Dversion=${stage.revision}" />
<arg value="-DgeneratePom=false" />
Expand Down Expand Up @@ -158,4 +144,33 @@ SPDX-License-Identifier: Apache-2.0
<stage-solver-file filename="libcvc4jni" fileending="so"/>
<stage-solver-file filename="libcvc4parser" fileending="so"/>
</target>

<!--
Yices2 consists of two parts:
- we release our JavaSMT-based bindings for Yices2.
- we release our Yices2 itself.
We do currently not track any dependency within Maven, but rely on the developer to provide them,
i.e., by including both packages in a proper JavaSMT deployment.
-->
<target name="stage-javasmt-yices2" depends="build-dependencies, install-contrib"
description="deploy current version of Yices2 to Maven staging repository">
<!-- get revision from dependencies -->
<ivy:artifactproperty name="[artifact].revision" value="[revision]"/>
<property name="stage.solver" value="yices2"/> <!-- <==unused -->
<property name="stage.revision" value="${javasmt-yices2.revision}"/>
<!-- then publish the files -->
<stage-solver-file filename="javasmt-yices2" fileending="jar" classifier=""
pomFile="solvers_maven_conf/maven_javasmt_yices2_pom.xml"/>
<stage-solver-file filename="javasmt-yices2-sources" fileending="jar" classifier="sources"
pomFile="solvers_maven_conf/maven_javasmt_yices2_pom.xml" filedirectory="lib/java-contrib"/>
</target>
<target name="stage-yices2" depends="build-dependencies"
description="deploy current version of Yices2 to Maven staging repository">
<!-- get revision from dependencies -->
<ivy:artifactproperty name="[artifact].revision" value="[revision]"/>
<property name="stage.solver" value="yices2"/>
<property name="stage.revision" value="${libyices2j.revision}"/>
<!-- then publish the file -->
<stage-solver-file filename="libyices2j" fileending="so"/>
</target>
</project>
197 changes: 197 additions & 0 deletions doc/Developers-How-to-Release-into-Ivy.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,197 @@
<!--
This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt

SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>

SPDX-License-Identifier: Apache-2.0
-->

# Release JavaSMT or Solver Binaries to Ivy

Please read the hints on release in the [developer documentation](Developers.md) first.

## Releasing JavaSMT

If you have write permission to the [Ivy Repository][] you can perform the release as follows:

- Symlink the `repository` folder in the JavaSMT to the root of the SVN checkout of the Ivy repository.
- Run the `publish` ANT task and inspect the files for correctness and completeness!
- Manually perform the commit in SVN.


## Releasing Solvers

Before actually releasing a new version of a solver into the public world,
make sure, it is tested sufficiently.
This is one of the most critical steps in JavaSMT development.


### Publishing Princess and SMTInterpol

By default, Java-based solvers are copied over from Maven Central.
Please execute the following in the root directory of the [Ivy Repository][]:

- ant install -Dorganisation=io.github.uuverifiers -Dmodule=princess_2.13 -Drevision=????-??-??
- ant install -Dorganisation=de.uni-freiburg.informatik.ultimate -Dmodule=smtinterpol -Drevision=?.?-???-g???????

Potentially outdated:
For manually uploading a Java-based solver to the [Ivy Repository][],
there are scripts for publishing available at the root of the [Ivy Repository](https://svn.sosy-lab.org/software/ivy).


### Publishing Z3

We prefer to use the official Z3 binaries,
please build from source only if necessary (e.g., in case of an important bugfix).

To publish Z3, download the **Ubuntu 16.04**, **Windows**, and **OSX** binary
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 from the three `bin` directories together into one directory,
and include the sources (we can keep the internal structure of each directory, just copy them above each other).
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:
```
ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION
```
Finally follow the instructions shown in the message at the end.

#### Optional
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:
```
./configure --staticlib --java --git-describe && cd build && make -j 2
```
(Note that additional binaries for other operating systems need to be provided, too.
This step is currently not fully tested from our side.)
Then execute the following command in the JavaSMT directory, where `$Z3_DIR` is the absolute path of the Z3 directory:
```
ant publish-z3 -Dz3.path=$Z3_DIR/build
```
Finally follow the instructions shown in the message at the end.


### Publishing CVC4

We prefer to use our own CVC4 binaries and Java bindings.

To publish CVC4, checkout the [CVC4 repository](https://github.com/kfriedberger/CVC4).
Then execute the following command in the JavaSMT directory,
where `$CVC4_DIR` is the path to the CVC4 directory
and `$CVC4_VERSION` is the version number:
```
ant publish-cvc4 -Dcvc4.path=$CVC4_DIR -Dcvc4.customRev=$CVC4_VERSION
```
Example:
```
ant publish-cvc4 -Dcvc4.path=../CVC4 -Dcvc4.customRev=1.8-prerelease-2019-10-05
```
Finally follow the instructions shown in the message at the end.


### Publishing Boolector

We prefer to use our own Boolector binaries and Java bindings.
Boolector's dependencies, mainly Minisat, requires GCC version 7 and does not yet compile with newer compilers.
We prefer to directly build diretly on Ubuntu 18.04, where gcc-7 is the default compiler.
It should also be possible to set environment varables like CC=gcc-7 on newer systems.

To publish Boolector, checkout the [Boolector repository](https://github.com/Boolector/boolector).
Then execute the following command in the JavaSMT directory,
where `$BTOR_DIR` is the path to the Boolector directory
and `$BTOR_VERSION` is the version number:
```
CC=gcc-7 ant publish-boolector -Dboolector.path=$BTOR_DIR -Dboolector.customRev=$BTOR_VERSION
```
Example:
```
ant publish-boolector -Dboolector.path=../boolector -Dboolector.customRev=3.0.0-2019-11-29
```
Finally follow the instructions shown in the message at the end.


### Publishing (Opti)-MathSAT5

We publish MathSAT for both Linux and Windows systems at once.
The build process can fully be done on a Linux system.

For publishing MathSAT5, you need to use a Linux machine with at least GCC 7.5.0 and x86_64-w64-mingw32-gcc 7.3.
First, [download the (reentrant!) Linux and Windows64 binary release](http://mathsat.fbk.eu/download.html) in the same version, unpack them,
then provide the necessary dependencies (GMP for Linux and MPIR/JDK for Windows) as described in the compilation scripts.
(see `lib/native/source/libmathsat5j/`), and then execute the following command in the JavaSMT directory,
where `$MATHSAT_PATH_LINUX` and `$MATHSAT_PATH_WINDOWS` are the paths to the MathSAT root directory,
and `$MATHSAT_VERSION` is the version number of MathSAT (all-in-one, runtime: less than 5s):
```
ant publish-mathsat \
-Dmathsat.path=$MATHSAT_PATH_LINUX \
-Dgmp.path=$GMP_PATH \
-Dmathsat-windows.path=$MATHSAT_PATH_WINDOWS \
-Dmpir-windows.path=$MPIR_PATH \
-Djdk-windows.path=$JDK_11_PATH \
-Dmathsat.version=$MATHSAT_VERSION
```
Concrete example (`$WD` is a working directory where all dependencies are located):
```
ant publish-mathsat \
-Dmathsat.path=$WD/mathsat-5.6.4-linux-x86_64-reentrant \
-Dgmp.path=$WD/gmp-6.1.2 \
-Dmathsat-windows.path=$WD/mathsat-5.6.4-win64-msvc \
-Dmpir-windows.path=$WD/mpir-2.7.2-win \
-Djdk-windows.path=$WD/jdk-11 \
-Dmathsat.version=5.6.4-debug
```
Finally follow the instructions shown in the message at the end.

A similar procedure applies to [OptiMathSAT](http://optimathsat.disi.unitn.it/) solver,
except that Windows is not yet supported and the publishing command is simpler:
```
ant publish-optimathsat -Dmathsat.path=$OPTIMATHSAT_PATH -Dgmp.path=$GMP_PATH -Dmathsat.version=$OPTIMATHSAT_VERSION
```


### Publishing Yices2

Yices2 consists of two components: the solver binary and the Java components in JavaSMT.
The Java components were splitt from the rest of JavaSMT because of the GPL.

#### Publishing the solver binary for Yices2

Prepare gperf and gmp (required for our own static binary):
```
wget http://ftp.gnu.org/pub/gnu/gperf/gperf-3.1.tar.gz && tar -zxvf gperf-3.1.tar.gz && cd gperf-3.1 && ./configure --enable-cxx --with-pic --disable-shared --enable-fat && make
wget https://gmplib.org/download/gmp/gmp-6.2.0.tar.xz && tar -xvf gmp-6.2.0.tar.xz && cd gmp-6.2.0 && ./configure --enable-cxx --with-pic --disable-shared --enable-fat && make
```

Download and build Yices2 from source:
```
git clone [email protected]:SRI-CSL/yices2.git && cd yices2 && autoconf && ./configure --with-pic-gmp=../gmp-6.2.0/.libs/libgmp.a && make
```

Get the version of Yices2:
```
git describe --tags
```

Publish the solver binary from within JavaSMT (adjust all paths to your system!):
```
ant publish-yices2 -Dyices2.path=../solver/yices2 -Dgmp.path=../solver/gmp-6.2.0 -Dgperf.path=../solver/gperf-3.1 -Dyices2.version=2.6.2-89-g0f77dc4b
```

Afterwards you need to update the version number in `solvers_ivy_conf/ivy_javasmt_yices2.xml` and publish new Java components for Yices2.

#### Publish the Java components for Yices2

Info: There is a small cyclic dependency: JavaSMT itself depends on the Java components of Yices2.

As long as no API was changed and compilation suceeds, simply execute `ant publish-artifacts-yices2`.

If the API was changed, we need to break the dependency cycle for the publication and revert this later:
edit `lib/ivy.xml` and replace the dependency towards `javasmt-yices2` with the dependency towards `javasmt-solver-yices2`
(the line can be copied from `solvers_ivy_conf/ivy_javasmt_yices2.xml`).
Then run `ant publish-artifact-yices2`.
We still need to figure out how to avoid the warning about a dirty repository in that case, e.g. by a temporary commit.

[Ivy Repository]: http://www.sosy-lab.org/ivy/org.sosy_lab/
Loading