Skip to content

Conversation

@kfriedberger
Copy link
Member

@kfriedberger kfriedberger commented Mar 2, 2025

With the support of more architectures we should also extend our test-coverage for those architectures.
This PR provides several smaller steps towards this:

  • we add a new ant-based test-step that is smaller, faster, and checks only general solver features, like loading/closing a context or prover, and creating formula managers,
  • we provide the initial technical foundation for aarm64-based tests, i.e., a docker image that is pushed into Gitlab registry and is used for tests.

Screenshot of the pipeline:

  • left column: building Docker image for x64 and arm64 (will only run when scheduled, i.e., once per week)
  • right column: unit-tests on x64 (full tests) and arm64 (quick tests)
    image

This PR violates the rule to reuse SoSy-Lab common project files for building and testing applications and libraries. However, this is due to the lack of support for multiple architectures from the common project template. We opened an issue there: https://gitlab.com/sosy-lab/software/java-project-template/-/issues/7 and aim for a merge of scripts into the common project template.

@kfriedberger kfriedberger force-pushed the feat/docker-images branch 4 times, most recently from 56a7217 to 8771eab Compare March 10, 2025 13:00
@kfriedberger kfriedberger force-pushed the feat/docker-images branch 7 times, most recently from 4f97f8f to b0b890f Compare March 16, 2025 13:40
@kfriedberger kfriedberger marked this pull request as ready for review March 29, 2025 13:40
Copy link
Contributor

@daniel-raffler daniel-raffler left a comment

Choose a reason for hiding this comment

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

We might want to wait for feedback on the java-project-template issue. Otherwise this looks good to me!

Comment on lines +17 to +33
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

Copy link
Contributor

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

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.

@kfriedberger
Copy link
Member Author

We might want to wait for feedback on the java-project-template issue. Otherwise this looks good to me!

I am unsure who will work on issues for java-project-template and when. JavaSMT is short for tests on arm64 now.

@kfriedberger kfriedberger merged commit 72ad803 into master Apr 2, 2025
1 of 3 checks passed
@kfriedberger kfriedberger deleted the feat/docker-images branch April 2, 2025 18:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants