Move the build environment under package/, behind an entry point

.github/actions/test-package/action.yml

@@ -14,7 +14,7 @@ inputs:
   dockerfile:
     description: 'Hardcode the path of the dockerfile to use.'
     required: false
-    default: .github/workflows/Dockerfile
+    default: package/build-env/Dockerfile
   build-package:
     description: 'Script which builds the given package.'
     required: true

.github/actions/with-docker/action.yml

@@ -25,7 +25,7 @@ inputs:
   dockerfile:
     description: 'Hardcode the path of the dockerfile to use.'
     required: false
-    default: .github/workflows/Dockerfile
+    default: package/build-env/Dockerfile
 runs:
   using: 'composite'
   steps:
@@ -42,9 +42,10 @@ runs:
     run: |
       set -euxo pipefail
 
-      USER=$(id -un)
+      # Ids only, deliberately: the Dockerfile names the account itself.
+      # Passing the runner's account NAME through collides with whatever the
+      # base image already ships -- see the comment on the ARGs it feeds.
       USER_ID=$(id -u)
-      GROUP=$(id -gn)
       GROUP_ID=$(id -g)
 
       docker build ${SUBDIR} --file ${SUBDIR}${DOCKERFILE}            \
@@ -53,14 +54,14 @@ runs:
           --build-arg BASE_DISTRO=${BASE_DISTRO}                      \
           --build-arg LLVM_VERSION=${LLVM_VERSION}                    \
           --build-arg JDK_VERSION=${JDK_VERSION}                      \
-          --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
-          --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID}
+          --build-arg USER_ID=${USER_ID}                              \
+          --build-arg GROUP_ID=${GROUP_ID}
 
       docker run                             \
           --name ${TAG_NAME}                 \
           --rm -it                           \
           --detach                           \
           --workdir /opt/workspace/${SUBDIR} \
-          --user ${USER}:${GROUP}            \
+          --user ${USER_ID}:${GROUP_ID}      \
           -v "$(pwd):/opt/workspace"         \
           runtimeverification/${TAG_NAME}

.github/workflows/Dockerfile → package/build-env/Dockerfile

@@ -45,12 +45,35 @@ ENV LANG en_US.UTF-8
 ENV LANGUAGE en_US:en
 ENV LC_ALL en_US.UTF-8
 
-# The image is built specifically for an environment with this user/group
-ARG USER=github-user
+# The build runs as an account whose uid/gid match the CALLER's, so that files
+# written to the bind-mounted checkout are owned by whoever invoked the build.
+# Only the ids matter for that; the names are ours to pick, and picking them
+# ourselves is what keeps this working on an arbitrary machine.
+#
+# Passing the caller's names through, which is what this used to do, collides
+# with whatever the base image already has: ubuntu:noble ships an `ubuntu`
+# account at uid/gid 1000, and `users` (gid 100) is the primary group of many
+# developer accounts. Either makes groupadd/useradd fail, several minutes into
+# the build, with a message that does not mention the build args.
+#
+# -o permits the ids to be shared with an existing account rather than trying
+# to delete one -- deleting a system group that something else already uses
+# fails just as hard.
+ARG USER=builder
 ARG GROUP=$USER
 ARG USER_ID=1000
 ARG GROUP_ID=$USER_ID
-RUN groupadd -g $GROUP_ID $GROUP && useradd -m -u $USER_ID -s /bin/sh -g $GROUP $USER
+RUN groupadd -o -g $GROUP_ID $GROUP && useradd -o -m -u $USER_ID -s /bin/sh -g $GROUP $USER
+
+# dpkg-buildpackage writes its output to the PARENT of the directory it builds
+# in, so the build has to run somewhere with a writable parent. Create that
+# parent here, owned by the build user; package/build-env/build-deb then mounts the
+# checkout at /opt/workspace/source rather than at /opt/workspace itself.
+#
+# Mounting the checkout directly at /opt/workspace makes the parent `/`, which
+# a non-root user cannot write, and the failure surfaces from inside
+# dpkg-buildpackage rather than from the mount that caused it.
+RUN mkdir -p /opt/workspace && chown $USER_ID:$GROUP_ID /opt/workspace
 
 USER $USER:$GROUP
 

package/build-env/README.md

