Idris standard library
Az Idris egy folyamatosan bővülő, általános célú szabványos könyvtárral rendelkezik. Ennek legfontosabb, kiemelendő elemei, részei, funkciói (inkább a nagyközönség érdeklődésének felkeltésére, mint a terminológia pontos használatára ügyelve):
- adatszerkezetek és algoritmusaik (vektor, stream, string, lista)
- monadikus programozáshoz kapcsolódó definíciók (Monad típusosztály, példányok)
- hasznos típusok (Either - unió, Maybe - kivétel, Fin - véges halmaz)
- IO kezelés (képernyő, fájlok)
- hasznos típusosztályok (Foldable, Functor, Traversable)
- helyességbizonyításhoz hasznos függvények
Érdekes információ, hogy ezen oldal elkészítésekor az Idrisben még nem volt lehetőség véletlenszámok előállítására, viszont az Idris közösség tagjai közül már többen is dolgoztak a probléma megoldásán. Ebből is látható, hogy az Idris standard library egy élő, fejlődő könyvtár.
Csomagok
Az Idris a 0.9.4-es verziótól tartalmaz egy egyszerű csomagkezelő rendszert is, amely képes csomagokat építeni csomagleíró-fájlok segítségével. A csomagleíró-fájlok kiterjesztése .ipkg kell legyen. Az összes modul fordítása egy adott csomagban:
idris --build csomag.ipkg
Csomag telepítése (ezután a csomag elérhető lesz minden más Idris program és könyvtár számára):
idris --install csomag.ipkg
A csomag fordítása közben keletkezett fájlok törlése:
idris --clean csomag.ipkg
Miután a csomagot telepítettük, a --package kapcsoló után írva a nevét elérhető lesz.
A csomagleíró-fájl felépítése, tartalma:
- fejléc a csomagnévvel
- mezők, melyek leírják a csomag tartalmát, field = value formátumban
Egy példa csomagra:
package csomag
modules = csomagmodul1, csomagmodul2