Skip to content

Extend Docker images and CI #442

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 16 commits into from
Apr 2, 2025
Merged

Extend Docker images and CI #442

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
3002f02
Inline Sosy-Lab Docker image definitions to get a multi-arch build.
kfriedberger Mar 10, 2025
a96c1d2
Docker: simplify redundant listing of build-docker for different JDK …
kfriedberger Mar 10, 2025
4507db1
remove outdated "dependencies" that should not be used together with …
kfriedberger Mar 10, 2025
ac4d97c
CI and Docker: add script to manually build and push images for multi…
kfriedberger Mar 10, 2025
4e28f07
CI and Docker: try to build Docker images for different architectures…
kfriedberger Mar 10, 2025
2fe1c35
add arm64-based junit test executions.
kfriedberger Mar 10, 2025
5d3c1af
CI: let unit tests for arm64 only execute a smaller subset of tests,
kfriedberger Mar 29, 2025
f2d32fe
CI: next test to build Dockerfile in GitlabCI.
kfriedberger Mar 16, 2025
1a88f53
CI: next test to build Dockerfile in GitlabCI.
kfriedberger Mar 16, 2025
61c7eca
CI: simplify build-step inheritance and formatting
kfriedberger Mar 29, 2025
8ffce60
CI: cleanup steps for unit-tests and docker-builds.
kfriedberger Mar 29, 2025
fe033aa
CI: cleanup steps for unit-tests and docker-builds.
kfriedberger Mar 29, 2025
9626ea5
CI: cleanup inheritance and limit docker-build to weekly schedule.
kfriedberger Mar 29, 2025
fcc3e67
Delete unused build/buildAndPublishDockerImages.sh
kfriedberger Mar 29, 2025
219a71e
increase timelimit for CVC5 tests.
kfriedberger Mar 29, 2025
14c2129
rename method
kfriedberger Apr 1, 2025
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
48 changes: 41 additions & 7 deletions build/build-junit.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,21 +46,21 @@ SPDX-License-Identifier: Apache-2.0
<path refid="classpath"/>
</path>

<delete dir="${junit.dir}"/>
<mkdir dir="${junit.dir}"/>
</target>

<target name="unit-tests" depends="build, load-junit, init-unit-tests" description="Run all JUnit tests">
<delete dir="{junit.dir}"/>
<macrodef name="run-junit-tests">
<sequential>
<junit fork="true" printSummary="true" showOutput="false" failureproperty="junit.failed" timeout="600000">
<assertions><enable/></assertions>
<formatter type="xml"/>
<classpath refid="classpath.junit"/>
<sysproperty key="java.awt.headless" value="true" />
<batchtest fork="true" todir="${junit.dir}">
<fileset dir="${class.dir}">
<include name="**/*Test.*"/>
<exclude name="**/*$*Test.*"/>
</fileset>
<fileset dir="${class.dir}">
<patternset refid="test.sources"/>
</fileset>
</batchtest>
</junit>
<junitreport todir="${junit.dir}">
Expand All @@ -69,6 +69,41 @@ SPDX-License-Identifier: Apache-2.0
</junitreport>
<move file="junit-noframes.html" tofile="JUnit.html"/>
<fail if="junit.failed" message="JUnit tests failed, look at JUnit.html"/>
</sequential>
</macrodef>

<target name="unit-tests-quick" depends="build, load-junit, init-unit-tests"
description="Run a minimal set of JUnit tests that are considered quick">
<!-- A simpler way for specifying quick tests would be an annotation on class or method level.
JUnit 5 might bring such features. However, we still depend on JUnit 4. -->
<patternset id="test.sources">
<include name="**/solvers/bitwuzla/BitwuzlaNativeApiTest.*"/>
<include name="**/solvers/boolector/BoolectorNativeApiTest.*"/>
<include name="**/solvers/cvc4/CVC4NativeAPITest.*"/>
<include name="**/solvers/cvc5/CVC5NativeAPITest.*"/>
<include name="**/solvers/mathsat5/Mathsat5AbstractNativeApiTest.*"/>
<include name="**/solvers/mathsat5/Mathsat5NativeApiTest.*"/>
<include name="**/solvers/mathsat5/Mathsat5OptimizationNativeApiTest.*"/>
<include name="**/solvers/opensmt/OpenSmtNativeAPITest.*"/>
<include name="**/solvers/yices2/Yices2NativeApiTest.*"/>
<include name="**/test/FloatingPointNumberTest.*"/>
<include name="**/test/FormulaManagerTest.*"/>
<include name="**/test/NumeralFormulaManagerTest.*"/>
<include name="**/test/ProverEnvironmentTest.*"/>
<include name="**/test/RationalFormulaManagerTest.*"/>
<include name="**/test/SolverContextFactoryTest.*"/>
<include name="**/test/SolverContextTest.*"/>
</patternset>
<run-junit-tests/>
</target>

