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

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.