Kuinka asentaa Agda ubuntu koneelle?
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.