user_l4v: Java errors with Isabelle build environment

[tompreston]

I'm trying to verify seL4 using the verification project and l4v proofs.

• https://github.com/seL4/verification-manifest
• https://github.com/seL4/l4v/

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.

[tompreston]

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

[LukeMondy]

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.

[tompreston]

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!