Closed tompreston closed 5 years ago
Steps to reproduce:
# clone the dockerfiles
git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git
# sync the verification project
mkdir verification
cd verification
repo init -u ssh://git@github.com/seL4/verification-manifest.git
repo sync
# build and enter the user_l4v container
make -C ../seL4-CAmkES-L4v-dockerfiles user_l4v HOST_DIR=$(pwd)
# inside the container
cd l4v
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
./run_tests
Hi @tompreston , thanks for the report.
I followed your instructions, and unfortunately I wasn't able to reproduce the error.
A few things to check:
make pull_l4v_image
in the dockerfile repo.docker volume ls
, and you will likely see something like <your username>-home
. You can try deleting that (docker volume rm <your username>-home
), and then running the commands again. It will mean you have to re-download the isabelle components though../isabelle/bin/isabelle jedit -bf
) and see if the other steps are OK?In regard to your reference to /root/.isabelle
- it is true that it is there, but from what I can tell it is not used when using the docker images with make user_l4v
, so it shouldn't cause an issue.
There has been some structural changes to how these files are used internally, so that may have introduced some bugs, and has lead to some of the confusing bits (e.g., the /root/.isabelle
, and /isabelle
) that need to be cleaned up.
Hi @LukeMondy, Thanks for getting back to me so quickly. I think removing the tpreston-home image and rebuilding has fixed the issue. I ran the following commands:
docker volume rm tpreston-home
make pull_l4v_image
Then I can enter the container, run the Isabelle configuration commands and run the tests with the commands above. Right now the tests are taking too long to run on my laptop, so I'm searching for a build machine but I think we can consider this issue solved for now.
For completeness, I am running Debian 9 with Gnome 3 (X11 environment) and docker version:
Docker version 18.06.1-ce, build e68fc7a
Thanks again for your help!
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
:When I try to configure Isabelle as a user, with the commands:
I get the following error at the
jedit
build command: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.