Ide index

[hakanaras]

Description

Previously IdeMode was not able to suggest completions for symbols outside of what is already imported.

This PR adds a new command line option --ide-index, which:

1. Implies --ide-mode, if neither --ide-mode nor --ide-mode-socket is set.
2. Reads all TTC files from all package_dirs and places their public definitions into ROpts before starting the IdeMode loop.
3. When providing completions, in addition to symbols from the current context, now also returns public symbols from this new index along with the module identifier that has to be imported to make the symbol accessible.

I've also tried out the new functionality in a fork of meraymond2/idris-vscode, and will be creating a pull request there if this gets merged. I've not done anything for the emacs-mode or other tools.

The auto-import completions are just the first of multiple IDE features that could benefit from such an index.

Behaviour should be unchanged as long as --ide-index is not set.

Demo:

ide-index-auto-import-demo.mov

Things I'm unsure of:

• This will almost certainly impact performance of IdeMode. On my MacBook Pro I felt no difference, but on older machines this might be prohibitively expensive. It is opt-in though.
• I had to export some previously private functions in Core.Binary to help with loading the TTC files. Might be better to use the function readFromTTC, which was already exported?
• I call it an index, but really it's just a list of GlobalDefs. Not sure how much memory that's guzzling.
• Currently only indexes definitions from package_dirs, not from the current package.
• This is my first time contributing. I might generally be doing some things catastrophically wrong.

Self-check

• This is my first time contributing, I've carefully read CONTRIBUTING.md
  and I've updated CONTRIBUTORS.md with my name.
• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md

[hakanaras]

I had to export some previously private functions in Core.Binary to help with loading the TTC files. Might be better to use the function readFromTTC, which was already exported?

Actually not as simple as just using readFromTTC. We need the currentNS from the TTCFile, otherwise we can't get the module to import from the Name/GlobalDef later it seems.

[hakanaras]

Made some changes as recommended by dunham on Discord.

• Now uses the already exported readFromTTC from Core.Binary. (The module identifier/namespace is now determined based on the file path of the ttc file that is being read.)
• If one module re-exports another, now both modules are suggested as auto-imports. The list of re-exports is also added to the IDEIndex for other features to use.

Bildschirmaufnahme.2025-09-07.um.12.48.40.mov