Skip to content

Commit 1511710

Browse files
AlexanderSchultheissibbem
authored andcommitted
Updated README
1 parent f29c774 commit 1511710

2 files changed

Lines changed: 8 additions & 3 deletions

File tree

INSTALL.md

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -99,13 +99,18 @@ The aggregated results of the validation can be found in the following files.
9999

100100
## Troubleshooting
101101

102-
### Got permission denied while trying to connect to the Docker daemon socket
102+
### 'Got permission denied while trying to connect to the Docker daemon socket'
103103
`Problem:` This is a common problem under Linux, if the user trying to execute Docker commands does not have the permissions to do so.
104104

105105
`Fix:` You can fix this problem by either following the [post-installation instructions](https://docs.docker.com/engine/install/linux-postinstall/), or by executing the scripts in the replication package with elevated permissions (i.e., `sudo`)
106106

107-
### Unable to find image 'replication-package:latest' locally
107+
### 'Unable to find image 'replication-package:latest' locally'
108108
`Problem:` The Docker container could not be found. This either means that the name of the container that was built does not fit the name of the container that is being executed (this only happens if you changed the provided scripts), or that the Docker container was not built yet.
109109

110110
`Fix:` Build the Docker container.
111111

112+
### No results after validation, or 'cannot create directory '../results/difftrees': Permission denied'
113+
`Problem:` This problem can occur due to how permissions are managed inside the Docker container. More specifically, it will appear, if Docker is executed with elevated permissions (i.e., `sudo`) and if there is no [results](results) directory because it was deleted manually. In this case, Docker will create the directory with elevated permissions, and the Docker user has no permissions to access the directory.
114+
115+
`Fix:` If there is a _results_ directory delete it (e.g., via your file explorer).
116+
Then, create a new _results_ directory without elevated permissions, or execute `git restore .` to restore the deleted directory.

docker/execute.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ if [ "$1" == 'replication' ] || [ "$1" == 'validation' ]; then
2323
java -cp DiffDetectiveRunner.jar mining.FindMedianCommitTime ../results/difftrees
2424
java -cp DiffDetectiveRunner.jar mining.tablegen.MiningResultAccumulator ../results/difftrees ../results/difftrees
2525
python3 plotting/plot.py
26-
cp ./runtime_histogram.png ../results/
26+
cp ./runtime_histogram.png ../results/ || exit
2727
echo "The results are located in the 'results' directory."
2828
elif [ "$1" == 'proofs' ]; then
2929
echo "Running the proofs"

0 commit comments

Comments
 (0)