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: README.md
+5-31Lines changed: 5 additions & 31 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -153,8 +153,8 @@ In general, we **recommend Nix** because it creates a sandbox environment with a
153
153
- For **Mac** users, we recommend Nix or Docker. (We experienced problems with installing Agda manually.)
154
154
- For **Linux** users, any alternative is fine but we recommend Nix for the reasons mentioned above.
155
155
156
-
There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose..
157
-
The only dependency of our library is the Agda standard library which is shipped as a git submodule within the `agda-stdlib` directory and is taken care of automatically by our [makefile](makefile).
156
+
There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose.
157
+
The only dependency of our library is the Agda standard library which is automatically taken care of by our Nix and Docker setups.
158
158
159
159
Note that building for the first time (or running `nix-shell`) will take a while because Agda has to build the required dependencies from the standard library (expect ~5-10min and a lot of terminal output).
160
160
@@ -253,24 +253,8 @@ make
253
253
which will compile the library and run its small demo.
254
254
The expected output is explained in detail in the Step-by-Step guide below.
255
255
256
-
## Step-by-Step Guide
257
256
258
-
The "Kick-The-Tires" section above basically explains all necessary steps to get the library up and running.
259
-
Here, we give additional instructions on the expected output and how to play with other demo inputs.
260
-
For using the library once you finished the setup, please have a look at the later _Reusability Guide_, which, among other
261
-
information, includes an overview of the library, notes on our mechanized proofs, and tutorials for getting to know the library.
262
-
263
-
### How does the demo know which standard library to use?
264
-
265
-
Agda looks for its dependencies in a directory specified by the environment variable `AGDA_DIR`. The provided [makefile](makefile) sets this environment variable temporarily and locally during the build process to the `.libs` directory within this repository. (Your global setup will not be affected). If you want to run `agda` manually, or if you want to work on this project in an editor (e.g., emacs) then you have to set this environment variable to the libs directory in this repository.
266
-
267
-
```shell
268
-
export AGDA_DIR="path/to/this/repository/libs"
269
-
```
270
-
271
-
Beware that setting the variable will overwrite any previously set directory. In that case you might want to overwrite the variable only temporarily while working on this project.
272
-
273
-
### Expected Output
257
+
#### Expected Output
274
258
275
259
The demo will print a long terminal output of about 1250 lines.
276
260
A copy of the expected output can be found in the [expected-output.txt](expected-output.txt).
@@ -593,23 +577,13 @@ during a Docker build, you might have encountered an out of memory issue.
593
577
Try to rerun the same command after closing other applications which might comsume a lot of RAM.
594
578
In some cases it may also be necessary to disable some kind of out-of-memory killer (also known as OOM killer or OOM deamon) but use this option with caution.
595
579
596
-
### Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib.
597
-
The following error may occur when executing `make` after a manual setup:
598
-
```
599
-
Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib.
600
-
Reason: ./libs/../agda-stdlib/standard-library.agda-lib: openBinaryFile: does not exist (No such file or directory)
601
-
make: *** [makefile:15: build] Error 42
602
-
```
603
-
This error indicates that the `agda-stdlib` git submodule has not been set up correctly.
604
-
Executing `git submodule update --init` in the root of the repository should fix the problem.
605
-
606
580
## Where does the library name 'Vatras' come from?
607
581
608
582
The name Vatras is (of course) an acronym, which stands for _VAriability language TRAnslationS_.
609
583
Besides, Vatras is a water mage in the classic german RPG [Gothic II](https://almanach.worldofgothic.de/index.php/Vatras), who stems from the city of Varant, which almost sounds like _Variant_.
610
584
Vatras is praying to the god Adanos, who brings some kind of equality or balance loosely speaking.
0 commit comments