Skip to content

Commit 93f730a

Browse files
committed
docs: update the setup instructions
1 parent 81cf52a commit 93f730a

1 file changed

Lines changed: 38 additions & 23 deletions

File tree

README.md

Lines changed: 38 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -140,9 +140,9 @@ We tested our setup on Manjaro, NixOS, Windows Subsystem for Linux (WSL2), and w
140140
> In case of problems, there is a "Troubleshooting" section at the bottom of this file.
141141
142142
### Setup
143-
Clone the library and its submodules to a directory of your choice:
143+
Clone the library to a directory of your choice:
144144
```shell
145-
git clone --recursive https://github.com/VariantSync/Vatras.git
145+
git clone https://github.com/VariantSync/Vatras.git
146146
```
147147

148148
There are **three alternative ways** to compile the library and run its small demo.
@@ -160,7 +160,7 @@ Note that building for the first time (or running `nix-shell`) will take a while
160160

161161
#### Alternative 1: Setup via Nix
162162

163-
The installation of Nix depends on your operating system. Head to the [NixOS website](https://nixos.org/download/) and follow the installation instructions for your system. Follow the download instructions for `Nix: the package manager`, not `NixOS: the Linux distribution`! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal terminal, you can install Nix by following the instructions for installing Nix on linux from the [NixOS website](https://nixos.org/download/).
163+
The installation of Nix depends on your operating system. Head to the [NixOS website](https://nixos.org/download/) and follow the installation instructions for your system. Follow the download instructions for `Nix: the package manager`, not `NixOS: the Linux distribution`! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal, you can install Nix by following the instructions for installing Nix on Linux from the [NixOS website](https://nixos.org/download/).
164164

165165
When you have Nix installed on your system, open a terminal, navigate to this directory, and then simply open a Nix shell by typing
166166
```shell
@@ -189,7 +189,7 @@ How to install Docker depends on your operating system. **For Windows or Mac**,
189189
Once you have installed Docker, start the Docker daemon.
190190
**On Windows**, open the search bar using the 'Windows Key' and search for 'Docker' or 'Docker Desktop'.
191191
**On Linux**, the docker daemon typically runs automatically, so there is nothing to do; otherwise, start Docker's service using your service manager (e.g., with `systemd`, execute `sudo systemctl start docker`).
192-
More detailed instructions on starting the deamon are given [here](https://docs.docker.com/config/daemon/start/) on the docker website.
192+
More detailed instructions on starting the deamon are given [on the docker website](https://docs.docker.com/config/daemon/start/).
193193

194194
Afterwards, open a terminal and navigate to this repository's directory (the directory containing this README.md).
195195
First, you must create the docker image:
@@ -210,7 +210,7 @@ docker run -t vatras
210210

211211
#### Alternative 3: Manual Setup
212212

213-
The library needs Agda version 2.6.4.3 (newer version should also work but we did not test them).
213+
The library needs Agda version 2.8.0 (newer version should also work but we did not test them).
214214
There are different ways to install Agda.
215215
Following the [Agda book's installation instructions], we recommend using [GHCup][ghcup] to install GHC, Cabal, and Agda as follows (You may skip steps for tools you have already installed but there might be compatibility errors with some versions):
216216

@@ -222,27 +222,36 @@ Following the [Agda book's installation instructions], we recommend using [GHCup
222222
1. Install the GHC compiler and the cabal build tool with [GHCup][ghcup].
223223

224224
```shell
225-
ghcup install ghc 9.2.4
225+
ghcup install ghc 9.12.2
226226
ghcup install cabal recommended
227227

228-
ghcup set ghc 9.2.4
228+
ghcup set ghc 9.12.2
229229
ghcup set cabal recommended
230230
```
231231

232232
2. Install Agda (this may take a while).
233233

234234
```shell
235235
cabal update
236-
cabal install Agda-2.6.4.3
236+
cabal install Agda-2.8.0
237237
```
238238

239239
To test whether the installation worked or whether your existing installation of Agda has the right version you can check the following command's output:
240240
```shell
241241
> agda --version
242-
Agda version 2.6.4.3
242+
Agda version 2.8.0
243243
```
244+
245+
3. Install the [Agda standard library](https://github.com/agda/agda-stdlib) version 2.3.
246+
247+
```shell
248+
wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.3.tar.gz
249+
tar -xzf agda-stdlib.tar.gz
250+
mkdir -p "$(agda --print-agda-app-dir)"
251+
realpath agda-stdlib-2.3/standard-library.agda-lib >> "$(agda --print-agda-app-dir)/libraries"
252+
```
244253
245-
In case of confusion or trouble, we recommend to check the [official installation instructions](https://agda.readthedocs.io/en/v2.6.4.3/getting-started/installation.html), or follow the Getting-Started guide in the [Programming Language Foundations in Agda][plfa] book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file.
254+
In case of confusion or trouble, we recommend to check the [official installation instructions](https://agda.readthedocs.io/en/v2.8.0/getting-started/installation.html), or follow the Getting-Started guide in the [Programming Language Foundations in Agda][plfa] book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file.
246255
247256
To test whether your setup is correct, and to run the demo you may use our makefile.
248257
Make sure your terminal is in full-screen because the demo assumes to have at least 100 characters of horizontal space in the terminal for pretty-printing.
@@ -342,9 +351,21 @@ Then add your new list to the `examples` list at the bottom of the file.
342351

343352
### Using our library in your own Agda projects
344353

354+
In order to use Vatras in your project, you need to state `Vatras` as a dependency in your Agda library file.
355+
An Agda library file has the suffix `.agda-lib` and is usually contained in the root directory of your project.
356+
Its content, including the dependency to Vatras, should include the following:
357+
```
358+
name: YOUR-PROJECT-NAME
359+
depend: Vatras
360+
include: SOME/PATH/IN/YOUR/PROJECT
361+
```
362+
For details about Agda's library management, please have a look at [Agda's packaging guide](https://agda.readthedocs.io/en/v2.8.0/tools/package-system.html).
363+
364+
Afterwards, you need to follow one of the following alternatives to let Agda know where to find Vatras.
365+
345366
#### Alternative 1: Installation via Nix
346367

347-
When using Nix, you can use this repository as a library in you own project, by using `agda.withPackages`:
368+
When using Nix, you can install this repository as an Agda library by using `agda.withPackages`:
348369
```nix
349370
agda = nixpkgs.agda.withPackages [
350371
nixpkgs.agdaPackages.standard-library
@@ -357,19 +378,13 @@ Though, not required, we recommend to use the [nixpkgs pin](nix/sources.json) cr
357378

358379
#### Alternative 2: Manual installation
359380

360-
After downloading this library, you can register it by appending the path of [Vatras.agda-lib](Vatras.agda-lib) to the file `$AGDA_DIR/libraries`, creating it if necessary.
361-
If the environment variable `AGDA_DIR` is unset, it defaults to `~/.agda` on unix-like systems and `C:\Users\USERNAME\AppData\Roaming\agda` or similar on Windows.
362-
After registering this library on your system, you can use it in your project by stating `Vatras` as a dependency in your Agda library file.
363-
An Agda library file has the suffix `.agda-lib` and is usually contained in the root directory of your project.
364-
Its content, including the dependency to Vatras, should include the following:
365-
366-
```
367-
name: YOUR-PROJECT-NAME
368-
depend: Vatras
369-
include: SOME/PATH/IN/YOUR/PROJECT
381+
After downloading this library, you can register it using the following commands:
382+
```shell
383+
mkdir -p "$(agda --print-agda-app-dir)"
384+
realpath Vatras.agda-lib >> "$(agda --print-agda-app-dir)/libraries"
370385
```
371-
372-
For details about Agda's library management, please have a look at [Agda's packaging guide](https://agda.readthedocs.io/en/v2.6.4.3/tools/package-system.html).
386+
Make sure that you also have the Agda standard library version 2.3 installed.
387+
See step 3 in the [manual setup](#alternative-3-manual-setup) for details on how to install ths Agda standard library.
373388

374389
### Notes on Mechanized Proofs
375390

0 commit comments

Comments
 (0)