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.

Posted in Kerhoillat.

Vastaa