search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.52k stars 375 forks source link

--install-with-src should include ipkg and ttm files #2216

Open michaelmesser opened 2 years ago

michaelmesser commented 2 years ago

--install-with-src should include ipkg and ttm files. This would allow editor functions such as semantic highlighting and jump to definition when viewing source files of install packages. The ipkg may also have to be modified to have correct build and source directories.

michaelmesser commented 2 years ago

Would a PR for this be accepted? Or is there a better way to solve this?

gallais commented 2 years ago

I think a better approach would be to design a ttp binary file format that would contain

  1. the relevant information from .ipkg
  2. potentially some additional metadata that would be useful (e.g. a map of all of the exported names and the module they're defined in which could help with out-of-scope issues by suggesting the addition of missing imports)