/klac

KL Agda course

Primary LanguageAgda

klac

                  _                                     __
        /\       | |                                   / _|
       /  \      | |_    __ _   ___    ___      ___   | |_
      / /\ \     | __|  / _` | / __|  / _ \    / _ \  |  _|
     / ____ \    | |_  | (_| | \__ \ |  __/   | (_) | | |
    /_/    \_\    \__|  \__,_| |___/  \___|    \___/  |_|

       _            _  _  _      _  _  _  _            _
     _(_)_       _ (_)(_)(_) _  (_)(_)(_)(_)         _(_)_
   _(_) (_)_    (_)         (_)  (_)      (_)_     _(_) (_)_
 _(_)     (_)_  (_)    _  _  _   (_)        (_)  _(_)     (_)_
(_) _  _  _ (_) (_)   (_)(_)(_)  (_)        (_) (_) _  _  _ (_)
(_)(_)(_)(_)(_) (_)         (_)  (_)       _(_) (_)(_)(_)(_)(_)
(_)         (_) (_) _  _  _ (_)  (_)_  _  (_)   (_)         (_)
(_)         (_)    (_)(_)(_)(_) (_)(_)(_)(_)    (_)         (_)

how to get it

git clone --recursive https://github.com/cmcmA20/klac

if you already cloned it

git submodule update --init --recursive

First step

Open any .agda file with your editor and try to typecheck it

Setup your environment

Using Guix

  1. Install guix using your preferred method:
  1. Issue this command to launch emacs in environment:

    guix time-machine -C channels.scm -- shell --pure --manifest=manifest.scm -- emacs -q -l init.el

Using GHCup

  1. Install GHCup using official documentation.

  2. Install GHC and cabal:

    ghcup upgrade
    ghcup install ghc 9.2.4
    ghcup set ghc 9.2.4
    ghcup install cabal 3.6.2.0
    ghcup set cabal 3.6.2.0
    cabal update
  3. Install Agda, it may take a while:

    cabal install Agda-2.6.3
  4. Install libraries:

    stdlib

    git clone -b experimental_compat https://github.com/cmcmA20/agda-stdlib ~/.agda/agda-stdlib
    echo "$HOME/.agda/agda-stdlib/standard-library.agda-lib" >> ~/.agda/libraries

    generics

    git clone -b experimental_compat https://github.com/cmcmA20/generics ~/.agda/generics
    echo "$HOME/.agda/generics/generics.agda-lib" >> ~/.agda/libraries
  5. Use emacs as your editor (commands for debian/ubuntu):

    sudo apt update
    sudo apt install emacs -y
    agda-mode setup
    agda-mode compile
  6. If you want emacs agda2-mode to load by default when opening literate agda files, add this to emacs config:

    (add-to-list 'auto-mode-alist '("\\.lagda.org\\'" . agda2-mode))

Other methods

Contributions are welcome