Agda Environment

Demo

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.7s
Agda Test (agda)
Agda
{-# BUILTIN NATURAL ℕ #-}
_+_ :     
zero + b = b
suc a + b = suc (a + b)
0.6s
Agda Test (agda)
Agda
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
2.4s
Agda Test (agda)
Agda
_ : 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
19.6s
Agda + StdLib (Bash)

Install Agda via Cabal.

cabal update
cabal install --jobs=16 Agda
1316.9s
Agda + StdLib (Bash)

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
15.8s
Agda + StdLib (Bash)

Install Jupyter and Agda Jupyter Kernel from nextjournal fork (better support for completions, e.g. give + case split).

Intall Jupyter Kernel

previouse kernel at 807c7f7c9f93cfd1af9648a3139b149b4096dba9. (Environment timestamp: 2019-12-06 15:54:24).

pip install jupyter jupyter_client \
  git+https://github.com/nextjournal/jupyter_core
pip install \
  git+https://github.com/nextjournal/agda-kernel.git@5486b2b9f277aa3434f889e6064cff4a8061d614
python -m agda_kernel.install
28.2s
kernel installAgda Kernel (Bash)
Agda + StdLib

Check.

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

Agda Environment

This is Agda with its Jupyter Kernel installed plus a warmup of stdlib imports for faster execution.

module StdLibWarmup where
import Relation.Binary.PropositionalEquality as Eq
open Eq
open Eq.-Reasoning
12.9s
Agda (agda)
Agda Kernel
open import Data.Nat
open import Data.Nat.Properties
56.7s
Agda (agda)
Agda Kernel
open import Level
1.0s
Agda (agda)
Agda Kernel
open import Function
open import Function.Inverse
open import Function.LeftInverse
3.7s
Agda (agda)
Agda Kernel
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Unit
open import Data.Bool
1.5s
Agda (agda)
Agda Kernel
open import Relation.Nullary
open import Relation.Nullary.Negation
0.8s
Agda (agda)
Agda Kernel

PLFA Environment

Agda with on top the book installed as library

cd /opt/agda
if [ -d "plfa.github.io" ]; then
  rm -rf plfa.github.io
fi
git clone https://github.com/plfa/plfa.github.io
5.5s
PLFA (Bash)
Agda
cat opt/agda/plfa.github.io/plfa.agda-lib
0.7s
PLFA (Bash)
Agda
echo "/opt/agda/plfa.github.io/plfa.agda-lib" >> ~/.agda/libraries
0.1s
PLFA (Bash)
Agda
cat ~/.agda/libraries
0.9s
PLFA (Bash)
Agda
echo "plfa" >> ~/.agda/defaults
0.1s
PLFA (Bash)
Agda
cat ~/.agda/defaults
0.5s
PLFA (Bash)
Agda

Test PLFA Imports

module plfa.part1.Connectives where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.-Reasoning
open import Data.Nat using ()
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality)
open plfa.part1.Isomorphism.-Reasoning
0.6s
Test PLFA Imports (Agda)
PLFA
export
0.6s
Test PLFA Imports (Bash in Agda)
PLFA
Runtimes (6)
Runtime Languages (2)