@@ -0,0 +1,69 @@
+# The build environment
+
+`package/debian/` holds the *recipe* for the Debian package. This directory holds the
+*environment* it is built in, and the entry points that drive it.
+
+```
+package/build-env/Dockerfile    the build environment (clang, cmake, maven, JDK, lit)
+package/build-env/build-deb     build the .deb for one Ubuntu release
+package/build-env/test-deb      install that .deb into a clean image, as root
+package/build-env/common.sh     the distro table both scripts read
+```
+
+```
+package/build-env/build-deb noble
+package/build-env/test-deb  noble
+```
+
+Both take an optional second argument naming the `.deb`; the default is
+`k-llvm-backend_amd64_ubuntu_<distro>.deb`, left at the root of the checkout. They can be run
+from any directory — they `cd` to the checkout root themselves, because
+`package/debian/build-package` assumes it. They use `podman` if it is installed and `docker`
+otherwise; `CONTAINER_ENGINE` overrides that.
+
+Which LLVM version goes with which Ubuntu release lives in `common.sh` and nowhere else, so
+adding a release is one edit here plus one in the CI matrix.
+
+`build-package` *moves* files out of `package/debian/` into a top-level `debian/`, so a second
+`build-deb` run needs a clean tree. That is pre-existing behaviour, noted here because it is
+surprising the first time.
+
+## Why it lives here
+
+It used to be `.github/workflows/Dockerfile`, invoked by two composite actions under
+`.github/actions/`. That made the environment reachable only from a GitHub workflow, and the
+knowledge of *how to invoke it* — which LLVM version pairs with which Ubuntu release, which
+build args the Dockerfile needs, how to map the calling user into the container, where to
+mount the checkout — was not written down as anything executable. It was spread across two
+action definitions and then copied, imperfectly, into whatever else needed to build a deb.
+
+Moving CI to the internal forge deletes `.github/` entirely. Rather than move the same
+arrangement sideways, the environment moved next to the recipe it builds, behind two scripts
+that a forge workflow, the release repository, and a developer's shell can all call the same
+way.
+
+## Two things that are easy to get wrong
+
+**The checkout mounts at `/opt/workspace/source`, not at `/opt/workspace`.**
+`dpkg-buildpackage` writes the `.deb` to the *parent* of the directory it builds in, and
+`package/debian/build-package` then moves it back. Mount the checkout at `/opt/workspace` and
+that parent is `/`, which the non-root build user cannot write — the build then fails from
+inside `dpkg-buildpackage`, naming neither the mount nor the reason. The `Dockerfile` creates
+`/opt/workspace` owned by the build user so that the parent is writable.
+
+**The package must be tested somewhere other than the build environment.** That image has
+every build dependency already installed, so a missing or wrong entry in `debian/control`
+would install cleanly there and fail only for a user. `test-deb` uses a bare
+`ubuntu:<distro>` for that reason, and needs root, which the build environment does not have.
+
+## The account inside the image
+
+The build runs as an account whose uid/gid match the caller's, so files written to the
+bind-mounted checkout come back owned by whoever ran the build. Only the *ids* matter for
+that, so the `Dockerfile` names the account itself (`builder`) and callers pass ids alone.
+
+Passing the caller's account *name* through — which is what this used to do — collides with
+whatever the base image already ships. `ubuntu:noble` has an `ubuntu` account at uid/gid 1000,
+and `users` (gid 100) is the primary group of many developer accounts; either one makes
+`useradd` fail several minutes into the build, with a message that never mentions a build arg.
+`-o` lets the ids be shared rather than deleting a system account that something else uses.

package/build-env/build-deb

@@ -0,0 +1,77 @@
+#!/usr/bin/env bash
+
+# Build the k-llvm-backend Debian package for one Ubuntu release.
+#
+# WHY THIS EXISTS
+#
+# The build RECIPE (package/debian/build-package) has always lived under
+# package/, versioned with the source it builds. The build ENVIRONMENT did not:
+# it was .github/workflows/Dockerfile, reachable only from a GitHub workflow.
+# And the knowledge of how to DRIVE it -- which LLVM version pairs with which
+# Ubuntu release, which build args the Dockerfile needs, how to map the calling
+# user into the container, where to mount the checkout -- was written down
+# nowhere executable, only spread across two composite actions.
+#
+# Moving CI to the internal forge deletes .github/ outright. This is the durable
+# replacement: one entry point that owns the environment, callable from a forge
+# workflow, from the release repository, or from a developer's shell.
+#
+# Usage:  package/build-env/build-deb <distro> [output.deb]
+#
+# Runnable from any directory. The deb is left at the root of the checkout.
+# Note that package/debian/build-package MOVES files out of package/debian/, so
+# a second run needs a clean tree.
+
+set -euo pipefail
+
+cd "$(dirname "${BASH_SOURCE[0]}")/../.."
+# shellcheck source=package/build-env/common.sh
+. package/build-env/common.sh
+
+distro="${1:-}"
+require_distro "${distro}"
+pkg_name="${2:-$(default_pkg_name "${distro}")}"
+
+llvm_version=$(llvm_version_for "${distro}")
+
+# The Dockerfile declares JDK_VERSION with NO default, so omitting it installs
+# the package `openjdk--jdk` and the image build fails several minutes in with
+# an apt error that does not mention the build arg.
+jdk_version="${JDK_VERSION:-17}"
+
+engine=$(container_engine)
+tag="llvm-backend-build:${distro}"
+
+echo "--- Build environment: ${distro}, llvm-${llvm_version}, jdk-${jdk_version} ---"
+"${engine}" build . \
+    --file package/build-env/Dockerfile \
+    --build-arg 'BASE_OS=ubuntu' \
+    --build-arg "BASE_DISTRO=${distro}" \
+    --build-arg "LLVM_VERSION=${llvm_version}" \
+    --build-arg "JDK_VERSION=${jdk_version}" \
+    --build-arg "USER_ID=$(id -u)" \
+    --build-arg "GROUP_ID=$(id -g)" \
+    --tag "${tag}"
+
+# Rootless podman maps the calling uid to a different uid inside the container
+# by default, which leaves the bind mount unwritable by the image's user.
+# keep-id maps it through. Docker has no equivalent and takes --user instead.
+run_args=()
+case "${engine##*/}" in
+    podman) run_args+=(--userns=keep-id) ;;
+    *)      run_args+=(--user "$(id -u):$(id -g)") ;;
+esac
+
+# Mount at /opt/workspace/SOURCE, not at /opt/workspace. dpkg-buildpackage
+# writes the .deb to the parent of the directory it builds in, and build-package
+# then moves it back; with the checkout mounted at /opt/workspace that parent is
+# `/`, which the build user cannot write. The Dockerfile creates /opt/workspace
+# owned by the build user for exactly this.
+echo "--- Building ${pkg_name} ---"
+"${engine}" run --rm "${run_args[@]}" \
+    --volume "${PWD}:/opt/workspace/source" \
+    --workdir /opt/workspace/source \
+    "${tag}" \
+    package/debian/build-package "${distro}" "${pkg_name}"
+
+echo "--- Built ${pkg_name} ---"

