Инструкции за подготвяне за работа с Agda

agda-instructions.md

Подготовка за работа с Agda

0. Инсталирате си Emacs (по възможност използвайки package manager-а ви)

   Не съм сигурен как става под windows, но има инструкции на GNU сайта, както и в spacemacs github-a например. Или пък това?

За инсталиране на самата Agda има вариант или да се компилира, или да се използва пакет от системата.

Например за arch linux хората в AUR има обновен пакет, но тъй като много дистрибуции, например debian/ubuntu (особено stable вариантите им) са с по-стари версии на Agda, тук ще има инструкции за инсталация чрез ghc+cabal.

1. Инсталирваме си ghc + cabal (по възможност използвайки package manager-а ни)

   Тук може да имаме проблем ако сме с много стара версия на ghc (<8.0) или cabal.

2. Инсталирваме си alex и happy

   Това са програми изпълняващи същите роли като съответно lex и yacc.

   За да ги инталираме е достатъчно да изпълним cabal install alex happy.

   След това е хубаво да проверим дали ги има в PATH като се опитаме да ги извикаме.

   Най-вероятно ги нямаме - би трябвало да са инсталирани в ~/.cabal/bin, така че може да трябва да добавим този път на края на PATH-а ни.

   Попринцип cabal си казва къде се намират след като ги компилира.

3. Инсталирате си agda

   cabal install Agda - забележете че е с главна буква. Това ще отнеме малко време - идете да пиете кафе.

   Отново, тук важи същия коментар за PATH както при alex и happy, тъй като пак инсталираме с `cabal.

В този момент имаме нужните програми, остава ни само да ги "сглобим" за да работят заедно.

Тук предлагам два варианта:

• може да следвате инструкциите от сайта, които изглеждат доста кратки (май е само извикване на agda-mode setup)

• да използвате spacemacs - "дистрибуция" за емакс, която включва и множество "слоеве" които може да си пускате

  Аз лично използвам този вариант, защото spacemacs идва наготово с vim клавишни кобминации, с които съм свикнал.

Инструкции за spacemacs:

4. Инсталираме си spacemacs

   git clone https://github.com/syl20bnr/spacemacs ~/.emacs.d (взето от сайта им)

5. Минаваме на develop клона им - в него има новости свързани с новата версия на Agda, които не са интегрирани в master-а им все още

   cd ~/.emacs.d
   git checkout develop
   

6. Пускаме emacs за да се изтеглят нужните от spacemacs неща

   При първото пускане spacemacs ще ви пита за различни конфигурационни настройки, включително и дали искате vim-стил или emacs-стил клавишни комбинации.

   Мисля че няма значение много какво ще изберете тук, но може да разгледате ако ви е интересно.

   Това ще отнеме малко време.

7. Добавяме Agda към списъка от използвани слоеве Списъкът се казва dotspacemacs-configuration-layers - ако потърсите за низа ще намерите списък (lisp-ски) към който може на нов ред да добавите agda.

8. Правим проверка дали всичко работи като хората

   Отваряме Agda файл в Emacs и се опитваме да го заредим - с vim клавиши в spacemacs става чрез <SPC> m l. (<SPC> означава шпация). Ако файлът се оцвети, най-вероятно работи.

   Тук има клавишни комбинации за Agda с "нормален" Emacs. В този случай ни интересува C-c C-l

   Примерен файл (кръстете го Asdf.agda):

   module Asdf where
   
   data Foo : Set where
   
   record Bar (P : Foo -> Set) : Set where
     field
       x : Foo
       y : P x