Funktsionaalprogrammeerimine 2025/26 sügis

Praktikum 0 - Tarkvara paigaldus

Toome välja mõned näited, kuidas Idris2 installida. Võite kasutada teisi meetodeid -- peamine, et teil oleks töötav Idris2 REPL (i.k. read-eval-print loop) ja mingi koodiredaktor. Alles viimastes praktikumides on ülesanded, mida on soovitatav lahendada plugin-at kasutades. Kui tarkvara paigaldamine õnnestus, saate läbida allpool toodud harjutuse.

Mac OS X - Intel (Homebrew)

 brew install rlwrap
 brew install idris2

Windows 10/11 (WSL)

• Paigaldada WSL
  • Open PowerShell in administrator mode by right-clicking and selecting "Run as administrator", enter the "wsl --install" command, then restart your machine.
• Installida nixos süsteem kasutades WSL käsurida (või PowerShellis käsk wsl):

 sh <(curl -L https://nixos.org/nix/install) --daemon
 exit

• Installida Idris2 ja rlwrap kasutades WSL käsurida (või PowerShellis käsk wsl):

 nix-env -i idris2
 nix-env -i rlwrap

• Installida VS Code Windowsi (vt. õpetust all)

Windows (mitte WSL)

• Õpetused TalTech-i FP kursusest: https://cs.taltech.ee/staff/iavara/idris/
• Muidugi töötab ka VirtualBox+Ubuntu-22.04 aga siis peate ka VS Code linuxisse installima.

Linux (nix)

Käsureal täita järgnevad käsud. Esimene käsk installib nixos-i siis tuleb terminal sulgeda ja uuesti avada. Kolmas käsk installib idris2-e.

 sh <(curl -L https://nixos.org/nix/install) --daemon
 exit
 nix-env -i idris2
 nix-env -i rlwrap

Ubuntu (apt) kui nix ei tööta

 sudo apt update
 sudo apt install chezscheme git build-essential libgmp-dev rlwrap
 wget https://github.com/idris-lang/Idris2/archive/refs/tags/v0.7.0.tar.gz
 tar -xvzf v0.7.0.tar.gz
 cd Idris2-0.7.0
 make bootstrap SCHEME=scheme
 make install
 cd ..
 echo 'export PATH="$HOME/.idris2/bin:$PATH"' >> ~/.bashrc
 echo 'export LD_LIBRARY_PATH="$HOME/.idris2/lib:$LD_LIBRARY_PATH"' >> ~/.bashrc

Visual Studio Code (WSL)

1. Lae alla ja paigalda VS Code
2. Käivita VS Code
3. Paigalda VS Code laiendus (extension) "WSL"
4. Sulge VS Code
5. Ava linux-i käsurida (näiteks Windowsi menüüst WSL või PowerShellist käsk "wsl")
6. Käsureal mine oma wsl-i kodukataloogi ja ava seal VSCode

   cd 
   code . 
   

7. Paigalda laiendus "Idris Language" (meraymond)
8. Veendu, et laiendus oleks installitud WSL:Ubuntu alla --- VS Code peaks ütlema "Extension is enabled on 'WSL:Ubuntu'"
9. Laienduse vaates vajuta hammasratta (Manage) peal ja vajuta 'Settings'
   • Sätetes vali: Idris2 Mode ja Idris Path pane "idris2"
   • Sulge sätted

Lõpuks on vaja konfigureerida klahvikombinatsioonid

• Ava: File -> Preferences -> Keyboard Shortcuts ning kirjuta otsingusse "Idris"
• Seadista klahvikobinatsioonid vastavalt enda soovile, näiteks
  • Idris: Case Split | Ctrl + Alt + C
  • Idris: Proof Search | Ctrl + Alt + P

Arendamisel avage VS Code-s vastav kataloog (kui avate ainult faili siis ei pruugi laiendus töötada)

• Näiteks WSL käsurealt: codium .

Märkus: Kuna VSCode laiendus "WSL" on arendatud Microsofti poolt, siis VS Codium-is seda avalikult ei leia. Selle saab küll tööle, kui VSCode-st alla tõmmata WSL laienduse VSIX fail ja see siis see VSIX fail VSCodiumis installida.

Visual Studio Code/Codium (mitte-WSL)

1. Lae alla ja paigalda VS Code või VS Codium
2. Paigalda laiendus "Idris Language" (meraymond)
3. Laienduse vaates vajuta hammasratta (Manage) peal ja vajuta 'Settings'
   • Sätetes vali: Idris2 Mode ja Idris Path pane "idris2"
   • Sulge sätted

Konfigureeri klahvikombinatsioonid

• Ava: File -> Preferences -> Keyboard Shortcuts ning kirjuta otsingusse "Idris"
• Seadista klahvikobinatsioonid vastavalt enda soovile, näiteks
  • Idris: Case Split | Ctrl + Alt + C
  • Idris: Proof Search | Ctrl + Alt + P

VIM

• Idrise looja Edwin Brady kasutab arendamiseks oma vim-i režiimi

Töökeskkonna tutvustus

Selle kursuse ülesandeid on mugav lahendada selliselt, et samal ajal on lahti koodiredaktor (näiteks VS Codium) ja käsurida/terminal Idris2 REPL-ga. Suurema monitoriga/ekraanilahutusega saavad need aknad olla kõrvuti. Sülearvutil võib olla mugavam kui mõlemad on täisekraanis s.t. vahetada nende vahel Alt-Tab/Command-Tab ga.

Tehke läbi järgnev lühike harjutus:

1. Avage käsurida, kus saate idrist käivitada.
2. Minge käsureal kataloogi, kus te tahate hoida kursuste materjale.
3. Looge uus kataloog: mkdir idris_test
4. Minge sinna kataloogi: cd idris_test
5. Looge fail test0: touch test0.idr
6. Avage VSCode: code .
7. Käivitage REPL: rlwrap idris2 test0.idr
   • Kui teil ei õnnestunud rlwrap-i installimine, siis kasutage lihtsalt idris2 test0.idr
8. REPL-is arvutage midagi: 5+5+5
9. Kopeerige järgnev kood VSCode-s avatud faili (ärge salvestamist unustage)

 liida5 : Int -> Int
 liida5 x = x+5

9. Laadige REPL-is fail uuest: :r
10. REPL-is arvutage: liida5 (5+5)
11. Hõljuge hiirega liida5 kohal
    • Peaks tekkima kastike Main.liida5: Int -> Int
12. Lisage faili lõppu kommentaar -- liida5 1
13. Selekteerige redaktoris avaldis liida5 1, vajutage klahvikombinatsioon Ctrl-Alt-i
    • Peaks tekkima juurde => 6
14. Sule REPL: :q