sel4 / sel4-camkes-l4v-dockerfiles Goto Github PK
View Code? Open in Web Editor NEWDockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.
Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.
This module does not work on MacOS the date command has different flags than Linux.
:; make user
# Figure out if any trustworthy systems docker images are potentially too old
date: illegal option -- -
usage: date [-jnRu] [-d dst] [-r seconds] [-t west] [-v[+|-]val[ymwdHMS]] ...
[-f fmt date | [[[mm]dd]HH]MM[[cc]yy][.ss]] [+format]
/bin/sh: ( 1587977226 - ) / (60*60*24) : syntax error: operand expected (error token is ") / (60*60*24) ")
make: *** [run_checks] Error 127
The linter complains about unrelated scripts in PRs.
Investigate if we can pass a list of changed files instead.
Follow-up from seL4/seL4#879
The Debinad/Ubuntu releases do not have the latest version, but using it would force us to improve RISC-V spec compliance.
It seems the docker container does not have the Python module "sh". I'm getting this error when trying to initialize them:
Traceback (most recent call last):
File "../sel4-tutorials-manifest/init", line 16, in <module>
import common
File "/host/sel4-tutorials/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module>
import sh
ImportError: No module named sh
installing it manually fixed it, but this just causes more errors due to missing packages. Seem this should become part of the general container setup: (see also http://sel4.systems/pipermail/devel/2018-October/002222.html):
pip install sh enum34 pyyaml
Make user exits with error 6 and prints
scripts/utils/check_for_old_docker_imgs.sh
docker build --force-rm=true \
--build-arg=USER_BASE_IMG=trustworthysystems/camkes \
-f dockerfiles/extras.dockerfile \
-t extras \
.
Sending build context to Docker daemon 82.94kB
Step 1/3 : ARG USER_BASE_IMG=trustworthysystems/sel4
Step 2/3 : FROM $USER_BASE_IMG
---> a33752e29215
Step 3/3 : RUN apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo
---> Using cache
---> 02560e099951
Successfully built 02560e099951
Successfully tagged extras:latest
docker build --force-rm=true \
--build-arg=EXTRAS_IMG=extras \
--build-arg=UNAME=srinivasa \
--build-arg=UID=1000 \
--build-arg=GID=985 \
--build-arg=GROUP=users \
-f dockerfiles/user.dockerfile \
-t user_img-srinivasa .
Sending build context to Docker daemon 82.94kB
Step 1/9 : ARG EXTRAS_IMG=extras
Step 2/9 : FROM $EXTRAS_IMG
---> 02560e099951
Step 3/9 : ARG UID
---> Using cache
---> 2f4f87ecb885
Step 4/9 : ARG UNAME
---> Using cache
---> 5cc6b37eee99
Step 5/9 : ARG GID
---> Using cache
---> ecc8b0ca7b71
Step 6/9 : ARG GROUP
---> Using cache
---> 7123a57c7bd5
Step 7/9 : RUN groupadd -fg ${GID} ${GROUP} && useradd -u ${UID} -g ${GID} ${UNAME} && adduser ${UNAME} sudo && passwd -d ${UNAME} && echo 'Defaults lecture_file = /etc/sudoers.lecture' >> /etc/sudoers && echo 'Defaults lecture = always' >> /etc/sudoers && echo '##################### Warning! #####################################' > /etc/sudoers.lecture && echo 'This is an ephemeral docker container! You can do things to it using' >> /etc/sudoers.lecture && echo 'sudo, but when you exit, changes made outside of the /host directory' >> /etc/sudoers.lecture && echo 'will be lost.' >> /etc/sudoers.lecture && echo 'If you want your changes to be permanent, add them to the ' >> /etc/sudoers.lecture && echo ' extras.dockerfile' >> /etc/sudoers.lecture && echo 'in the seL4-CAmkES-L4v dockerfiles repo.' >> /etc/sudoers.lecture && echo '####################################################################' >> /etc/sudoers.lecture && echo '' >> /etc/sudoers.lecture && mkdir /home/${UNAME} && echo 'echo "___ "' >> /home/${UNAME}/.bashrc && echo 'echo " | _ _ |_ _ _ |_ |_ "' >> /home/${UNAME}/.bashrc && echo 'echo " | | |_| _) |_ \)/ (_) | |_ | ) \/ "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo " __ "' >> /home/${UNAME}/.bashrc && echo 'echo "(_ _ |_ _ _ _ "' >> /home/${UNAME}/.bashrc && echo 'echo "__) \/ _) |_ (- ||| _) "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo "Hello, welcome to the sel4/CAmkES/L4v docker build environment"' >> /home/${UNAME}/.bashrc && grep export /root/.bashrc >> /home/${UNAME}/.bashrc && echo 'export PATH=/scripts/repo:$PATH' >> /home/${UNAME}/.bashrc && echo 'cd /host' >> /home/${UNAME}/.bashrc && mkdir -p /isabelle && chown -R ${UNAME}:${GROUP} /isabelle && ln -s /isabelle /home/${UNAME}/.isabelle && chown -R ${UNAME}:${GROUP} /home/${UNAME} && chmod -R ug+rw /home/${UNAME}
---> Running in d44c5439c0ea
useradd: group '985' does not exist
Removing intermediate container d44c5439c0ea
The command '/bin/sh -c groupadd -fg ${GID} ${GROUP} && useradd -u ${UID} -g ${GID} ${UNAME} && adduser ${UNAME} sudo && passwd -d ${UNAME} && echo 'Defaults lecture_file = /etc/sudoers.lecture' >> /etc/sudoers && echo 'Defaults lecture = always' >> /etc/sudoers && echo '##################### Warning! #####################################' > /etc/sudoers.lecture && echo 'This is an ephemeral docker container! You can do things to it using' >> /etc/sudoers.lecture && echo 'sudo, but when you exit, changes made outside of the /host directory' >> /etc/sudoers.lecture && echo 'will be lost.' >> /etc/sudoers.lecture && echo 'If you want your changes to be permanent, add them to the ' >> /etc/sudoers.lecture && echo ' extras.dockerfile' >> /etc/sudoers.lecture && echo 'in the seL4-CAmkES-L4v dockerfiles repo.' >> /etc/sudoers.lecture && echo '####################################################################' >> /etc/sudoers.lecture && echo '' >> /etc/sudoers.lecture && mkdir /home/${UNAME} && echo 'echo "___ "' >> /home/${UNAME}/.bashrc && echo 'echo " | _ _ |_ _ _ |_ |_ "' >> /home/${UNAME}/.bashrc && echo 'echo " | | |_| _) |_ \)/ (_) | |_ | ) \/ "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo " __ "' >> /home/${UNAME}/.bashrc && echo 'echo "(_ _ |_ _ _ _ "' >> /home/${UNAME}/.bashrc && echo 'echo "__) \/ _) |_ (- ||| _) "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo "Hello, welcome to the sel4/CAmkES/L4v docker build environment"' >> /home/${UNAME}/.bashrc && grep export /root/.bashrc >> /home/${UNAME}/.bashrc && echo 'export PATH=/scripts/repo:$PATH' >> /home/${UNAME}/.bashrc && echo 'cd /host' >> /home/${UNAME}/.bashrc && mkdir -p /isabelle && chown -R ${UNAME}:${GROUP} /isabelle && ln -s /isabelle /home/${UNAME}/.isabelle && chown -R ${UNAME}:${GROUP} /home/${UNAME} && chmod -R ug+rw /home/${UNAME}' returned a non-zero code: 6
make: *** [Makefile:182: build_user] Error 6
It says useradd:group 985 does not exist eventhough groupadd is there before it
Instead of mounting the localtime file, pass the TZ
variable to Docker.
This may work on Linux as well.
--hostname in-container \
--rm \
$(EXTRA_DOCKER_RUN_ARGS) \
-v $(HOST_DIR):/host:z \
-v $(DOCKER_VOLUME_HOME):/home/$(shell whoami) \
- -v /etc/localtime:/etc/localtime:ro \
+ -e TZ=`ls -la /etc/localtime | cut -d/ -f8-9` \
$(USER_IMG) $(EXEC)
The cut
works on my system, but 8-9 is arbitrary, maybe
better written in awk as ls -la /etc/localtime | awk -F '/' '{ printf "%s/%s\n", $(NF - 1), $NF }'
The build for Cogent is now failing and Cogent is no longer under active development.
If the TSC agrees P propose to remove the Cogent build from the docker containers and remove the Cogent examples from the repos where they occur and/or archive where appropriate.
The Dockerfiles are currently based on Debian Bullseye, which is the old stable release.
I'd suggest providing an alternate branch for trixie (the release that is due this year) to be ready for it when it comes.
Then we can (finally) get rid of python 2.
Hi,
When l4v/run_tests is run, the test named HaskellKernel fails.
This is due to cabal not being installed, according to the test log.
Indeed, ghc and cabal install section are commented out in l4v.dockerfile.
When uncommented, ghc install succeeds but cabal install fails.
Is this something you also experiment and is there a way to fix it?
Thank you very much in advance.
Best regards,
Paolo Crisafulli
The uncompressed disk size of the l4v docker container is currently 17.8GB -- this is after several attempts at size reduction (was temporarily around 20GB).
For interactive use, this is large, but otherwise perfectly fine. For GitHub use, it is too much, because the disk quota for a GitHub runner is 14GB. That means just pulling and extracting the image will make the job run out of disk space.
We could try to produce a l4v-slim
base image that is missing more Isabelle components and doesn't have the Haskell stack
cache set up. It could potentially also be missing some other packages, although pretty much all of them are required at some point for l4v
to work.
got this when trying to run make user on mac:
groupadd: group 'staff' already exists
full output:
~/work/seL4-CAmkES-L4v-dockerfiles (master)$ make user
scripts/utils/check_for_old_docker_imgs.sh
WARNING: Unable to check if your trustworthysystems docker images are getting a bit old!
The date command did not behave as expected. Skipping the check.
docker build --force-rm=true
--build-arg=USER_BASE_IMG=trustworthysystems/camkes
-f dockerfiles/extras.dockerfile
-t extras
.
Sending build context to Docker daemon 79.87kB
Step 1/3 : ARG USER_BASE_IMG=trustworthysystems/sel4
Step 2/3 : FROM $USER_BASE_IMG
---> 63930b6612d7
Step 3/3 : RUN apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo
---> Using cache
---> 84a2f86c12ab
Successfully built 84a2f86c12ab
Successfully tagged extras:latest
docker build --force-rm=true
--build-arg=EXTRAS_IMG=extras
--build-arg=UNAME=arthurmorgan
--build-arg=UID=501
--build-arg=GID=20
--build-arg=GROUP=staff
-f dockerfiles/user.dockerfile
-t user_img-arthurmorgan .
Sending build context to Docker daemon 79.87kB
Step 1/9 : ARG EXTRAS_IMG=extras
Step 2/9 : FROM $EXTRAS_IMG
---> 84a2f86c12ab
Step 3/9 : ARG UID
---> Using cache
---> 75b0030ce337
Step 4/9 : ARG UNAME
---> Using cache
---> 04f452558ff9
Step 5/9 : ARG GID
---> Using cache
---> fc637242511c
Step 6/9 : ARG GROUP
---> Using cache
---> 56a3d78a7674
Step 7/9 : RUN groupadd -g ${GID} ${GROUP} && useradd -u ${UID} -g ${GID} ${UNAME} && adduser ${UNAME} sudo && passwd -d ${UNAME} && echo 'Defaults lecture_file = /etc/sudoers.lecture' >> /etc/sudoers && echo 'Defaults lecture = always' >> /etc/sudoers && echo '##################### Warning! #####################################' > /etc/sudoers.lecture && echo 'This is an ephemeral docker container! You can do things to it using' >> /etc/sudoers.lecture && echo 'sudo, but when you exit, changes made outside of the /host directory' >> /etc/sudoers.lecture && echo 'will be lost.' >> /etc/sudoers.lecture && echo 'If you want your changes to be permanent, add them to the ' >> /etc/sudoers.lecture && echo ' extras.dockerfile' >> /etc/sudoers.lecture && echo 'in the seL4-CAmkES-L4v dockerfiles repo.' >> /etc/sudoers.lecture && echo '####################################################################' >> /etc/sudoers.lecture && echo '' >> /etc/sudoers.lecture && mkdir /home/${UNAME} && echo 'echo "___ "' >> /home/${UNAME}/.bashrc && echo 'echo " | _ _ |_ _ _ |_ |_ "' >> /home/${UNAME}/.bashrc && echo 'echo " | | || ) | )/ () | |_ | ) / "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo " __ "' >> /home/${UNAME}/.bashrc && echo 'echo "(_ _ |_ _ _ _ "' >> /home/${UNAME}/.bashrc && echo 'echo ") / ) | (- ||| ) "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo "Hello, welcome to the sel4/CAmkES/L4v docker build environment"' >> /home/${UNAME}/.bashrc && echo 'export PATH=/scripts/repo:$PATH' >> /home/${UNAME}/.bashrc && echo 'cd /host' >> /home/${UNAME}/.bashrc && mkdir -p /isabelle && chown -R ${UNAME}:${GROUP} /isabelle && ln -s /isabelle /home/${UNAME}/.isabelle && chown -R ${UNAME}:${GROUP} /home/${UNAME} && chmod -R ug+rw /home/${UNAME}
---> Running in fc11857d6ea4
groupadd: group 'staff' already exists
Removing intermediate container fc11857d6ea4
The command '/bin/sh -c groupadd -g ${GID} ${GROUP} && useradd -u ${UID} -g ${GID} ${UNAME} && adduser ${UNAME} sudo && passwd -d ${UNAME} && echo 'Defaults lecture_file = /etc/sudoers.lecture' >> /etc/sudoers && echo 'Defaults lecture = always' >> /etc/sudoers && echo '##################### Warning! #####################################' > /etc/sudoers.lecture && echo 'This is an ephemeral docker container! You can do things to it using' >> /etc/sudoers.lecture && echo 'sudo, but when you exit, changes made outside of the /host directory' >> /etc/sudoers.lecture && echo 'will be lost.' >> /etc/sudoers.lecture && echo 'If you want your changes to be permanent, add them to the ' >> /etc/sudoers.lecture && echo ' extras.dockerfile' >> /etc/sudoers.lecture && echo 'in the seL4-CAmkES-L4v dockerfiles repo.' >> /etc/sudoers.lecture && echo '####################################################################' >> /etc/sudoers.lecture && echo '' >> /etc/sudoers.lecture && mkdir /home/${UNAME} && echo 'echo " "' >> /home/${UNAME}/.bashrc && echo 'echo " | _ _ |_ _ _ |_ |_ "' >> /home/${UNAME}/.bashrc && echo 'echo " | | || ) | )/ () | |_ | ) / "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo " __ "' >> /home/${UNAME}/.bashrc && echo 'echo "(_ _ |_ _ _ _ "' >> /home/${UNAME}/.bashrc && echo 'echo "__) / ) | (- ||| _) "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo "Hello, welcome to the sel4/CAmkES/L4v docker build environment"' >> /home/${UNAME}/.bashrc && echo 'export PATH=/scripts/repo:$PATH' >> /home/${UNAME}/.bashrc && echo 'cd /host' >> /home/${UNAME}/.bashrc && mkdir -p /isabelle && chown -R ${UNAME}:${GROUP} /isabelle && ln -s /isabelle /home/${UNAME}/.isabelle && chown -R ${UNAME}:${GROUP} /home/${UNAME} && chmod -R ug+rw /home/${UNAME}' returned a non-zero code: 9
make: *** [build_user] Error 9
~/work/seL4-CAmkES-L4v-dockerfiles (master)$
More recent Debian versions (including for python 3.11 in bookworm) prevent you from installing python packages via pip
or pip3
system-wide.
The recommendation on the failure message is to use Debian packages or virtual envs. Neither look to me like they make sense for this.
Installing under the default user account is also problematic, because that is root, and the interactive version oft he docker images will be running under a different account, so won't pick up that installation.
One option that could work is to make a virtual env under the root user (because further images, e.g. CI, derived from the base images would expect the packages to be visible by default), and make the host user for the interactive image somehow use that virtual env. Not sure how much work that is.
Does anyone have a better idea?
This all sounds like a whole lot of unnecessary work, because these images are essentially single user systems.
camkes-deps depends on simpleeval, whose latest version currently cannot be installed (see danthedeckie/simpleeval#90).
This affected the CASE Vagrant/VirtualBox VM setup:
https://github.com/sireum/case-env/runs/3568671703?check_suite_focus=true#step:5:6023
As a workaround, we patched basetools.sh and sel4.sh to keep the CASE VM reproducible:
One approach is to freeze seL4+CAmkES Python package dependencies to prevent similar issues to crop up (similar to using Debian snapshot).
It looks like a new form of #16 has reappeared. For
make user
I'm getting
docker run \
-it \
--hostname in-container \
--rm \
-u 501:20 --group-add stack \
--group-add sudo \
-v /Users/kleing/src/seL4/sel4-camkes-l4v-dockerfiles:/host:z \
-v kleing-home:/home/kleing \
-v /usr/share/zoneinfo.default/Australia/Sydney:/etc/localtime:ro \
user_img-kleing bash
docker: Error response from daemon: failed to create shim task: OCI runtime create failed: runc create failed: unable to start container process: error during container init: error mounting "/usr/share/zoneinfo.default/Australia/Sydney" to rootfs at "/etc/localtime": mount /usr/share/zoneinfo.default/Australia/Sydney:/etc/localtime (via /proc/self/fd/14), flags: 0x5001: not a directory: unknown: Are you trying to mount a directory onto a file (or vice-versa)? Check if the specified host path exists and is the expected type.
make: *** [Makefile:131: user_run] Error 125
If I delete the time zone line and inspect the container, there is indeed already a symlink in /etc/localtime
:
kleing@in-container:/host$ ls -l /etc/localtime
lrwxrwxrwx 1 root root 27 Aug 16 2021 /etc/localtime -> /usr/share/zoneinfo/Etc/UTC
This is on MacOS Ventura (13.0.1) and Docker version 20.10.21, build baeda1f
Follow-up from #49, do not run Authenticate and Push on forks because this always fails due to missing credentials.
Maybe we can check if secrets.DOCKER_USER
and secrets.DOCKER_TOKEN
is set. Do forks could use their own credentials here - but this would require putting allowing to customize the hard-coded trustworthysystems
then also.
I was building sel4bench and was getting compile errors due to extra GCC warnings, so I thought I'd use the compiler in the Docker container just to check that it works in there since an older compiler is used.
I did:
../init-build.sh -DPLATFORM=tx2 -DVCPU=1
and got the following output:
ivanv@in-container:/host/tx2_vcpu_container$ ../init-build.sh -DPLATFORM=tx2 -DVCPU=1
loading initial cache file /host/projects/sel4bench/settings.cmake
-- Set platform details from PLATFORM=tx2
-- KernelPlatform: tx2
-- Found seL4: /host/kernel
-- platform tx2 supports multiple architectures, none was given
-- defaulting to: aarch64
-- Found GCC with prefix aarch64-linux-gnu-
-- The C compiler identification is GNU 10.2.1
-- The CXX compiler identification is GNU 10.2.1
-- The ASM compiler identification is GNU
-- Found assembler: /usr/bin/aarch64-linux-gnu-gcc
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/aarch64-linux-gnu-gcc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/aarch64-linux-gnu-g++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found elfloader-tool: /host/tools/seL4/elfloader-tool
-- /host/tx2_vcpu_container/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating from DTB...
WARNING:root:Only mapping 4096/16777216 bytes from node /iommu@12000000, region 0. Set kernel_size in YAML to silence.
-- CPIO test cpio_reproducible_flag PASSED
-- Found musllibc: /host/projects/musllibc
-- Found util_libs: /host/projects/util_libs
-- Found seL4_libs: /host/projects/seL4_libs
-- Found sel4_projects_libs: /host/projects/sel4_projects_libs
-- Found projects_libs: /host/projects/projects_libs
-- Found sel4runtime: /host/projects/sel4runtime
-- Performing Test compiler_arch_test
-- Performing Test compiler_arch_test - Success
-- libmuslc architecture: 'aarch64' (from KernelSel4Arch 'aarch64')
-- Detecting cached version of: musllibc
-- Found Git: /usr/bin/git (found version "2.30.2")
-- Found valid cache entry for musllibc
-- Found Nanopb: /host/nanopb
-- Configuring done
-- Generating done
-- Build files have been written to: /host/tx2_vcpu_container
ivanv@in-container:/host/tx2_vcpu_container$ ninja
[210/303] Running C++ protocol buffer compiler using nanopb plugin on /host/projects/sel4_projects_libs/libsel4rpc/rpc.proto
FAILED: apps/sel4bench/sel4_projects_libs/libsel4rpc/rpc.pb.c apps/sel4bench/sel4_projects_libs/libsel4rpc/rpc.pb.h
cd /host/tx2_vcpu_container/apps/sel4bench/sel4_projects_libs/libsel4rpc && /usr/bin/protoc -I/host/tx2_vcpu_container/nanopb/generator -I/host/tx2_vcpu_container/nanopb/generator/proto -I/host/tx2_vcpu_container/apps/sel4bench/sel4_projects_libs/libsel4rpc -I/host/projects/sel4_projects_libs/libsel4rpc --plugin=protoc-gen-nanopb=/host/tx2_vcpu_container/nanopb/generator/protoc-gen-nanopb --nanopb_out=:/host/tx2_vcpu_container/apps/sel4bench/sel4_projects_libs/libsel4rpc /host/projects/sel4_projects_libs/libsel4rpc/rpc.proto
Traceback (most recent call last):
File "/host/tx2_vcpu_container/nanopb/generator/nanopb_generator.py", line 51, in <module>
from .proto import nanopb_pb2
ImportError: attempted relative import with no known parent package
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
File "/host/tx2_vcpu_container/nanopb/generator/nanopb_generator.py", line 72, in <module>
import proto.nanopb_pb2 as nanopb_pb2
File "/host/tx2_vcpu_container/nanopb/generator/proto/nanopb_pb2.py", line 8, in <module>
from google.protobuf.internal import builder as _builder
ImportError: cannot import name 'builder' from 'google.protobuf.internal' (/usr/lib/python3/dist-packages/google/protobuf/internal/__init__.py)
--nanopb_out: protoc-gen-nanopb: Plugin failed with status code 1.
[211/303] Building C object kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
ninja: build stopped: subcommand failed.
Commit 3946f2c introduced an option (":exec") when calling docker.
When using docker (version 19.03.11 on Linux) this option is rejected as not being supported:
"docker: Error response from daemon: invalid mode: exec." Also, I did not find any official piece of documentation from docker which defines the mode ":exec".
When removing this option I can successfully use the docker container from l4v.
As this change is now active for a while: am I the only one running into this problem?
The docker container is missing the 32 bit libstdc++ for compiling the poke module in Camkes VM Linux Tutorial. (Error at the end)
I was able to fix the error by installing lib32stdc++-10-dev, command below.
$ sudo apt install lib32stdc++-10-dev
Originally I was going to submit a pull request proposing an update to scripts/camkes.sh
, but when I modify the shell script and rebuild the container, the new libraries are still absent. Would someone with a better understanding of the build system look at this please? Thank you in advance. :-)
Steps to reproduce:
$ ./init --tut camkes-vm-linux --solution
$ ninja
Should fail with the error below.sudo apt install lib32stdc++-10-dev
$ ninja
Related issue: seL4/sel4-tutorials#99
Error:
- [polly] Used toolchain: Linux / gcc / PIC / c++11 support / 32 bit
-- The C compiler identification is GNU 10.2.1
-- The CXX compiler identification is GNU 10.2.1
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/gcc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - failed
-- Check for working CXX compiler: /usr/bin/g++
-- Check for working CXX compiler: /usr/bin/g++ - broken
CMake Error at /usr/share/cmake-3.18/Modules/CMakeTestCXXCompiler.cmake:59 (message):
The C++ compiler
"/usr/bin/g++"
is not able to compile a simple test program.
It fails with the following output:
Change Dir: /host/sel4-tutorials-manifest/camkes-vm-linuxay_d0gp7_build/poke-module/CMakeFiles/CMakeTmp
Run Build Command(s):/usr/bin/ninja cmTC_a618a && [1/2] Building CXX object CMakeFiles/cmTC_a618a.dir/testCXXCompiler.cxx.o
[2/2] Linking CXX executable cmTC_a618a
FAILED: cmTC_a618a
: && /usr/bin/g++ -m32 -fPIC -std=c++11 CMakeFiles/cmTC_a618a.dir/testCXXCompiler.cxx.o -o cmTC_a618a && :
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/10/libstdc++.so when searching for -lstdc++
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/10/libstdc++.a when searching for -lstdc++
/usr/bin/ld: cannot find -lstdc++
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/10/libstdc++.so when searching for -lstdc++
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
CMake will not be able to correctly generate this project.
-- Configuring incomplete, errors occurred!
The scheduled docker build+deploy action has been failing the last 3 cycles.
This first looked like a problem with the docker setup itself, because it was complaining of running out of space inside the container, but it turns out that it is actually the GitHub runner VM that is running out of space. It seems that the sum of all pulled images + installs is more than the runners have available.
I can see two options forward:
Follow-up from seL4/capdl#44
Update Haskell toolchain in containers. Currently the CI job download and build the toolchain because it's missing. This make the CI jobs running for ages and look stuck, because thee is no output until this is finished
For anything running on the host, we should not assume bash
, and in general we should invoke everything that is not /bin/sh
with /usr/bin/env
.
See also #55
Commit ac8254 apparently breaks the 'make user' command because the Dockerfiles are now in a different directory.
john@john-VirtualBox:~/Documents/cpre440x/sel4-CAmkES-L4v-dockerfiles$ make user # Figure out if any trustworthy systems docker images are potentially too old docker build --force-rm=true \ --build-arg=USER_BASE_IMG=trustworthysystems/camkes \ -f extras.dockerfile \ -t extras \ . unable to prepare context: unable to evaluate symlinks in Dockerfile path: lstat /home/john/Documents/cpre440x/sel4-CAmkES-L4v-dockerfiles/extras.dockerfile: no such file or directory Makefile:160: recipe for target 'build_user' failed make: *** [build_user] Error 1
The problem does not exist in the previous commit.
Additional docker image makes updates of packages according to build instruction Developer system requirements.
The only change is: "make user_cp" instead of "make user".
Instruction to build SDK would be:
Run container as recommended here: Using Docker for seL4, etc
Inside the container run:
/tmp/cp_prep.sh
The script will install proper sources of Core Platform and seL4 as well as
create python environment inside /host/sel4-core-platformcd /host/sel4-core-platform/sel4cp
../pyenv/bin/python build_sdk.py --sel4=../sel4_cp_support
I'm trying to verify seL4 using the verification project and l4v proofs.
I want to use the user_l4v
container to handle my dependencies but I'm having trouble when installing and configuring Isabelle.
The Isabelle components appear to be installed to /root/.isabelle
. The problem is that I can't access this as another user, so the Isabelle test fails when I run ./run_tests
:
TEST FAILED: isabelle
### Building Isabelle/Scala ...
Unknown JAVA_HOME -- Java unavailable
Failed to compile sources
When I try to configure Isabelle as a user, with the commands:
mkdir -p ~/.isabelle/etc
cp -i misc/etc/settings ~/.isabelle/etc/settings
./isabelle/bin/isabelle components -a
./isabelle/bin/isabelle jedit -bf
./isabelle/bin/isabelle build -bv HOL-Word
I get the following error at the jedit
build command:
tpreston@in-container:/host/l4v$ ./isabelle/bin/isabelle jedit -bf
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 1.6
Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
1 warning
### Building Isabelle/Scala ...
Error: Could not find or load main class scala.tools.nsc.Main
Failed to compile sources
I'm not sure what I'm missing, or if the warnings are to do with my error. Any assistance here would be useful. Thank you.
robbiewu@robbiedeair seL4-CAmkES-L4v-dockerfiles % make user
scripts/utils/check_for_old_docker_imgs.sh
WARNING: Unable to check if your trustworthysystems docker images are getting a bit old!
The date command did not behave as expected. Skipping the check.
docker build --force-rm=true \
--build-arg=USER_BASE_IMG=trustworthysystems/camkes \
-f dockerfiles/extras.Dockerfile \
-t extras \
.
[+] Building 276.2s (7/7) FINISHED
=> [internal] load build definition from extras.Dockerfile 0.0s
=> => transferring dockerfile: 607B 0.0s
=> [internal] load .dockerignore 0.0s
=> => transferring context: 153B 0.0s
=> [internal] load metadata for docker.io/trustworthysystems/camkes:latest 4.2s
=> [auth] trustworthysystems/camkes:pull token for registry-1.docker.io 0.0s
=> [1/2] FROM docker.io/trustworthysystems/camkes@sha256:2dfe8e125a61b661e475a75 121.6s
=> => resolve docker.io/trustworthysystems/camkes@sha256:2dfe8e125a61b661e475a753f 0.0s
=> => sha256:2dfe8e125a61b661e475a753f6081dc12c95a63c245f8eb56fe58 1.79kB / 1.79kB 0.0s
=> => sha256:dd50eddb09bea873c9139295bdf5e18c0cea3a276d63f5edf1086 8.26kB / 8.26kB 0.0s
=> => sha256:6fc55abfba0d87027dac918d6beba1579daefa4fa39e1a1f8c3 12.13kB / 12.13kB 1.1s
=> => sha256:afb6ec6fdc1c3ba04f7a56db32c5ff5ff38962dc4cd0ffdef5b 27.10MB / 27.10MB 1.2s
=> => sha256:03d756ce13c072cc33240799e524316d1942d0f8f21e51bd 132.98MB / 132.98MB 27.0s
=> => sha256:cfaf6fd66bfefddf974a6f11ef5f94f7e588f312812050c54de 12.10kB / 12.10kB 1.4s
=> => sha256:4092e53e147f12f08a54990ea088cf98d448610536f70870 702.53MB / 702.53MB 91.3s
=> => extracting sha256:afb6ec6fdc1c3ba04f7a56db32c5ff5ff38962dc4cd0ffdef5beaa0ce2 0.8s
=> => sha256:815c86a1454a9f90ffe7848d985c17648ac3cda2ee0baf0e3dc 12.10kB / 12.10kB 1.8s
=> => sha256:bb3669078ee93402dccc7d8e61182849fac976009fa04c66 476.80MB / 476.80MB 76.2s
=> => extracting sha256:6fc55abfba0d87027dac918d6beba1579daefa4fa39e1a1f8c3d98bac3 0.0s
=> => extracting sha256:03d756ce13c072cc33240799e524316d1942d0f8f21e51bdc91901c764 3.1s
=> => extracting sha256:cfaf6fd66bfefddf974a6f11ef5f94f7e588f312812050c54de64c206f 0.0s
=> => extracting sha256:4092e53e147f12f08a54990ea088cf98d448610536f7087005294f59b 17.8s
=> => extracting sha256:815c86a1454a9f90ffe7848d985c17648ac3cda2ee0baf0e3dc54838d1 0.0s
=> => extracting sha256:bb3669078ee93402dccc7d8e61182849fac976009fa04c66c0f836b98 11.6s
=> [2/2] RUN apt-get update -q && apt-get install -y --no-install-recommends 150.0s
=> exporting to image 0.3s
=> => exporting layers 0.3s
=> => writing image sha256:d488115963071b0845c2621f3667b1b56e68b9a2f07c6236e79bc19 0.0s
=> => naming to docker.io/library/extras 0.0s
Use 'docker scan' to run Snyk tests against images to find vulnerabilities and learn how to fix them
docker build --force-rm=true \
--build-arg=EXTRAS_IMG=extras \
--build-arg=UNAME=robbiewu \
--build-arg=UID=501 \
--build-arg=GID=20 \
--build-arg=GROUP=staff \
-f dockerfiles/user.Dockerfile \
-t user_img-robbiewu .
[+] Building 3.0s (4/4) FINISHED
=> [internal] load build definition from user.Dockerfile 0.0s
=> => transferring dockerfile: 358B 0.0s
=> [internal] load .dockerignore 0.0s
=> => transferring context: 34B 0.0s
=> ERROR [internal] load metadata for docker.io/library/extras:latest 2.9s
=> [auth] library/extras:pull token for registry-1.docker.io 0.0s
------
> [internal] load metadata for docker.io/library/extras:latest:
------
failed to solve with frontend dockerfile.v0: failed to create LLB definition: pull access denied, repository does not exist or may require authorization: server message: insufficient_scope: authorization failed
make: *** [build_user] Error 1
robbiewu@robbiedeair seL4-CAmkES-L4v-dockerfiles % docker images -a
REPOSITORY TAG IMAGE ID CREATED SIZE
extras latest d48811596307 54 seconds ago 4.92GB
The branches "spdx" and "fix_os" have been merged, so they should be deleted.
On my machine the make user
command fails as in [0]. Not sure if this is related to running on MacOS. This is with the TZ workaround from #16.
If I remove the --group-add stack
statements out of the Docker run commands in the Makefile it works fine. See
Makefile:143 and Makefile:159.
The --group-add logic is from 4468454. I'd be happy to provide more info or do a bit more digging, though I'm not quite sure what to look for.
Thanks!
[0]
$ make user
scripts/utils/check_for_old_docker_imgs.sh
WARNING: Unable to check if your trustworthysystems docker images are getting a bit old!
The date command did not behave as expected. Skipping the check.
docker build --force-rm=true \
--build-arg=USER_BASE_IMG=trustworthysystems/camkes \
-f dockerfiles/extras.dockerfile \
-t extras \
.
Sending build context to Docker daemon 82.94kB
Step 1/3 : ARG USER_BASE_IMG=trustworthysystems/sel4
Step 2/3 : FROM $USER_BASE_IMG
---> 8a4b088ab00a
Step 3/3 : RUN apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo
---> Using cache
---> 2bcdbd197230
Successfully built 2bcdbd197230
Successfully tagged extras:latest
docker build --force-rm=true \
--build-arg=EXTRAS_IMG=extras \
--build-arg=UNAME=davidm \
--build-arg=UID=501 \
--build-arg=GID=20 \
--build-arg=GROUP=staff \
-f dockerfiles/user.dockerfile \
-t user_img-davidm .
Sending build context to Docker daemon 82.94kB
Step 1/9 : ARG EXTRAS_IMG=extras
Step 2/9 : FROM $EXTRAS_IMG
---> 2bcdbd197230
Step 3/9 : ARG UID
---> Using cache
---> a892a214a72e
Step 4/9 : ARG UNAME
---> Using cache
---> eaf7700c5c44
Step 5/9 : ARG GID
---> Using cache
---> af9bd3f12730
Step 6/9 : ARG GROUP
---> Using cache
---> 1ba31f073f1e
Step 7/9 : RUN groupadd -fg ${GID} ${GROUP} && useradd -u ${UID} -g ${GID} ${UNAME} && adduser ${UNAME} sudo && passwd -d ${UNAME} && echo 'Defaults lecture_file = /etc/sudoers.lecture' >> /etc/sudoers && echo 'Defaults lecture = always' >> /etc/sudoers && echo '##################### Warning! #####################################' > /etc/sudoers.lecture && echo 'This is an ephemeral docker container! You can do things to it using' >> /etc/sudoers.lecture && echo 'sudo, but when you exit, changes made outside of the /host directory' >> /etc/sudoers.lecture && echo 'will be lost.' >> /etc/sudoers.lecture && echo 'If you want your changes to be permanent, add them to the ' >> /etc/sudoers.lecture && echo ' extras.dockerfile' >> /etc/sudoers.lecture && echo 'in the seL4-CAmkES-L4v dockerfiles repo.' >> /etc/sudoers.lecture && echo '####################################################################' >> /etc/sudoers.lecture && echo '' >> /etc/sudoers.lecture && mkdir /home/${UNAME} && echo 'echo "___ "' >> /home/${UNAME}/.bashrc && echo 'echo " | _ _ |_ _ _ |_ |_ "' >> /home/${UNAME}/.bashrc && echo 'echo " | | |_| _) |_ \)/ (_) | |_ | ) \/ "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo " __ "' >> /home/${UNAME}/.bashrc && echo 'echo "(_ _ |_ _ _ _ "' >> /home/${UNAME}/.bashrc && echo 'echo "__) \/ _) |_ (- ||| _) "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo "Hello, welcome to the sel4/CAmkES/L4v docker build environment"' >> /home/${UNAME}/.bashrc && grep export /root/.bashrc >> /home/${UNAME}/.bashrc && echo 'export PATH=/scripts/repo:$PATH' >> /home/${UNAME}/.bashrc && echo 'cd /host' >> /home/${UNAME}/.bashrc && mkdir -p /isabelle && chown -R ${UNAME}:${GROUP} /isabelle && ln -s /isabelle /home/${UNAME}/.isabelle && chown -R ${UNAME}:${GROUP} /home/${UNAME} && chmod -R ug+rw /home/${UNAME}
---> Using cache
---> 96226bebb062
Step 8/9 : VOLUME /home/${UNAME}
---> Using cache
---> 54d078d1551a
Step 9/9 : VOLUME /isabelle
---> Using cache
---> e967f268baec
Successfully built e967f268baec
Successfully tagged user_img-davidm:latest
docker run \
-it \
--hostname in-container \
--rm \
-u 501:20 \
--group-add stack \
-v /Users/davidm/Dev/seL4-CAmkES-L4v-dockerfiles:/host:z \
-v davidm-home:/home/davidm \
-e TZ=Australia/Sydney \
user_img-davidm bash
docker: Error response from daemon: Unable to find group stack.
make: *** [user_run] Error 125
Currently the images are not building, due to an incompatibility with some of clang's dependencies requiring changes in gcc's dependencies. This is because clang is pulled from Debian Testing, and so is constantly being changed and updated.
The error looks something like this:
bash -c 'apt-get install -y --no-install-recommends -t bullseye clang-8 libclang-8-dev qemu-system-arm '
Reading package lists...
Building dependency tree...
Reading state information...
Some packages could not be installed. This may mean that you have
requested an impossible situation or if you are using the unstable
distribution that some required packages have not yet been created
or been moved out of Incoming.
The following information may help to resolve the situation:
The following packages have unmet dependencies:
clang-8 : Depends: libobjc-8-dev but it is not going to be installed
libc6-dev : Breaks: libgcc-8-dev (< 8.4.0-2~) but 8.3.0-6 is to be installed
libclang-8-dev : Depends: libobjc-8-dev but it is not going to be installed
E: Error, pkgProblemResolver::Resolve generated breaks, this may be caused by held packages.
We're currently working on a fix, and hope to have it pushed out soon.
For a more trustworthy build/supply chain story, we should
apt-install
I can see needing the stack group for the l4v image but it doesn't seem required for a regular build environment. It seems to work fine if I remove this line:
When running make user command inside the seL4-CAmkES-L4v-dockerfiles folder the following error occurs on Step 3. "rm: cannot remove '/var/lib/apt/lists/*': No such file or directory". (Full error message below). I am not sure
System Setup
Ubuntu 18.04.3 LTS
Kernel version: 5.0.0-37-generic x86_64 I
Step 3/3 : RUN rm -r /var/lib/apt/lists/* && apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo && apt-get clean autoclean && apt-get autoremove --yes && rm -rf /var/lib/{apt,dpkg,cache,log}/
---> Running in e66d8cad4c49
rm: cannot remove '/var/lib/apt/lists/': No such file or directory
Removing intermediate container e66d8cad4c49
The command '/bin/sh -c rm -r /var/lib/apt/lists/ && apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo && apt-get clean autoclean && apt-get autoremove --yes && rm -rf /var/lib/{apt,dpkg,cache,log}/' returned a non-zero code: 1
Makefile:160: recipe for target 'build_user' failed
I am not sure if this a real error.
Thanks & Regards
BeFlo
Hi,
I'm using the user container to build seL4 Tutorial 1 but I get the following unexpected error:
tpreston@in-container:/host$ mkdir build_hello_1
tpreston@in-container:/host$ cd build_hello_1/
tpreston@in-container:/host/build_hello_1$ ../init --plat pc99 --tut hello-1
The following files do not require modifications but are copied to provide context:
hello-1/src/util.c
The following files need to be modified to complete the tutorial
hello-1/src/main.c
-- Configuring done
-- Generating done
-- Build files have been written to: /host/build_hello_1
tpreston@in-container:/host/build_hello_1$ ninja
[2/148] Generate invocation header gen_headers/arch/api/sel4_invocation.h
FAILED: kernel/gen_headers/arch/api/sel4_invocation.h
cd /host/build_hello_1/kernel && rm -f gen_headers/arch/api/sel4_invocation.h && python /h
Traceback (most recent call last):
File "/host/kernel/tools/invocation_header_gen.py", line 21, in <module>
import tempita
ImportError: No module named tempita
[3/148] Generate invocation header gen_headers/arch/api/invocation.h
FAILED: kernel/gen_headers/arch/api/invocation.h
cd /host/build_hello_1/kernel && rm -f gen_headers/arch/api/invocation.h && python /host/h
Traceback (most recent call last):
File "/host/kernel/tools/invocation_header_gen.py", line 21, in <module>
import tempita
ImportError: No module named tempita
[5/148] Generate invocation header gen_headers/api/invocation.h
FAILED: kernel/gen_headers/api/invocation.h
cd /host/build_hello_1/kernel && rm -f gen_headers/api/invocation.h && python /host/kerneh
Traceback (most recent call last):
File "/host/kernel/tools/invocation_header_gen.py", line 21, in <module>
import tempita
ImportError: No module named tempita
[6/148] Generate syscall invocations
FAILED: kernel/gen_headers/arch/api/syscall.h
cd /host/build_hello_1/kernel && /host/kernel/tools/xmllint.sh --noout --schema /host/kerh
Traceback (most recent call last):
File "/host/kernel/tools/syscall_header_gen.py", line 22, in <module>
import tempita
ImportError: No module named tempita
[7/148] Concatenating C files
ninja: build stopped: subcommand failed.
Because python-tempita is only installed for Python 3:
tpreston@in-container:/host/build_hello_1$ python3 -c "import tempita"
tpreston@in-container:/host/build_hello_1$ python -c "import tempita"
Traceback (most recent call last):
File "<string>", line 1, in <module>
ImportError: No module named tempita
tpreston@in-container:/host/build_hello_1$ find ~/.local/lib/ -name tempita
/home/tpreston/.local/lib/python3.6/site-packages/tempita
So I have to manually install it for Python 2 like so:
mkdir ~/.local/lib/python2.7/site-packages
python ./kernel/tools/python-deps/setup.py install --prefix=~/.local
Where in the Dockerfile is the correct place to install this? Presumably this should be done at the same time python-tempita is installed for Python 3.
When I used "make user", the error was:
useradd: user 'root' already exists
Makefile:284: recipe for target 'build_user' failed
make: *** [build_user] Error 9
I used Ubuntu 16.04 for x86_64, thanks!
Sincerely
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.