<target name="unit-tests" depends="build, load-junit, init-unit-tests"
description="Run all JUnit tests">
<patternset id="test.sources">
<include name="**/*Test.*"/>
<exclude name="**/*$*Test.*"/>
</patternset>
<run-junit-tests/>
</target>

<target name="load-jacoco" depends="resolve-dependencies">
Expand All @@ -78,7 +113,6 @@ SPDX-License-Identifier: Apache-2.0
</target>

<target name="unit-tests-coverage" depends="build, load-junit, load-jacoco, init-unit-tests" description="Run all JUnit tests with coverage report">
<delete dir="{junit.dir}"/>
<jacoco:coverage destfile="${junit.dir}/jacoco.exec" excludes="**/*Test*:**/Dummy*">
<junit fork="true" printSummary="true" showOutput="false" failureproperty="junit.failed" timeout="600000">
<assertions><enable/></assertions>
Expand Down
20 changes: 18 additions & 2 deletions build/gitlab-ci.Dockerfile.jdk-11
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
# an API wrapper for a collection of SMT solvers:
# https://github.com/sosy-lab/java-smt
#
# SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

Expand All @@ -14,6 +14,22 @@
# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 - < build/gitlab-ci.Dockerfile.jdk-11
# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11

FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-11
FROM ubuntu:20.04

ENV DEBIAN_FRONTEND=noninteractive
ENV TZ=UTC

RUN apt-get update && apt-get install -y --no-install-recommends \
ant \
curl \
git \
jq \
openjdk-11-jre-headless \
openjdk-11-jdk-headless \
wget \
&& rm -rf /var/lib/apt/lists/*

ENV LANG C.UTF-8

Comment on lines +17 to +33
Copy link
Contributor

@daniel-raffler daniel-raffler Apr 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are the changes here just temporary due to the java-project-template issue you mentioned? Otherwise, I think that something like FROM --platform=?? registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-11 could be used to pull the image for a specific architecture.

Copy link
Member Author

@kfriedberger kfriedberger Apr 1, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, temporary, until further notice 😄, e.g., until there is one multi-arch Docker image in the registry where we can inherit from.

FROM --platform <ARCH> <TAG> can be used to select one of several architectures from a multi-arch Docker image, but not the other way. See https://docs.docker.com/reference/dockerfile/#from . I do not expect it to work in this case.

RUN apt-get update && apt-get install -y \
libgomp1
20 changes: 18 additions & 2 deletions build/gitlab-ci.Dockerfile.jdk-17
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
# an API wrapper for a collection of SMT solvers:
# https://github.com/sosy-lab/java-smt
#
# SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

Expand All @@ -14,6 +14,22 @@
# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 - < build/gitlab-ci.Dockerfile.jdk-17
# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17

FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-17
FROM ubuntu:20.04

ENV DEBIAN_FRONTEND=noninteractive
ENV TZ=UTC

RUN apt-get update && apt-get install -y --no-install-recommends \
ant \
curl \
git \
jq \
openjdk-17-jre-headless \
openjdk-17-jdk-headless \
wget \
&& rm -rf /var/lib/apt/lists/*

ENV LANG C.UTF-8

RUN apt-get update && apt-get install -y \
libgomp1
19 changes: 17 additions & 2 deletions build/gitlab-ci.Dockerfile.jdk-21
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
# an API wrapper for a collection of SMT solvers:
# https://github.com/sosy-lab/java-smt
#
# SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

Expand All @@ -14,6 +14,21 @@
# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 - < build/gitlab-ci.Dockerfile.jdk-21
# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21

FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-21
FROM ubuntu:20.04

ENV DEBIAN_FRONTEND=noninteractive
ENV TZ=UTC

RUN apt-get update && apt-get install -y --no-install-recommends \
ant \
curl \
git \
jq \
openjdk-21-jdk-headless \
wget \
&& rm -rf /var/lib/apt/lists/*

ENV LANG C.UTF-8

RUN apt-get update && apt-get install -y \
libgomp1
16 changes: 15 additions & 1 deletion build/gitlab-ci.Dockerfile.jdk-23
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,20 @@
# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-23 - < build/gitlab-ci.Dockerfile.jdk-23
# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-23

FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-23
# Older Ubuntu versions currently do not have GLIC_2.34 and Java 23
FROM ubuntu:24.10

ENV DEBIAN_FRONTEND=noninteractive
ENV TZ=UTC

RUN apt-get update && apt-get install -y --no-install-recommends \
ant \
curl \
git \
jq \
openjdk-23-jdk-headless \
wget \
&& rm -rf /var/lib/apt/lists/*

RUN apt-get update && apt-get install -y \
libgomp1
Loading