Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

When searching for packages, rule out incompatible TTC versions #3444

Open
wants to merge 4 commits into
base: main
Choose a base branch
from

Conversation

mattpolzin
Copy link
Collaborator

@mattpolzin mattpolzin commented Dec 14, 2024

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

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.
@mattpolzin mattpolzin marked this pull request as ready for review December 16, 2024 11:00
src/Idris/SetOptions.idr Outdated Show resolved Hide resolved
@gallais
Copy link
Member

gallais commented Dec 17, 2024

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
Copy link
Collaborator Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants