Feature request: Custom prelude

[siddhartha-gadgil]

• In a few contexts, it would be helpful if in addition to Init another file can be loaded before each file.
• This can be a command-line option
• In addition, Lake can have a convenient way to specify this.

[ydewit]

Is this something that can/should be done per module in the same way that, for instance, Racket does it? Or this feature request implies an all-or-nothing proposition (all modules in a package) for now?

For instance, this shows examples of how modules can customize prelude (and a prepackaged set of macros, notations available out of the box by adding a #lang ... to each module) in Racket. Or the specific prelude can be automatically inferred by the module (file) extension based on installed packages.

[digama0]

I would expect this to be a command line flag which is controlled by lake, so it could be per-file but it would probably be a global setting for the package. It would not be controlled by syntax in the lean file, that defeats the purpose (because the syntax could just be import MyInit).

[siddhartha-gadgil]

I would expect this to be a command line flag which is controlled by lake, so it could be per-file but it would probably be a global setting for the package. It would not be controlled by syntax in the lean file, that defeats the purpose (because the syntax could just be import MyInit).

Yes indeed. This is only to avoid having a separate import in each file.