You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: INSTALL.md
+15-10Lines changed: 15 additions & 10 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -6,12 +6,13 @@ In the following, we describe how to build the Docker image and run the experime
6
6
How to install Docker depends on your operating system.
7
7
8
8
#### Windows or Mac
9
-
You can find download and installation instructions [here](https://www.docker.com/get-started).
9
+
You can find download and installation instructions [here](https://www.docker.com/get-started).
10
+
10
11
#### Linux Distributions
11
-
How you can install Docker on your system, depends on your distribution. However, the chances are high that Docker is part of your distributions package database.
12
+
How to install Docker on your system, depends on your distribution. However, the chances are high that Docker is part of your distributions package database.
12
13
Docker's [documentation](https://docs.docker.com/engine/install/) contains instructions for common distributions.
To build the Docker container you can run the build script corresponding to your OS
30
32
```
31
33
# Windows:
@@ -34,19 +36,19 @@ To build the Docker container you can run the build script corresponding to your
34
36
./build.sh
35
37
```
36
38
37
-
## Validation & expected output
39
+
## Validation & Expected Output
38
40
39
-
### Running the validation
41
+
### Running the Validation
40
42
To run the validation you can run the script corresponding to your OS with `validation` as first argument. The validation should take about 10-20 minutes depending on your hardware.
41
43
```
42
44
# Windows:
43
45
.\execute.bat validation
44
46
# Linux/Mac (bash):
45
47
./execute.sh validation
46
48
```
47
-
The results of the validation are stored in the [results](results) directory.
49
+
The results of the validation will be stored in the [results](results) directory.
48
50
49
-
### Expected output of the validation
51
+
### Expected Output of the Validation
50
52
The aggregated results of the validation can be found in the following files.
51
53
52
54
- The [speed statistics](results/difftrees/speedstatistics.txt) contain information about the total runtime, median runtime, mean runtime, and more:
@@ -93,6 +95,9 @@ The aggregated results of the validation can be found in the following files.
93
95
#Error[#else or #elif without #if]: 9
94
96
#Error[not all annotations closed]: 6
95
97
```
98
+
99
+
(Note that the above links only have a target after running the validation.)
100
+
The processing times might deviate.
96
101
97
102
## Troubleshooting
98
103
@@ -104,10 +109,10 @@ The aggregated results of the validation can be found in the following files.
104
109
### 'Unable to find image 'replication-package:latest' locally'
105
110
`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.
106
111
107
-
`Fix:` Build the Docker container.
112
+
`Fix:`Follow the instructions described above in the section `Build the Docker Container`.
108
113
109
114
### No results after validation, or 'cannot create directory '../results/difftrees': Permission denied'
110
115
`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.
111
116
112
117
`Fix:` If there is a _results_ directory delete it with elevated permission (e.g., `sudo rm -r results`).
113
-
Then, create a new _results_ directory without elevated permissions, or execute `git restore .` to restore the deleted directory.
118
+
Then, create a new _results_ directory without elevated permissions, or execute `git restore .` to restore the deleted directory.
0 commit comments