idris-lang / Idris2

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

Flexible and lightweight specification of modules #2515

Open joelberkeley opened 2 years ago

joelberkeley commented 2 years ago

Summary

Allow developers to specify which modules to include in a library/executable with minimal effort and practical flexibility.

Motivation

Manually specifying modules to include via .ipkg modules is tiresome and error prone. I frequently find I've forgotten to add modules in my .ipkg file when I push to git remote.

The proposal

Currently, users can specify which modules to include. This would be much easier if there was some mechanism to say "I want everything in this directory". Glob patterns are a possible candidate.

Some people apparently like to be able to specify which files not to include. This of course is allowed in the current mechanism, by simply omitting such files. It could also be allowed with a clever use of glob patterns. It may well be simpler to simply say "I want to exclude these files". This could be as a simple list of files under an exclude section, or it could also allow globs. An exclude section may only be of use if we adopt globs in modules. If a file appears in exclude and is explicitly mentioned in modules, we could raise an error. I don't know if people would want to exclude non-Idris files. If they did, this would either need to be in a separate section of the ipkg file, or we'd need to change the format of exclude to include the file extension, rather than just the module names.

The above may well be backwards compatible.

I think this orthogonal to which directory modules are in (src, test etc.)

Examples

I want to include everything

modules = *

I want to include everything in the Foo module and package

modules =
    Foo
  , Foo.*

I want to include everything except Foo.Bar

modules = *
exclude = Foo.Bar

I want to include everything except the Bar package

modules = *
exclude = Bar.*

Technical implementation

Haven't thought about implementation.

Alternatives considered

I don't know any alternatives. I've based much of this off python's setup.py setup function, because I'm used to that.

As a first move, we could enable the simple pattern * (not Foo.* etc.) for modules. This would be backwards compatible with our current state, and remove the main difficulty I (anecdotally) see people facing. It think it would also be forwards compatible with the above.

iacore commented 2 years ago

We should also make idris2 --typecheck x.ipkg only load modules mentioned. Currently it loads anything in source folder and installed folder of other packages used.

The implementation should scan all the modules first, then decide which module to include. modules = *, !Test.* should work as expected (unlike .gitignore).