FAQ: Working on Idris

Sometimes while working with the compiler you might encounter some weird errors. Or sometimes you might wonder about how to do something specific. Here is a list of how to solve some of the most common problems.

I can't bootstrap! idris2-boot.so: no such file or directory

If you are not on linux and try running make bootstrap SCHEME=scheme you might find this error:

../../build/exec/idris2: line 9: realpath: command not found
usage: dirname path
Exception in load: failed for /idris2_app/idris2-boot.so: no such file or directory
make[2]: *** [all] Error 255
make[1]: *** [prelude] Error 2
make: *** [bootstrap-build] Error 2

This tells you that the bootstrapping process cannot find realpath, for this you need coreutils, you can install it on mac OS with brew install coreutils or by using your local package manager to download either realpath or coreutils.

More about how to install on the INSTALL.md tutorial.

How can I see logs of what the compiler is doing?

Add %logging n where n is your log-level. For example

module TestFile

%logging 5

If you are in the repl you can type :log n to change the log level for the current session

How do I fix Control.Delayed not found ?

Try invoking idris with -p contrib

Like this: idris2 -p contrib

How do I fix Network.Socket not found ?

Try invoking idris with -p network

Like this: idris2 -p network

None of these worked! What do I do?

If you're lucky, the libraries are compiled but not installed. Try running make install to fix this.

Otherwise you might have to bootstrap again. With

make bootstrap SCHEME=chez
make install

You can check which libraries are installed the idris prefix. Usually $(HOME)/.idris2/idris-0.2.0/ (idris-0.2.0 might be different if you're working on a higher version)

I added some fancy stuff to the compiler/standard libraries but CI complains when I use my new additions in the standard libs/compiler!

During continuous integration (CI) we verify that the current version of the compiler and standard libraries can be built both with the current bootstrap compiler and the latest release version of the compiler. Building with the bootstrap compiler goes through the following steps:

• build prelude
• build base (using previously built prelude)
• build contrib and other libs (using previously built prelude and base)
• build the Idris compiler using the previously built standard libraries

Since the bootstrap compiler does not come with its own sets of standard libraries, it must first build these before it can build the current Idris compiler. Therefore, the standard libraries must not use recent stuff, about which the bootstrap compiler knows nothing.

Building Idris with the latest release does the following:

• build the Idris compiler with the latest release compiler (using that compiler's version of the standard libraries)
• build the standard libraries with the freshly built Idris compiler

Therefore, the current compiler sources must not use data types or functions from the standard libraries that were not yet there in the latest release version.

So, if we add new stuff to the compiler, we must wait until the next (minor) release before this stuff can be used in the standard libraries. Likewise, if we add new stuff to the standard libraries, we must wait until the next minor release before this stuff can be used in the compiler sources. The latter means that we often have to temporarily duplicate new functions from the standard libraries in the compiler sources.