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.5s
Agda Test (Agda)
Agda 2.6.1.2 + StdLib
{-# BUILTIN NATURAL ℕ #-}
_+_ : ℕ → ℕ → ℕ
zero + b = b
suc a + b = suc (a + b)
0.4s
Agda Test (Agda)
Agda 2.6.1.2 + StdLib
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
3.6s
Agda Test (Agda)
Agda 2.6.1.2 + StdLib
_ : 1 + 1 ≡ 2
_ =
  begin
    1 + 1
  ≡⟨⟩
    (suc 0) + 1
  ≡⟨⟩
    suc (0 + 1)
  ≡⟨⟩
    suc 1
  ≡⟨⟩
    2
  ∎
0.6s
Agda Test (Agda)
Agda 2.6.1.2 + StdLib

Setup

Agda Install

Get dependencies and the Cabal package manager.

apt-get -qq update
DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends \
  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
24.5s
Agda + StdLib (Bash)
→

Install Agda via Cabal.

cabal update
cabal install --jobs=16 Agda-2.6.1.2
1998.6s
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.4.tar.gz
cd /opt/agda
tar -zxvf agda-stdlib.tar
cd /opt/agda/agda-stdlib-1.4
cabal install
mkdir -p ~/.agda
echo "/opt/agda/agda-stdlib-1.4/standard-library.agda-lib" > ~/.agda/libraries
echo "standard-library" > ~/.agda/defaults
15.2s
Agda + StdLib (Bash)
→

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

agda --version
0.7s
Test CLI (Bash)
Agda + StdLib

Intall Jupyter Kernel

previous kernel at 5486b2b9f277aa3434f889e6064cff4a8061d614. (Environment timestamp: 2020-07-09 09:31:15).

conda install jupyter
pip install --upgrade jupyter_client jupyter_core
pip install \
  git+https://github.com/nextjournal/agda-kernel.git@9139338a08e4c14c305fe6f16602fcc8a4a03150
python -m agda_kernel.install
60.7s
kernel installAgda Kernel (Bash)
Agda + StdLib

Check.

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

Stdlib Warmup

This is a warmup of stdlib imports for faster import at "runtime".

module StdLibWarmup where
import Relation.Binary.PropositionalEquality as Eq
open Eq
open Eq.≡-Reasoning
19.7s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Data.Nat
open import Data.Nat.Properties
open import Data.Fin
open import Data.Fin.Properties
56.9s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Level
1.4s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Function
open import Function.Inverse
open import Function.LeftInverse
3.1s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Unit
open import Data.Bool
1.7s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Data.Vec
open import Data.Vec.Properties
open import Data.List
open import Data.List.Properties
101.9s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
20.3s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Data.Sum
open import Data.Product
1.5s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable
open import Relation.Unary
open import Relation.Binary
1.5s
Agda 2.6.1.2 + StdLib (Agda)
Agda Kernel
open import Algebra
1.7s
Agda 2.6.1.2 + StdLib (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
6.2s
PLFA (Bash)
Agda 2.6.1.2 + StdLib
cat opt/agda/plfa.github.io/plfa.agda-lib
0.7s
PLFA (Bash)
Agda 2.6.1.2 + StdLib
echo "/opt/agda/plfa.github.io/plfa.agda-lib" >> ~/.agda/libraries
0.5s
PLFA (Bash)
Agda 2.6.1.2 + StdLib
cat ~/.agda/libraries
0.6s
PLFA (Bash)
Agda 2.6.1.2 + StdLib
echo "plfa" >> ~/.agda/defaults
0.5s
PLFA (Bash)
Agda 2.6.1.2 + StdLib
cat ~/.agda/defaults
0.7s
PLFA (Bash)
Agda 2.6.1.2 + StdLib

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
10.7s
Test PLFA Imports (Agda)
PLFA
export
0.7s
Test PLFA Imports (Bash in Agda)
PLFA

Build Agda 2.6.1.2

This is our "official" default Agda v2.6.1.2 environment ships with standard library and the cubical library. This will be used when adding an agda cell via ```agda or insert-menu.

wget -O /opt/agda/cubical-v0.2.tar \
        https://github.com/agda/cubical/archive/v0.2.tar.gz
cd /opt/agda
tar -zxvf cubical-v0.2.tar
2.2s
Agda 2.6.1.2 (Bash)
Agda 2.6.1.2 + StdLib
echo "/opt/agda/cubical-0.2/cubical.agda-lib" >> ~/.agda/libraries
echo "cubical" >> ~/.agda/defaults
0.7s
Agda 2.6.1.2 (Bash)
Agda 2.6.1.2 + StdLib
{-# OPTIONS --cubical #-}
module CubiTest {ℓ} where
open import Cubical.Core.Primitives
  hiding (_≡_)
_ : I
_ = i0
_ = i1
postulate
  ℐ : I → Set ℓ
  a₀ : (ℐ i0)
  a₁ : (ℐ i1)
-- PathP : (ℐ : I → Set ℓ) → (ℐ i0) → (ℐ i1) → Set ℓ
-- intro and elim
PathP⁺ : (f : (i : I) → (ℐ i)) → PathP ℐ (f i0) (f i1)
PathP⁺ f = λ i → f i
PathP⁻ : (p : PathP ℐ a₀ a₁) → (r : I) → (ℐ r)
PathP⁻ p r = p r
-- equality
_≡_ : {A : Set ℓ} → A → A → Set ℓ
_≡_ {A} = PathP (λ _ → A)
funExt : {A : Set ℓ} → {B : A → Set ℓ} →
         {f g : (x : A) → B x} →
         (p : (x : A) → f x ≡ g x) → f ≡ g
funExt p = λ i x → (p x) i
0.5s
Cubical Agda Test (Agda)
Agda 2.6.1.2
Runtimes (9)
Runtime Languages (2)