Table of Contents
- I can't bootstrap! idris2-boot.so: no such file or directory
- How can I see logs of what the compiler is doing?
- How do I fix Control.Delayed not found ?
- How do I fix Network.Socket not found ?
- None of these worked! What do I do?
- I added some fancy stuff to the compiler/standard libraries but CI complains when I use my new additions in the standard libs/compiler!
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.
- Wiki Home Page
- Using Idris
- Working on Idris
- Proposed changes