überSpark: Refinements to General User's Guide installation walk-through

@Cap, have created this thread bringing in some of the discussions from:

and

Let us use this thread for purposes of refining the general user’s guide based on your installation walkthrough.

Thanks!

Linked PR:

I am confused about installing the backend theorem provers.

The uberspark documentation states that “CVC3, Alt-Ergo and Z3” are needed. Versions are later given for “Why3 version 0.87.3 and Alt-ergo version 1.30.” However, there are no versions for CVC3 and Z3.

The frama-c documentation referenced doesn’t give me an intuition about how to install these other provers. It seems to imply that the latest opam version should work. Is this the case?

Also, should the provers be installed before frama-c? As the frama-c documentation states “when using Coq and Why-3, it is better to install them before, or to re-configure and re-install
WP”

@Cap, dont worry about the frama-c dependencies for now. With the nextgen toolkit, all these details will be subsumed by the verification bridge for frama-c (which in essence will be a docker container).

The current generation toolkit docs and the next generation toolkit docs are mutually exclusive. i.e., one would follow one or the other, never both. The current generation toolkit will at some point soon be defunct and superseded by the new toolkit.

I have revised the task description to reflect that we will only be focusing on the next-gen toolkit for this task.

Copy all. When I follow the next-gen build instructions. I am failing to make at the build_sdefpp step.

I receive the following error:

successfully built x86_64 build truss!
docker run --rm -i -e D_CMD="make -f sdefpp.mk" -e D_CMDARGS=" -w all" -e MAKE="make" -v /home/slab/uberspark:/home/docker/uberspark -t hypcode/uberspark-build-x86_64 
# Run eval $(opam env) to update the current shell environment
touch: cannot touch './build-docs.mk': Permission denied
touch: cannot touch './install.mk': Permission denied
touch: cannot touch './build-libs.mk': Permission denied
touch: cannot touch './build-x86_64.Dockerfile': Permission denied
touch: cannot touch './commondefs.mk': Permission denied
touch: cannot touch './sdefpp.mk': Permission denied
touch: cannot touch './build-frontend.mk': Permission denied
Makefile:50: recipe for target 'build_sdefpp' failed
make: *** [build_sdefpp] Error 1

Hey @Cap, this is with a

make clean
make

?

Also, could you provide the development environment details?

This looks like some docker permissions related issue. Can you check the permissions of the git clone folder?

Yes, I receive that error after a

make clean
make

This is on a Ubuntu 16.04 VM running in virtualbox (linux kernel 4.15.0-91, Docker version 18.06.0-ce). The git clone folder has read/write permissions for the user and group, but only read for other (i.e. -rw-rw-r--), with the owner being $USER

Within the docker container, the files are owned by the opam user/group. This write permission issue continues to create build issues throughout the build process (e.g. when directories are made in the sdefpp Makefile).

This seems like a generic docker volume mount issue to me. Can you post the listing of the ls -l command within uberspark.git folder?

Within the docker container, the files are owned by the opam user/group.

Can you try using chown to set both the owner and group of all files within the local checkout folder to $USER?

I list below the output of ls -l for my working local checkout (I am running WSL/Ubuntu 16.04.2 LTS under Window 10):

dv@optimus:/c/data/work/repos/public/uberspark/uberspark.git$ ls -l
total 24
drwxrwxrwx 1 dv dv 4096 Feb 26 11:59 build-trusses
-rw-rw-rw- 1 dv dv 1743 Mar 27 13:16 CHANGELOG.rst
-rw-rw-rw- 1 dv dv 1926 Mar 27 13:16 COPYING.rst
drwxr-xr-x 1 dv dv 4096 Mar 27 13:14 docs
drwxr-xr-x 1 dv dv 4096 Mar 27 13:16 _install
-rw-rw-rw- 1 dv dv 1900 Mar 27 13:16 LICENSE
-rw-rw-rw- 1 dv dv 4230 Mar 27 13:16 Makefile
-rw-rw-rw- 1 dv dv 1033 Mar 27 13:16 README.rst
-rw-rw-rw- 1 dv dv  404 Mar 27 13:16 RELEASE
drwxr-xr-x 1 dv dv 4096 Feb 26 15:32 src
drwxrwxrwx 1 dv dv 4096 Mar 27 11:12 src-nextgen
drwxrwxrwx 1 dv dv 4096 Feb 26 11:59 testbed

the files on my local machine are owned by $USER. Below is the output from ls -l

slab@slab-VBox:~/uberspark$ ls -l
total 48
drwxrwxrwx  2 slab slab 4096 Mar 27 16:28 build-trusses
-rw-rw-r--  1 slab slab 1743 Mar 27 16:24 CHANGELOG.rst
-rw-rw-r--  1 slab slab 1926 Mar 27 16:24 COPYING.rst
drwxrwxrwx  3 slab slab 4096 Mar 27 16:24 docs
-rw-rw-r--  1 slab slab 1900 Mar 27 16:24 LICENSE
-rw-rw-r--  1 slab slab 4230 Mar 27 16:24 Makefile
-rw-rw-r--  1 slab slab 1033 Mar 27 16:24 README.rst
-rw-rw-r--  1 slab slab  404 Mar 27 16:24 RELEASE
drwxrwxrwx  6 slab slab 4096 Mar 27 16:24 src
drwxrwxrwx 16 slab slab 4096 Mar 27 14:33 src-nextgen
drwxrwxrwx  4 slab slab 4096 Mar 27 16:24 testbed

