certifying copy.lisp

[riya-avronna]

when I try building the docker image with the following modifications:

ARG ACL2_COMMIT=HEAD
ENV ACL2_SNAPSHOT_INFO="Git commit hash: ${ACL2_COMMIT}"
ARG ACL2_BUILD_OPTS=""
ARG ACL2_CERTIFY_OPTS="-j 8 all"
ARG ACL2_CERTIFY_TARGETS="all"
ENV CERT_PL_RM_OUTFILES="1"

I get the following error message:

1319.8    | 
1319.8    | 
1319.8    | ACL2 Error in COPY-FILE:  Expected copy-file to fail to copy to /root.
1319.8    | 
1319.8    | 
1319.8    | 
1319.8    | ACL2 Error in ( MAKE-EVENT (B* ...)):  Error in MAKE-EVENT from expansion
1319.8    | of:
1319.8    |   (B*
1319.8    |    ((-
1319.8    |      (CW
1319.8    |       "Test: primitive copy-file to /root where we should have no permission.~%"))
1319.8    |     ((MV ERR STATE)
1319.8    |      (COPY-FILE "./copy.lisp" "/root/foo"))
1319.8    |     ((UNLESS ERR)
1319.8    |      (ER SOFT 'COPY-FILE
1319.8    |          "Expected copy-file to fail to copy to /root.")))
1319.8    |    (CW "Successfully got error: ~@0" ERR)
1319.8    |    (VALUE '(VALUE-TRIPLE :SUCCESS)))
1319.8    | 
1319.8    | 
1319.8    | 
1319.8    | Summary
1319.8    | Form:  ( MAKE-EVENT (B* ...))
1319.8    | Rules: NIL
1319.8    | Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
1319.8    | 
1319.8    | ACL2 Error [Failure] in ( MAKE-EVENT (B* ...)):  See :DOC failure.
1319.8    | 
1319.8    | ******** FAILED ********

I'm assuming other people have had the same issue -- because you'd require oslib in order to attempt the hardware verification tutorial in the SV book. How do people typically go around this -- simply certifying the books in another directory before copying stuff over/creating another user?