Importing from the contrib library fails

Question

I'm following the TDD book in Idris 2, and the online documentation gives the following advice:

For the VList view in the exercise 4 after Chapter 10-2 import Data.List.Views.Extra from contrib library.

So I put this import in a source file (example.idr)

import Data.List.Views.Extra

But running idris2 example.idr fails with

Error: Module Data.List.Views.Extra not found

I believe the contrib library is correctly installed, because contrib (0.5.1) appears in the list printed by idris2 --list-packages.

How can Idris 2 be made to accept imports from the contrib library?

Answer 1

In addition to explicitly providing -p on the command line (as in this answer), you can also define a package for your project, using an IPKG file, wherein you can specify your dependencies.

Minimal example, to be placed in the top-level directory of your project:

package type-driven-development
depends = contrib

Then you can invoke Idris 2 with idris2 --find-ipkg Example.idr, and all of the depends will be included as if you had specified -p for each one.

The Idris 2 CLI also can generate a template IPKG file for you. The idris2 --init command will provide you with interactive prompts in order to fill in some basic values.

Answer 2

The idris2 binary accepts a --package or -p argument to add a package as a dependency.

Invoking the interpreter with idris2 -p contrib example.idr allows the import to be resolved correctly.