Getting started

Installation

Via apt

Agdalache is available as an apt repo! For installing from there, issue these commands:

echo 'deb [arch=amd64 signed-by=/etc/apt/keyrings/csimmaviktor.gpg] https://agda-sdk-apt.web.app/ unstable main' | sudo tee /etc/apt/sources.list.d/agdasdk.list
curl -fsSL https://csimmaviktor.web.elte.hu/apt-key.gpg | sudo gpg --dearmor -o /etc/apt/keyrings/csimmaviktor.gpg
sudo apt update
sudo apt install agdasdk

Afterwards, you should add the agda2hs library to your AGDA_LIB/libraries file (see details here). So, for Linux:

mkdir -p ~/.config/agda
echo "/usr/share/x86_64-linux-ghc-9.4.8/Agda-2.6.4.3/lib/prim/agda-builtins.agda-lib
/usr/share/agda2hs/agda2hs.agda-lib" | tee -a ~/.config/agda/libraries

For configuring Emacs, you don’t need to install an Agda instance; simply copy this to your .emacs file:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
(custom-set-variables
 '(agda2-program-name "agda2hs")
)

(require 'package)
(package-initialize)

Via the installation scripts

The installation scripts can be found in the repo itself (which you will probably want to use). These scripts download all the necessary tools directly from their producers. This means:

  • GHC;

  • agda2hs (commit acb521e on master has been tested to work with Agdalache);

  • Qt (a version that is compatible with the machine code produced by GHC).

So, to install this kit, do the following:

  • Clone the repository (of course, you need Git for this) by saying:

    git clone https://github.com/viktorcsimma/skeleton

Or you can also fork the repo on GitHub and work on your fork from then on. * Switch to the root of the repo with cd. * Run the appropriate installation script: sh install.sh on Linux or the PowerShell script on Windows. (For the latter, you might need to modify some security settings in order for this to work.) And you are now set and done!

Alternatively, you can also download the tools yourself. In this case, make sure you have

  • the custom agda2hs fork available on the the-agda-sdk branch of github.com/viktorcsimma/agda2hs;

  • a Qt version compatible with GHC-generated libraries (that is, linux_gcc_64 on Linux and win64_llvm_mingw on Windows).

First project

To start, simply use the skeleton repo cloned in the previous step (you can change the origin, fork the repository, or create a new one, if you wish).

You may, however, want to change the project name from the ugly and simple “skeleton” to a more appealing one. To do so, follow the steps in this commit diff.

An automatised script for doing this would be welcome!