Awesome

MiniAgda

A prototypical dependently typed languages with sized types and variances.

Installation from Hackage

Requires ghc and cabal, for instance via the Haskell Platform or via ghcup. In a shell, type

  cabal update
  cabal install MiniAgda

Installation from Stackage

MiniAgda is not on Stackage because it depends on a specific version of haskell-src-exts rather than the latest version. You can install with stack from source though, see next section.

Installation from source

Obtain the sources.

git clone https://github.com/andreasabel/miniagda
cd miniagda

Checkout the desired version (optional): If you want to build a released version or a branch rather than the latest master, switch to this version/branch.
```
git checkout $REF
```
E.g. REF = v0.2022.3.11 for version 0.2022.3.11 or REF = unfold for branch unfold.
Building and running the tests (optional).
- With cabal (requires ghc in your PATH):
```
cabal build --enable-tests
cabal test
```
  After building, you can run MiniAgda locally, e.g.:
```
cabal run miniagda -- examples/Gcd/gcd.ma
```
- With stack:
```
stack build --stack-yaml=stack-$GHCVER.yaml
stack test  --stack-yaml=stack-$GHCVER.yaml
```
  At the time of writing (2022-05-14), GHCVER can be any of 8.8.4, 8.10.7, 9.0.2, or 9.2.2.
  
  After building, you can run MiniAgda locally, e.g.:
```
stack run --stack-yaml=stack-9.2.2.yaml -- examples/Gcd/gcd.ma
```
  You can copy stack-$GHCVER.yaml for your choice of GHCVER into stack.yaml and drop the --stack-yaml argument from stack invocation.
Install.
- With cabal (requires ghc in your PATH):
```
cabal install
```
- With stack:
```
stack install --stack-yaml=stack-$GHCVER.yaml
```
  At the time of writing (2022-05-14), GHCVER can be any of 8.8.4, 8.10.7, 9.0.2, or 9.2.2.
Note that the respective installation directory should be on your PATH.

Examples

See directories test/succeed/ and examples/.

Some examples are commented on the (dormant) MiniAgda blog.