Environment

supersedes nextjournal/agda-environment with a simplified env stack:

  • base

  • kernel

  • libraries (stdlib, cubical)

  • lib warmup (Agda cells)

  • PLFA

  • lib warmup (Agda cells)

Agda Base Env

Install a newer GHC via https://launchpad.net/~hvr/+archive/ubuntu/ghc/+index, we'll need to prepend /opt/ghc/bin to the PATH in the runtime's env variables.

apt-get update && apt-get install software-properties-common
6.1s
add-apt-repository ppa:hvr/ghc
apt-get -qq update
DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends \
  zlib1g-dev libncurses5-dev libicu-dev \
  ghc-9.0.1 cabal-install-3.4 alex happy
apt-get clean
rm -r /var/lib/apt/lists/* # Clear package list so it isn't stale
7.3s
ghc --version
0.7s
cabal update
cabal install -foptimise-heavily --jobs=16 Agda-2.6.2
2662.5s

/root/.cabal/bin is added to PATH in the following dependent runtime

/root/.cabal/bin/agda --version
0.6s

Agda Kernel

agda --version
0.6s
pip install --upgrade jupyter jupyter_client jupyter_core
pip install \
  git+https://github.com/nextjournal/agda-kernel.git@9139338a08e4c14c305fe6f16602fcc8a4a03150
python -m agda_kernel.install
24.1s
jupyter kernelspec list
1.1s

Agda Libraries

Standard library

mkdir -p /opt/agda
wget -O /opt/agda/agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.tar.gz
cd /opt/agda
tar -zxvf agda-stdlib.tar
cd /opt/agda/agda-stdlib-1.7
cabal install
mkdir -p ~/.agda
echo "/opt/agda/agda-stdlib-1.7/standard-library.agda-lib" >> ~/.agda/libraries
echo "standard-library" >> ~/.agda/defaults
17.0s

Agda Cubical library

wget -O /opt/agda/cubical-v0.3.tar \
        https://github.com/agda/cubical/archive/v0.3.tar.gz
cd /opt/agda
tar -zxvf cubical-v0.3.tar
echo "/opt/agda/cubical-0.3/cubical.agda-lib" >> ~/.agda/libraries
echo "cubical" >> ~/.agda/defaults
1.0s
cat ~/.agda/libraries
cat ~/.agda/defaults
0.6s

Warmup Libraries

Importing common modules and exporting the resulting runtime speeds up imports in notebooks using the Agda environment.

{-# OPTIONS --cubical #-}
module Libraries.Warmup where
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable
open import Relation.Unary
open import Relation.Binary
import Relation.Binary.PropositionalEquality as Eq
open Eq
open Eq.≡-Reasoning
27.5s
open import Level
0.7s
open import Function
open import Function.Inverse
open import Function.LeftInverse
3.9s
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Sum
open import Data.Product
16.3s
open import Data.Nat
open import Data.Vec
open import Data.Vec.Properties
open import Data.List
open import Data.List.Properties
open import Data.Fin
116.2s
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
18.6s
open import Algebra
1.8s
open import Cubical.Core.Everything
4.7s
open import Cubical.Foundations.Everything
59.8s
open import Cubical.Algebra.Algebra
73.1s
Runtimes (4)