This image is available on Docker Hub under atwalter/acl2 and on the GitHub Container Registry under mister-walter/acl2.
Be aware that the prebuilt Docker image is known to have issues on non-Intel macOS machines. It will work correctly if the image is rebuilt from scratch on an M1/M2 machine.
The jq command-line tool bust be installed to use the provided Makefile to build an ACL2 Docker image. This tool is used to get the latest commit hash for the ACL2 repo from Github.
To enable reproducible builds, reduce image size, image build time, and download bandwidth during a build, the Dockerfile expects that it is provided a ACL2_REPO_LATEST_COMMIT build argument. This argument must be set to a URL-safe string corresponding to a commit or tag format that Github understands. I have tested this with full commit hashes and short commit hashes (e.g. the first 8 characters of the full commit hash). As suggested above, the build make target will use Github's API to determine the commit hash for the latest commit to the ACL2 repo and pass that to Docker when building an image.
By default, certification is done with 4 parallel tasks. This can be changed by overriding the ACL2_CERTIFY_OPTS build argument. (i.e. using docker build --build-arg ACL2_CERTIFY_OPTS="-j 2")
By default, the "basic" book selection is certified. This can be changed by overriding the ACL2_CERTIFY_TARGETS build argument. Multiple targets can be provided to this argument if desired.
To update the Gradescope image, one should update the ACL2_COMMIT value in the make-gradescope.sh script to be the Git hash of the appropriate commit in the ACL2 repo. IMAGE_VERSION should also be modified to be some label appropriate for the semester.
Currently docker-slim is the base image used because this osicat bug causes the ACL2 build to fail due to Alpine Linux's use of musl instead of glibc for its libc implementation.