[fix] Package Search Paths

[mattpolzin]

Description

For a number of versions now it has been the case that two different concepts share the same name in the Idris2 build process:

1. Locations where packages are searched for (e.g. ~/.idris2/idris2-0.7.0)
2. Directories containing packages at the required versions for the current build (e.g. ~/.idris2/idris2-0.7.0/base-0.7.0)

The build context has stored both of these things as package_dirs until now. This mixed-use can be quite confusing. If you print idris2 --paths, you will see a mix of (1) and (2) in the output for "Package Directories." Despite this output, the two really are used differently. Adding a path to IDRIS2_PACKAGE_PATH will add it to that shared list, but it will only work (i.e. a package will only be discoverable due to the additional path) if you are specifying a path of type (1), not type (2).

This PR breaks the two concepts out. directories containing packages at resolved versions are still stored as package_dirs but directories within which packages should be searched for are stored as package_search_paths. They have their own line items in the output of idris2 --paths. IDRIS2_PACKAGE_PATH only affects package_search_paths.

This PR also takes the previously implicit "global" package search path and explicitly stores it in the package_search_paths. This is a small code cleanup, but it has the added benefit that the global search path is printed by idris2 --paths rather than being a hidden implementation detail.

The last thing this PR does is fix a bug already present in Idris2 that stopped the REPL :package "<name>" command from working. It must have stopped working way back when package ttc files started getting stored under a versioned subfolder because the fix was to pop the top directory off of the path when attempting to load a whole package at the REPL.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[mattpolzin]

@stefan-hoeck although this PR passes the pack tests, I still wanted to ping you since Pack has a more intimate relationship with Idris2's various paths than most projects.

[mattpolzin]

I'll merge this soon if no one objects in the interim.

[mattpolzin]

Note to self: explain this change in the CHANGELOG. [DONE]