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:

• Guix System: available out of the box;
• Arch Linux: see arch wiki;
• Debian GNU/Linux: guix is available since bullseye;
• Ubuntu: guix is available since impish
• Other distros: Use official binary distribution

2. 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