package/build-env/common.sh

@@ -0,0 +1,47 @@
+# Shared by build-deb and test-deb. Source it; it is not executable.
+
+# The one table. The LLVM version is a property of the Ubuntu release, not a
+# free choice: each release carries one clang/lld/llvm-tools set that the
+# package is built and tested against. Adding a release means editing here and
+# in the CI matrix, and nowhere else.
+llvm_version_for() {
+    case "${1}" in
+        jammy) echo 15 ;;
+        noble) echo 17 ;;
+        *)     return 1 ;;
+    esac
+}
+
+SUPPORTED_DISTROS='jammy noble'
+
+# Both scripts take a distro as their first argument and must agree on which
+# ones exist -- a list kept in two places is a list that drifts.
+require_distro() {
+    if [ -z "${1}" ]; then
+        echo "${0##*/}: usage: ${0##*/} <${SUPPORTED_DISTROS// /|}> [package.deb]" >&2
+        exit 2
+    fi
+    if ! llvm_version_for "${1}" > /dev/null; then
+        echo "${0##*/}: unknown distro '${1}' (expected: ${SUPPORTED_DISTROS})" >&2
+        exit 2
+    fi
+}
+
+default_pkg_name() {
+    echo "k-llvm-backend_amd64_ubuntu_${1}.deb"
+}
+
+# podman is what RV uses; docker is accepted so this still runs on a machine
+# that only has that. CONTAINER_ENGINE overrides both.
+container_engine() {
+    if [ -n "${CONTAINER_ENGINE:-}" ]; then
+        echo "${CONTAINER_ENGINE}"
+    elif command -v podman > /dev/null 2>&1; then
+        echo podman
+    elif command -v docker > /dev/null 2>&1; then
+        echo docker
+    else
+        echo "${0##*/}: no container engine found (looked for podman, docker)" >&2
+        exit 1
+    fi
+}

package/build-env/test-deb

@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+
+# Install a built package into a clean Ubuntu image, as root.
+#
+# Separate from build-deb for a reason worth stating: the test MUST NOT run in
+# the build environment. That image already has every build dependency
+# installed, so a package with a missing or wrong entry in debian/control would
+# install cleanly there and fail only for a user. It also ends with a non-root
+# USER, and apt-get needs root.
+#
+# So this uses a bare ubuntu:<distro> -- nothing but the base image and the deb.
+#
+# Usage:  package/build-env/test-deb <distro> [package.deb]
+#
+# Runnable from any directory, after build-deb.
+
+set -euo pipefail
+
+cd "$(dirname "${BASH_SOURCE[0]}")/../.."
+# shellcheck source=package/build-env/common.sh
+. package/build-env/common.sh
+
+distro="${1:-}"
+require_distro "${distro}"
+pkg_name="${2:-$(default_pkg_name "${distro}")}"
+
+if [ ! -f "${pkg_name}" ]; then
+    echo "test-deb: ${pkg_name} not found -- run 'package/build-env/build-deb ${distro}' first" >&2
+    exit 1
+fi
+
+engine=$(container_engine)
+
+echo "--- Installing ${pkg_name} into a clean ubuntu:${distro} ---"
+"${engine}" run --rm \
+    --volume "${PWD}:/opt/workspace/source" \
+    --workdir /opt/workspace/source \
+    "docker.io/library/ubuntu:${distro}" \
+    package/debian/test-package "${pkg_name}"
+
+echo "--- ${pkg_name} installs cleanly ---"