From 7f276fb89d659ad86bf2b862f4de4ed3c362d3d6 Mon Sep 17 00:00:00 2001 From: Jan Sucan Date: Fri, 26 Apr 2024 08:55:12 +0200 Subject: devel_tools: Add CI Docker image --- devel_tools/ci_container/Dockerfile | 37 +++++++++++++++++++++++++ devel_tools/ci_container/build.sh | 3 ++ devel_tools/ci_container/entry.sh | 55 +++++++++++++++++++++++++++++++++++++ devel_tools/ci_container/run.sh | 7 +++++ 4 files changed, 102 insertions(+) create mode 100644 devel_tools/ci_container/Dockerfile create mode 100644 devel_tools/ci_container/build.sh create mode 100644 devel_tools/ci_container/entry.sh create mode 100644 devel_tools/ci_container/run.sh (limited to 'devel_tools/ci_container') diff --git a/devel_tools/ci_container/Dockerfile b/devel_tools/ci_container/Dockerfile new file mode 100644 index 0000000..3cca866 --- /dev/null +++ b/devel_tools/ci_container/Dockerfile @@ -0,0 +1,37 @@ +FROM ubuntu:22.04 + +RUN <&2 + exit 1 +fi + +UID=$1 +GID=$2 +USER_NAME=new-user +GROUP_NAME=new-group +shift 2 + +if ! getent passwd $UID >/dev/null; then + # The UID does not exist, create it + useradd -m -u $UID $USER_NAME +else + USER_NAME=$(id -n -u $UID) +fi + +if ! getent group $GID >/dev/null; then + # The GID does not exist, create it + groupadd -g $GID $GROUP_NAME +else + GROUP_NAME=$(getent group $GID | cut -d: -f1) +fi + +# Make sure the group is the user's primary group +usermod -g $GROUP_NAME $USER_NAME + +# Check that the user has expected UID and GID +ACTUAL_UID=$(su -c 'id -u' $USER_NAME) +if [ $ACTUAL_UID -ne $UID ]; then + echo "Error: Actual UID $ACTUAL_UID != $UID" + exit 1 +fi + +ACTUAL_GID=$(su -c 'id -g' $USER_NAME) +if [ $ACTUAL_GID -ne $GID ]; then + echo "Error: Actual GID $ACTUAL_GID != $GID" + exit 1 +fi + +if [ ! -e /.cache ]; then + # Needed for running pre-commit + mkdir /.cache + chown $USER_NAME: /.cache +fi + +su -c "$*" $USER_NAME diff --git a/devel_tools/ci_container/run.sh b/devel_tools/ci_container/run.sh new file mode 100644 index 0000000..ea01ee1 --- /dev/null +++ b/devel_tools/ci_container/run.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +USER_UID=$(id -u) +USER_GID=$(id -g) + +# Intended to run from root directory of the project +docker run -v .:/diff-dd ghcr.io/jansucan/diff-dd-ci $USER_UID $USER_GID "$@" -- cgit v1.2.3