Agda Environment


Interaction should follow Jupyter Agda Kernel rules, e.g Tab for symbol expansion or hole filling, Shift+Tab to inspect goal summary.

module HelloAgda where

data ℕ : Set where 
  zero : ℕ
  suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
0 + n = n
(suc n) + m = suc (n + m)
import Relation.Binary.PropositionalEquality as Eq

open Eq public using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning public using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

Note: since Agda Jupyter Kernel wraps every cell in its own module prior to loading, in order to be able to use definitions from imported modules, these have to be opened in public mode.

_ : 1 + 1 ≡ 2
_ =
    1 + 1
    (suc 0) + 1
    suc (0 + 1)
    suc 1


Agda Install

Get dependencies and the Cabal package manager.

apt-get -qq update
DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends \
  build-essential gfortran cmake automake libtool libltdl-dev pkg-config \
  zlib1g-dev libncurses5-dev libicu-dev \
  ghc cabal-install alex happy
apt-get clean
rm -r /var/lib/apt/lists/* # Clear package list so it isn't stale

Install Agda via Cabal.

cabal update
cabal install --jobs=4 Agda

Install Agda Standard Library

And require it by default. See the installation instructions for more informations.

mkdir -p /opt/agda

wget -O /opt/agda/agda-stdlib.tar

cd /opt/agda
tar -zxvf agda-stdlib.tar

cd /opt/agda/agda-stdlib-1.1
cabal install

mkdir -p ~/.agda
echo "/opt/agda/agda-stdlib-1.1/standard-library.agda-lib" > ~/.agda/libraries
echo "standard-library" > ~/.agda/defaults

Install Jupyter and Agda Jupyter kernel forked at nextjournal (we need increased timeout when issuing commands to the agda process).

pip install jupyter jupyter_client 
pip install git+
python -m agda_kernel.install


du -hsx /
agda -V
jupyter kernelspec list

PLFA Environment

This is Agda, plus a warmup of stdlib imports for faster execution

module plfa.imports where

import Relation.Binary.PropositionalEquality as Eq
open Eq
open Eq.≡-Reasoning
open import Data.Nat
open import Data.Nat.Properties
open import Level
open import Function
open import Function.Inverse
open import Function.LeftInverse
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Unit
open import Data.Bool
open import Relation.Nullary
open import Relation.Nullary.Negation

TODO: clone and install plfa as lib

ls /