idrisidris2

Importing from the contrib library fails

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?

Solution

  • 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.