madman-bob / idris2-python

A Python backed for Idris 2
Other
19 stars 4 forks source link

[ refactor ] move module template to lib dir #4

Closed stefan-hoeck closed 2 years ago

stefan-hoeck commented 2 years ago

This moves the python stuff to directory lib where it can be picked up and installed by pack. Please note that I did not adjust the Makefile or install docs.

madman-bob commented 2 years ago

To avoid this repository depending on pack, I think it makes more sense for pack to have a config option for the libs dir.

ohad commented 2 years ago

I don't think putting these files in a different directory is introducing a hard dependency on pack.

  1. On the idris2-python side, it doesn't really matter under which subdirectory these files are located.
  2. Pack configuration files / .ipkg files should have a better support for installing resources, and hard-coded lib subdirectory is probably not a robust long-term solution.