user_l4v: Java errors with Isabelle build environment about sel4-camkes-l4v-dockerfiles HOT 3 CLOSED

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://[email protected]/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

from sel4-camkes-l4v-dockerfiles.

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:

• What image are you using? If it's a bit old, you can update it by running: make pull_l4v_image in the dockerfile repo.
• Do you have an older docker volume hanging around? Run 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.
• Can you try skipping that step (./isabelle/bin/isabelle jedit -bf) and see if the other steps are OK?
• Are you running these commands in an X11 environment, in a VM, or something else? Any extra info is helpful.

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.

from sel4-camkes-l4v-dockerfiles.

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!

from sel4-camkes-l4v-dockerfiles.