Skip to content

Commit c5656b0

Browse files
carlostomeWhatisRT
authored andcommitted
Add instructions to build without nix (#431)
1 parent cef3505 commit c5656b0

File tree

1 file changed

+29
-0
lines changed

1 file changed

+29
-0
lines changed

CONTRIBUTING.md

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,8 @@ To install Agda locally and use that install with emacs, you can do the followin
6161

6262
`nix-shell` provides Agda complete with the correct dependencies. So you should be able to run your preferred editor within `nix-shell` and it should see the required `agda` executable.
6363

64+
For instructions _not using_ `nix-shell`, check [Setup without nix-shell](setup-without-nix-shell).
65+
6466
## Working on libraries
6567

6668
To work simultaneously on the ledger and one of its dependencies, the easiest way to do this is to remove the library from the ledger's `.agda-lib` file and add its path to the `include:` section. Then, when finished, push the changes to the library, then update `default.nix` to point to your new commit.
@@ -110,6 +112,33 @@ niv update nixpkgs -r 4e329926df7ee5fa49929a83d31ee7d541f8b45c
110112
niv update nixpkgs -v 21.11.337905.902d91def1e
111113
```
112114

115+
## Setup without nix-shell
116+
117+
- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-1-install-agda>).
118+
- In a folder `LIB`, clone the dependencies
119+
+ [agda-stdlib](https://github.com/agda/agda-stdlib)
120+
+ [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes)
121+
+ [agda-stdlib-meta](https://github.com/agda/agda-stdlib-meta)
122+
+ [agda-sets](https://github.com/input-output-hk/agda-sets)
123+
and checkout the commits/tags found in `default.nix` (e.g. `v2.1.1` for `agda-stdlib-meta`).
124+
- Create a file `LIB/libraries` with the following content:
125+
```
126+
LIB/agda-stdlib/standard-library.agda-lib
127+
LIB/agda-stdlib-classes/agda-stdlib-classes.agda-lib
128+
LIB/agda-stdlib-meta/agda-stdlib-meta.agda-lib
129+
LIB/agda-sets/abstract-set-theory.agda-lib
130+
```
131+
- Instead of `agda` use `agda --library-file LIB/libraries`. For example, to typecheck `Everything.agda`:
132+
```
133+
cd src/
134+
agda --library-file LIB/libraries Everything.agda
135+
```
136+
137+
To build targets from the Makefile (e.g. see [Building other artifacts](building-other-artifacts)), use:
138+
```
139+
AGDA="agda --library-file LIB/libraries" make html
140+
```
141+
113142
## Maintainer
114143

115144
This repository is maintained by @WhatisRT.

0 commit comments

Comments
 (0)