Update mkimage

[chadbrewbaker]

Pin build to x86 since it is broken on ARM. Required for M1 users.

[chadbrewbaker]

Looks like there is a build error, looking into it.

Making docker image rvt_solvers:latest using Dockerfile                                                                                                            
../mkimage: line 20: [: -v: unary operator expected
[+] Building 0.4s (6/17)                                                                                                                                           
 => [internal] load build definition from Dockerfile                                                                                                          0.0s
 => => transferring dockerfile: 1.76kB                                                                                                                        0.0s
 => [internal] load .dockerignore                                                                                                                             0.0s
 => => transferring context: 2B                                                                                                                               0.0s
 => [internal] load metadata for docker.io/library/rvt_base:latest                                                                                            0.0s
 => [ 1/13] FROM docker.io/library/rvt_base:latest                                                                                                            0.0s
 => importing cache manifest from rvt_solvers:latest                                                                                                          0.0s
 => ERROR [ 2/13] RUN mkdir /home/root/minisat                                                                                                                0.2s
------
 > [ 2/13] RUN mkdir /home/root/minisat:
#4 0.184 /usr/bin/mkdir: cannot create directory '/home/root/minisat': No such file or directory

[chadbrewbaker]

Apparently /home/root didn't exist. Spammed a mkdir -p /home/root, crossing fingers.

[alastairreid]

Brilliant, thanks for this!

[chadbrewbaker]

Um, it doesn't work yet, why I pulled the PR. First issue is you need to set up a non-root user under Ubuntu or else change the paths on /root/ vs /home/root. Second issue was a lot of compiler errors in Rust. Setting "-C codegen-units=1" fixed the termcolor error, but there was another memory out of bounds issue on rust demangle.

For now running https://mac.getutm.app/gallery/ubuntu-20-04 (rebuilt as x86) might be the best option for M1 users.

[alastairreid]

I'm not sure what is going on with /root vs /home/root - the docker building step should not be doing anything with either of those directories. Instead, everything should be built inside /home/${USERNAME} where ${USERNAME} is your account name. So if your login was 'chad', it should all be in /home/chad In case this is going wrong, the key bits of code that do this are:

docker/mkimage

# The default user for a Docker container has uid 0 (root). To avoid creating
# root-owned files in the build directory we tell Docker to use the current user
# ID, if known.
# See
# https://github.com/googleapis/google-cloud-cpp/blob/a186208b79d900b4ec71c6f9df3acf7638f01dc6/ci/kokoro/docker/build.sh#L147-L152
readonly DOCKER_UID="${UID:-0}"
readonly DOCKER_GID="$(id -g)"
readonly DOCKER_USER="${USER:-root}"

and docker/base/Dockerfile

# Placeholder args that are expected to be passed in at image build time.
# See https://code.visualstudio.com/docs/remote/containers-advanced#_creating-a-nonroot-user
ARG USERNAME=user-name-goes-here
ARG USER_UID=1000
ARG USER_GID=${USER_UID}
ENV USER_HOME=/home/${USERNAME}

# Create the specified user and group and add them to sudoers list
#
# Ignore errors if the user or group already exist (it should only happen if the image is being
# built as root, which happens on GCB).
RUN (groupadd --gid=${USER_GID} ${USERNAME} || true) \
  && (useradd --shell=/bin/bash --uid=${USER_UID} --gid=${USER_GID} --create-home ${USERNAME} || true) \
  && echo "${USERNAME}  ALL=(ALL) NOPASSWD: ALL" >> /etc/sudoers

And then various docker/*/Dockerfile scripts do things like this at the start

USER ${USERNAME}
WORKDIR ${USER_HOME}

[alastairreid]

I'm guessing that the problem you are hitting is due to the way we (mis?)use docker.

Our process of building a docker container is intended to create a container that is customized for one specific user (usually the person who built it).

We haven't tried to make a more general/flexible container that can be shared with others – we're trying to strike a balance between having something that is easy for us to use when developing RVT and something that is easy to install on a range of platforms.

We also have not put much effort into creating small images that are suitable for sharing with others. (eg by copying the pattern in the KLEE Dockerfile of building all the binaries in one docker image and then COPYing the binaries over. Instead, our docker images include full source, intermediate files, etc. so that it is easy to modify them and rebuild them as part of developing RVT.

This seemed like a good choice when we started because it forced us to use Docker on a day to day basis - which made it less likely that we would break Docker. But, the downside is that we don't have something small and convenient for others to use. Thoughts (and pull requests!) welcome on how to turn what we have into small, lightweight containers.

[chadbrewbaker]

The M1 is macOS zsh by default, so it is probably passing environment information differently than Ubuntu/bash.

In other projects I set up a "builder" user in the base image that is added to the sudoers file. I'll resubmit when I figure out the rest of the Rust compile errors.