Agda Environment

Showcase

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

proj1 : ∀ {A B : Set} → A → B → A
proj1 x y = x
module DepTypes where

data Bool : Set where
    true false : Bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data ⊥ : Set where
not : Bool → Bool
not true  = false
not false = true

Setup

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 the Agda Jupyter kernel.

pip install jupyter jupyter_client agda_kernel
python -m agda_kernel.install

Install Jupyter extensions that may be useful.

pip install git+https://github.com/lclem/jupyter_contrib_nbextensions
jupyter contrib nbextension install --system
jupyter nbextension enable --py widgetsnbextension
jupyter nbextension enable agda-extension/main
jupyter nbextension enable toc2/main

Check.

du -hsx /
agda -V
jupyter kernelspec list