Andrea Amantini / Aug 21 2019

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
data ℕ : Set where 
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
_+_ : ℕ → ℕ → ℕ

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

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
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)
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

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_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

❌ 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)

and but the cell below executes alright.

module Test.Import.Broken2 where

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

❌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 = {! !}

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

module TestCrossCellHole where

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 = ?

Setup Standard Library

mkdir -p /opt/agda

Download stdandard library.

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

extract

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

Install Agda Standard Library v1.1

cd /opt/agda/agda-stdlib-1.1
cabal install
mkdir -p ~/.agda

Register as library

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

Register as default

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

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
cat ~/.agda/libraries
cat ~/.agda/defaults
cat /opt/agda/agda-stdlib-1.1/standard-library.agda-lib
module Test.Import where

import Relation.Binary.PropositionalEquality as Eq

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

No better luck from master branch of agda kernel repo:

module Test.Import.Broken where

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