When searching for packages, rule out incompatible TTC versions

[mattpolzin]

Description

Prior to this change, the first package matching version requirements would be used by the compiler -- if that package was only installed with an incompatible TTC version, it simply cannot be used. After this change, we skip package directories with only incompatible TTC versions which allows the compiler to find a farther down option (if one exists) in some other directory that does have a compatible TTC vesrion.

For example, if you've got an incompatible package named foo at ~/.idris2/idris2-0.7.0/foo-0/12345 and a compatible package at ~/extra/idris2/foo-0/56789 this PR allows the compiler to succeed given ~/extra/idris2 is in IDRIS2_PACKAGE_PATH. Prior to this PR, that would not have worked.

When a package is passed over due to incompatible TTC version, you see the following warning:

Warning: Found version 0 of package pg-idris-tests installed with no compatible binaries for the current Idris2 compiler.

Reinstall pg-idris-tests with the current Idris2 compiler to resolve the issue.

Note that for successful dependency resolution (not for dependency resolution failures) this warning is currently output twice. That's not great, but it's better than 0 warnings. The cause is two calls to the code that resolves package dependecies in two different parts of the build process. It's not trivial to squash because we only want the warning to emit when a dependency is used, so we don't want to cache/warn only on first crawl of a depedency directory (which may not be when we need a particular dependency), but that would be the easiest place to cache something. This isn't an unsolvable problem, just not one I am going to spend the time on at this moment for a warning that is pretty edge-case to begin with.

• Add a test.

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

[gallais]

This feels like it could have counter-intuitive results.
Any chance we can pre-emptively add a bit logging explaining the package selection strategy?
People can then turn it on if they want to see a rational for the behaviour they observe.

[mattpolzin]

Yeah logging is a good call. I wonder if this shouldn't even be a warning -- to have some packages only installed as incompatible binaries. Definitely already surprising prior to this PR to wonder why such a library simply isn't working.

[mattpolzin]

@gallais do you have a preference on warning vs. log message here before I get to the point of modifying tests to reflect the change? I like the warning because (a) it is formatted more boldly and (b) it gets logged unconditionally instead of only upon request. That said, if a warning feels too strong, I'm open to just logging it. Of course this is a sufficiently edge-case situation only occurring at most when the Idris compiler is updated without reinstalling existing packages so that also factors into my opinion of warning being a good fit.

[buzden]

I wasn't asked here, but still I feel warning to be good here