Nextjournal / Aug 06 2021
by Andrea Amantini, Micah P. Dombrowski and Martin Kavalar

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

data ℕ : Set where 
  zero : ℕ
  suc : ℕ → ℕ
0.6s
Agda Test (agda)
Agda
{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
0 + n = n
(suc n) + m = suc (n + m)
0.8s
Agda Test (agda)
Agda
import Relation.Binary.PropositionalEquality as Eq

open Eq public using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning public using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
0.8s
Agda Test (agda)
Agda

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
_ =
  begin
    1 + 1
  ≡⟨⟩
    (suc 0) + 1
  ≡⟨⟩
    suc (0 + 1)
  ≡⟨⟩
    suc 1
  ≡⟨⟩
    2
  ∎
0.7s
Agda Test (agda)
Agda

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
50.7s
Agda + StdLib (Bash)
Minimal Python 3

Install Agda via Cabal.

cabal update
cabal install --jobs=4 Agda
1567.0s
Agda + StdLib (Bash)
Minimal Python 3

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 https://github.com/agda/agda-stdlib/archive/v1.1.tar.gz

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
16.2s
Agda + StdLib (Bash)
Minimal Python 3

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+https://github.com/nextjournal/agda-kernel.git
python -m agda_kernel.install
22.8s
Agda (Bash)
Agda + StdLib

Check.

du -hsx /
agda -V
jupyter kernelspec list
1.5s
Agda (Bash)
Agda + StdLib

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
0.6s
PLFA (agda)
Agda
open import Data.Nat
open import Data.Nat.Properties
0.7s
PLFA (agda)
Agda
open import Level
0.8s
PLFA (agda)
Agda
open import Function
open import Function.Inverse
open import Function.LeftInverse
4.2s
PLFA (agda)
Agda
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Unit
open import Data.Bool
0.9s
PLFA (agda)
Agda
open import Relation.Nullary
open import Relation.Nullary.Negation
0.8s
PLFA (agda)
Agda

TODO: clone and install plfa as lib 

ls /
0.7s
PLFA (Bash in agda)
Agda