Eipä ollut ollenkaan niin helppoa asentaa kuin olisi voinut
kuvitella. Tässä suurinpiirtein vaiheet, jotka itse tarvitsin toimivan
lopputuloksen saavuttamiseksi. Kannattaa varmaan ohessa myös katsella
agdan virallisia ohjeita. Jostakin syystä agdan stdlib ei ainakaan
minulla tullut automaattisesti mukaan joten myös agdan
kirjastoriippuvuuksiin kannattaa perehtyä.

Agda version 2.6.1.1

GNU Emacs 26.3

Stack 2.3.3

Ubuntu 20.04

Asensin agdan haskell tool stackin kautta.

Pistä muistiin mihin tiedostosijaintiin stack asensi Agdan.

Rammia asennus käytti ~ 6GB että pidä hatustasi kiinni ja sulje
kaikki ylimäräinen. Ja jos alkaa näyttää pahalta niin sammuta
“tarpeelliset” softat kanssa. Asennus testatusti kaatui rammin
loppumiseen.

stack update

stack install Agda

Lataa https://github.com/agda/agda-stdlib.git stackin asennus
sijaintiin, joka on jotakin suuntaan :
~/.stack/snapshots/x86_64-linux-tinfo6/asakfasdklja...asdjasdkljaskkfj/8.8.4/share/x86_64-linux-ghc-8.8.4/Agda-2.6.1.1/lib

En ole ihan varma täytyykö tuon olla juurikin tuolla. Periaatteesa
ainakaan ei.

Tee kansioon ~/.agda tiedostot:

defaults

sisällöllä:

standard-library

Kertoo mitkä paketit otetaan agdan buildiin defaulttina mukaan.

sekä

libraries

jossa sisältönä pathin stackin agda kansioon asenettun standard
kirjaston standard-library.agda-lib tiedostoon:

/home/esko/.stack/snapshots/x86_64-linux-tinfo6/asdklasjdklasdaslk...asdasjdhkajshdk/8.8.4/share/x86_64-linux-ghc-8.8.4/Agda-2.6.1.1/lib/agda-stdlib/standard-library.agda-lib

Sitten asensin aptista agda-stdlib paketin. En kuitenkaan saanut sitä
toimimaan itsessään, vaan asensin sen jotta sain kaikki sen vaatimat
riippuvuudet kasaan. siirsin varsinaisen kansion /usr/share/agda-stdlib
sijainnista /usr/share/agda-stdlib-notUsed. Jos kansiota ei siirrä, niin
bootin jälkeen Agda vaikuttaa kaatuvan päälekkäisiin riippuvuuksiin.

Seuraavaksi ajoin komennon varmistaakseni, että asennuksen pitäisi
olla emacsille kunnossa

agda-mode setup

lisäksi lisäsin .emacs tiedostoon rivit


(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))

Kokeillin ajaa tämän myös agda-mode locate ja se
toimi.

Seuraavaksi johonkin emacsilla tiedosto hello.agda sisällöllä:


module hello where

open import IO

main = run (putStrLn "päeveä mualima")

Sitten ajat M-x agda2-load tai C-c C-l ja
jos näyttää vähän aikaa, että juuri mitään ei tapahdu, niin kaikki menee
niinkuin pitää. Jos saat virheen niin jokin on pielessä. Tekstin pitäisi
värjäytyä kivasti, juuri niin että että kaikki oleellinen teksti on
suunnilleen saman väristä, kuin tumman teemasi tausta.

Tämän jälkeen voit myös kokeilla kääntää ohjelman agdalla:

agda --compile hello.agda

ja kansioon pitäisi ilmestuä ajettava tiedosto.

Sitten voit alkaa käydä läpi kirjaa: https://plfa.github.io/ ainakin tämä
on minun suunnitelmani.