search

seL4 / seL4-CAmkES-L4v-dockerfiles

Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.
12 stars 39 forks source link

Docker option :exec not accepted by docker. #21

Closed gbadevic-hc closed 4 years ago

gbadevic-hc commented 4 years ago

Commit 3946f2c24db528311b4c27a2d8bc19ce8357ad62 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?

LukeMondy commented 4 years ago

Yes, I ran into it yesterday too.

As part of the changes I made (as per: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles/pull/20#issuecomment-647892101 ), I removed it as well.

As to you being the first to notice: we don't have any data on how many people use the Docker images in this way, unfortunately. In this case, I imagine you would be in the minority, given that this issue only affects people using the L4v image. In my experience, most people go for the C code first, rather than the verification, so that may explain it :)

Thanks again.

LukeMondy commented 4 years ago

You can see the change here: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles/commit/7aab59fdeebc49a717613cd3b0dc558bda10fa28