package manager for idris,in idris
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.

Join the chat at

ikan : package manager for idris,in idris

a example build file is at src/build.idr

execution of build file : src/Package/IkanExecute.idr

packages will be hosted here: , please email me if you would like to help manage the packages. Basically, the packages this org forked would be available to ikan.

The user api is mainly monadic, using free monads, which easily allows multiple kinds of analysis and interpretation.The philosophy is emacs like,that ikan just acts like a library.

General discuss about idris package manager is here

Currently Implemented

create new project with .ipkg template

new file/module


clone and cd into this repo

idris --build ikan.ipkg

and then move or symlink generated bin ikan to your path


├── src
│   ├── Main.idr main entry
│   └── Package
│       ├── IkanAssets.idr  templates for new project ,etc
│       ├── IkanAst.idr
│       ├── IpkgAst.idr
│       └── IpkgParser.idr

Why is it named ikan

kan extensions subsume all concepts in 1-dimensional category theory(by Mac Lane), and this project will use freer monads, which are closely connected to kan extensions. However, using ikan will assume no knowledge of any category theory, you just have to be familiar with do notation and functional programming.

Planned functionality

any thing is put at a central place , ~/.idris-ikan ,which keeps your project directory clean

sandboxed environment for every project

multiple backends , js,jvm,etc,and library management

multiple version resolution methods, via git commit specification or automatic

build,install to local ,clean,list all pkgs

generate template project

zsh integration

a website (currently everything will be put at , contact me if you want to manage packages!)

The big picture

The entry main : PkgIO () is just the IO () for our package manager (We may just use plain old IO () instead. However we do not do actions in IO directly, any operations would be implemented DSLs (deep embedding), which makes it convenient to do multiple kinds of interpretation, and allows a comprehensive way of viewing what happens at building.

The reason for this kind of separation is that we can perform any analysis or inspection before actually performing it. Although the theories behind free monads are frightening, its usage is quite simple, and as users you will only see a simple monadic interface.


Some examples of freer monadic DSL can be found at

repo hosting : just use git repos forked by idris-industry

convert from/to .ipkg


install idris-free package with freer (not merged yet)

Ideas to draw from

scala 's mill and sbt :

haskell's shake build

clojure :

Build Systems à la Carte(Haskell shake build) :

Existing idris pm

Contribution welcomed!