The issue is stemming from the lack of a write permission for those outside of the owner’s group (mine lack the 3rd ‘w’ in the permissions).

Even after recursively changing all of the files in the repository to have a write permission (chmod -R o+w .), I still get a build error.

Warning 26: unused variable id_value.
make[1]: Leaving directory '/home/docker/uberspark/src-nextgen/tools/sdefpp'
make: Leaving directory '/home/docker/uberspark/build-trusses'
find  -type f  -exec touch {} + 
touch: cannot touch './src-nextgen/tools/sdefpp/_build/uberspark_sdefpp': Permission denied
touch: cannot touch './src-nextgen/tools/sdefpp/_build/uberspark_sdefpp.cmx': Permission denied
touch: cannot touch './src-nextgen/tools/sdefpp/_build/uberspark_sdefpp.ml': Permission denied
touch: cannot touch './src-nextgen/tools/sdefpp/_build/uberspark_sdefpp.cmi': Permission denied
touch: cannot touch './src-nextgen/tools/sdefpp/_build/uberspark_sdefpp.o': Permission denied
Makefile:50: recipe for target 'build_sdefpp' failed
make: *** [build_sdefpp] Error 1

Hmm, there seem to be two problems from what I can see:

  1. the other permissions are only “r” on all files
  2. files and directories created within the build docker container (e.g., ./src-nextgen/tools/sdefpp/_build/*) somehow have different permissions to that of the host which explains why the find -type f -exec touch {} + (which is executed on the host after sdefpp build) fails…

Can you do a ls -l on ./src-nextgen/tools/sdefpp/ and ./src-nextgen/tools/sdefpp/_build/ to see what permissions the folder/files there have?

Thanks!

the files/folders created by the build script are missing write permissions.

k$ ls -l src-nextgen/tools/sdefpp/
total 40
drwxr-xr-x 2 systemd-timesync 65533  4096 Mar 28 09:21 _build
-rw-rw-rw- 1 slab             slab    673 Mar 28 09:21 Makefile
-rw-rw-rw- 1 slab             slab     98 Mar 28 09:21 README.rst
-rw-rw-rw- 1 slab             slab  16173 Mar 28 09:21 uberspark_sdefpp.ml
-rw-rw-rw- 1 slab             slab  12168 Mar 28 09:21 uberspark_sdefpp.ml.triage

and

$ ls -l src-nextgen/tools/sdefpp/_build/
total 5352
-rwxr-xr-x 1 systemd-timesync 65533 5350600 Mar 28 09:21 uberspark_sdefpp
-rw-r--r-- 1 systemd-timesync 65533    2694 Mar 28 09:21 uberspark_sdefpp.cmi
-rw-r--r-- 1 systemd-timesync 65533   47598 Mar 28 09:21 uberspark_sdefpp.cmx
-rw-r--r-- 1 systemd-timesync 65533   16173 Mar 28 09:21 uberspark_sdefpp.ml
-rw-r--r-- 1 systemd-timesync 65533   55760 Mar 28 09:21 uberspark_sdefpp.o

Where systemd-timesync and 65533 correspond to docker and nogroup respectively.

However, when I add the ls -l into the dockerfile so that it runs just before the touch command, the files are shown as owned by opam

Ahh…I think I might have found the issue…the build docker container does not run as root, so there might be a UID conflict resulting in all the mayhem

See:

Interestingly, this does not manifest under WSL. Can you try to tweak the build docker container to remove the USER docker line and see if that might do the trick?

removing the USER docker line from the Dockerfile fixed the problem. It builds successfully now.

However, I didn’t fully heed the note about where the binaries are installed at ~/uberspark as this was where my repo was also located (as the make install script performs a rm -rf ~/uberspark).

My estimate on the required disk space for installing the next-gen uberspark toolchain is ~2.4GB (with ~1.5GB being required for docker images)

@Cap, thanks for all the tests – very helpful!

Can you perhaps issue a PR with the following refinements:

  1. ensure all files have 644 permissions, with scripts having additional execute permissions
  2. comment out USER docker within build dockerfile with a comment perhaps to say we need to at some point address UID with alpine distros
  3. revise the documentation with a note on the disk space requirements
  4. amend build scripts to add a check to see if ~/uberspark is non-empty; if so warn the user and/or provide a prompt to go ahead and overwrite it

Let me know if you need any clarifications on the above or want to include something more to this list.

I am working on the PR.

As a note, I think that commenting out the USER docker line fixes the file permissions (fix 2 removes the need for fix 1). After I recloned the repo into a new directory, I did not modify the permissions and was able to successfully build with only the change to the Docker USER.

After I recloned the repo into a new directory, I did not modify the permissions and was able to successfully build with only the change to the Docker USER.

Great! Thanks @Cap!

PR created. I had some issues creating a user option to continue if directory already exists. So PR only stops and reports and error because the directory already exists.

That should work for now. Maybe we can just throw a message informing the user to retry after deleting the directory, if already present. Thanks!