PLFA Environment

[Deprecated]: New Agda default env/templates have stdlib baked in

A Nextjournal Companion Environment to the PLFA book. See the Setup section below for seeing what's installed in the PLFA environment. The idea is to use the PLFA environment in each notebook covering book chapters (e.g. see imported naturals chapter ).

Using PLFA env

module plfa.Naturals where

0.7s

Naturals Test (agda)

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

0.5s

Naturals Test (agda)

{-# BUILTIN NATURAL ℕ #-}

0.6s

Naturals Test (agda)

_+_ : ℕ → ℕ → ℕ

0 + n = n
(suc n) + m = suc (n + m)

0.6s

Naturals Test (agda)

Test less-equal as inductive type (indexed on pairs of nats).

data _≤_ : ℕ -> ℕ -> Set where
  leq-zero : {n : ℕ} -> zero ≤ n
  leq-suc : {m n : ℕ} -> m ≤ n -> suc m ≤ suc n

0.7s

Naturals Test (agda)

leq-trans : {l m n : ℕ} -> l ≤ m -> m ≤ n -> l ≤ n
leq-trans leq-zero _ = leq-zero
leq-trans (leq-suc p) (leq-suc q) = leq-suc (leq-trans p q)

0.7s

Naturals Test (agda)

import Relation.Binary.PropositionalEquality as Eq

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

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    suc (1 + 3)
  ≡⟨⟩
    suc (suc (0 + 3))
  ≡⟨⟩
    suc (suc 3)
  ≡⟨⟩
    5
  ∎

0.6s

Naturals Test (agda)

Caveats

At present for some reason we cannot import Data.Nat module from standard lib even though other modules seem to be importable, like the one below

module Test.Import where

import Relation.Binary.PropositionalEquality as Eq

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

11.9s

Import Test (agda)

❌ Cannot import Data.Nat The following cell will never terminate (UPDATE: this is actually a kernel timeout, works with the forked kernel, cell takes about 70s to type check).

module Test.Import.Broken where

open import Data.Nat using (ℕ; zero; suc)

0.6s

Import Test (agda)

and but the cell below executes alright.

module Test.Import.Broken2 where

open import Agda.Builtin.Nat public
  using (zero; suc) renaming (Nat to ℕ)

0.6s

Import Test (agda)

❌Cross-cell holes/goal-hints missing and auto

Hole-filling (Tab) and Goal inspection (shift + Tab) through completions seems to work if the cell is a self-contained module: (hitting Tab or shift+Tab with the cursor after the ?). Although sometimes a ? is filled with the hole marker {! !} but sometimes auto-fill seems to apply and a concrete variable is filled.

module TestHole where

id : (A : Set) → A → A
id A a = {! !}

0.5s

Naturals Test (agda)

If the module is split (as often the case in PLFA)

module TestCrossCellHole where

0.5s

Naturals Test (agda)

Tab seems to trigger auto (i.e. emacs C-c C-a) shift+Tab doesn't seem to work any more. Need to clarify this upstream with the Jupyter Kernel

id : {A : Set} → A → A
id a = ?

0.5s

Naturals Test (agda)

Setup Standard Library

mkdir -p /opt/agda

0.6s

PLFA (Bash)

Download stdandard library.

wget -O /opt/agda/agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.1.tar.gz

2.1s

PLFA (Bash)

extract

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

0.7s

PLFA (Bash)

Install Agda Standard Library v1.1

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

18.9s

PLFA (Bash)

mkdir -p ~/.agda

0.2s

PLFA (Bash)

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

0.2s

PLFA (Bash)

echo "standard-library" > ~/.agda/defaults

0.2s

PLFA (Bash)

cat ~/.agda/libraries
cat ~/.agda/defaults
cat /opt/agda/agda-stdlib-1.1/standard-library.agda-lib

0.7s

PLFA (Bash)

Build PLFA on top of Agda Kernel dev

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

23.0s

PLFA (dev kernel) (Bash)

cat ~/.agda/libraries
cat ~/.agda/defaults
cat /opt/agda/agda-stdlib-1.1/standard-library.agda-lib

0.6s

PLFA (dev kernel) (Bash)

module Test.Import where

import Relation.Binary.PropositionalEquality as Eq

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

11.8s

agda

No better luck from master branch of agda kernel repo:

module Test.Import.Broken where

open import Data.Nat using (ℕ; zero; suc)

67.7s

agda