Skip to content

Commit

Permalink
README: refactor description of running the demo
Browse files Browse the repository at this point in the history
  • Loading branch information
AlexanderSchultheiss committed Jul 3, 2024
1 parent da3d698 commit 1f1c3b2
Showing 1 changed file with 17 additions and 8 deletions.
25 changes: 17 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -63,10 +63,9 @@ When you have Nix installed on your system, you can get access to all necessary
```shell
nix-shell
```
Alternatively, the demo can be compiled and run directly using
Alternatively, the demo can be compiled locally to [./result/bin](./result/bin):
```shell
nix-build
./result/bin/Vatras
```

#### Alternative 2: Setup via Docker
Expand All @@ -90,11 +89,6 @@ docker images
```
and checking that an image called `vatras` is listed.

You can then run the demo by running the image:

```shell
docker run -t vatras
```

#### Alternative 3: Manual Setup

Expand Down Expand Up @@ -133,6 +127,10 @@ Following the [Agda book's installation instructions], we recommend using [GHCup
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.
### Compiling the Library and Running the Demo
> The following three alternatives depend on the setup you have chosen above. Please make sure to use the instructions meant for your setup.
#### Running the demo in a `nix-shell` or after a `manual setup`.
If you set up the environment using `nix-shell` or a `manually`, you can compile and run the demo using `make`.
To test whether your setup is correct, and to run the demo you may use our makefile (except for the docker setup which requires to run the image as explained above).
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.
Expand All @@ -142,10 +140,21 @@ Then run
make
```
which will compile the library and run its small demo.
Alternatively, you may use `nix-build` as explained above.
The demo will then print a range of translations of variational expressions to the terminal.
The expected output is explained in detail in the Step-by-Step guide below.
#### Running the demo after `nix-build`
If you already build the library locally with `nix-build`, you should run the demo's binary directly instead of using `make`.
```shell
./result/bin/Vatras
```

#### Running the demo with Docker
You can then run the demo by running the Docker image that you created during the setup:
```shell
docker run -t vatras
```

## Step-by-Step Guide

The "Kick-The-Tires" section above basically explains all necessary steps to get the library up and running.
Expand Down

0 comments on commit 1f1c3b2

Please sign in to comment.