-
Инсталирате си Emacs (по възможност използвайки package manager-а ви)
Не съм сигурен как става под windows, но има инструкции на GNU сайта, както и в spacemacs github-a например. Или пък това?
За инсталиране на самата Agda има вариант или да се компилира, или да се използва пакет от системата.
Например за arch linux хората в AUR има обновен пакет, но тъй като много дистрибуции, например debian/ubuntu (особено stable вариантите им)
са с по-стари версии на Agda, тук ще има инструкции за инсталация чрез ghc
+cabal
.
-
Инсталирваме си
ghc
+cabal
(по възможност използвайки package manager-а ни)Тук може да имаме проблем ако сме с много стара версия на
ghc
(<8.0
) илиcabal
. -
Инсталирваме си
alex
иhappy
Това са програми изпълняващи същите роли като съответно
lex
иyacc
.За да ги инталираме е достатъчно да изпълним
cabal install alex happy
.След това е хубаво да проверим дали ги има в
PATH
като се опитаме да ги извикаме.Най-вероятно ги нямаме - би трябвало да са инсталирани в
~/.cabal/bin
, така че може да трябва да добавим този път на края наPATH
-а ни.Попринцип
cabal
си казва къде се намират след като ги компилира. -
Инсталирате си
agda
cabal install Agda
- забележете че е с главна буква. Това ще отнеме малко време - идете да пиете кафе.Отново, тук важи същия коментар за
PATH
както приalex
иhappy
, тъй като пак инсталираме с `cabal.
В този момент имаме нужните програми, остава ни само да ги "сглобим" за да работят заедно.
Тук предлагам два варианта:
-
може да следвате инструкциите от сайта, които изглеждат доста кратки (май е само извикване на
agda-mode setup
) -
да използвате spacemacs - "дистрибуция" за емакс, която включва и множество "слоеве" които може да си пускате
Аз лично използвам този вариант, защото
spacemacs
идва наготово с vim клавишни кобминации, с които съм свикнал.
Инструкции за spacemacs
:
-
Инсталираме си
spacemacs
git clone https://github.com/syl20bnr/spacemacs ~/.emacs.d
(взето от сайта им) -
Минаваме на
develop
клона им - в него има новости свързани с новата версия наAgda
, които не са интегрирани вmaster
-а им все ощеcd ~/.emacs.d git checkout develop
-
Пускаме
emacs
за да се изтеглят нужните отspacemacs
нещаПри първото пускане
spacemacs
ще ви пита за различни конфигурационни настройки, включително и дали искате vim-стил или emacs-стил клавишни комбинации.Мисля че няма значение много какво ще изберете тук, но може да разгледате ако ви е интересно.
Това ще отнеме малко време.
-
Добавяме
Agda
към списъка от използвани слоеве Списъкът се казваdotspacemacs-configuration-layers
- ако потърсите за низа ще намерите списък (lisp-ски) към който може на нов ред да добавитеagda
. -
Правим проверка дали всичко работи като хората
Отваряме
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