Customizing prelude for automatic imports?

Stream: general

[Lhr]

I am using lean4 as a host language for my own embedded language. As such there are libraries I've made which I essentially have to import in every single file in every codebase.

Is there any way for me to add my own libraries to the prelude that gets automatically inserted to every file, such that I never have to manually import my stuff and can have them globally available in my projects?

[Kim Morrison]

No, there is no such mechanism at present.

[Yury G. Kudryashov]

As a workaround, you can create 1 file that public imports them all, then import this file.

[Lhr]

I saw talk about such a feature as a future possibility before on other forum; what technical obstacles stand in the way for this?

[Yury G. Kudryashov]

Let me guess (disclaimer: it's a guess, not some insider knowledge): someone has to convince FRO that this feature is worth the extra maintainance costs it brings.

[Chris Henson]

One place where such a feature would be nice is ensuring that syntax linters are always available, as opposed to what Mathlib and CSLib currently do with ensuring their Init file is transitively imported everywhere. The error messages downstream can be pretty confusing if linting is set in the lakefile but you're missing the import.

[Sebastian Ullrich]

I'm considering whether this could be best implemented as a shake feature, in the sense that shake will ensure a given set of modules is imported everywhere they can (without creating cycles) in the project

[Lhr]

Apologies for my ignorance, I'm new around here. Why couldn't it be as simple as specifying some line in a lake file?

auto_imports = ["MyLib",  "MyOtherLib"]

And then every file in the codebase could be imagined as having an invisible 1st line containing the imports. Right before sending the file contents to the compiler, we would inject these import lines at the top as if the user had written them, without modifying their actual file contents. So, just a string prepending operation, file_contents' = auto_imports ++ file_contents. Is it much harder than this?

[Kim Morrison]

Yes, it is harder than this, in multiple directions. :-) Consider, for example, the module keyword, the processHeader function, python scripts reading imports, people copying and pasting for an #mwe, etc.