Combining Envs

Stream: lean4

[Adam Topaz]

Suppose I have a lean file with some imports at the top, and later in the file I obtain an environment env from the ether (doesn't really matter how). Do we have something that will update the environment of the given file by incorporating env?

It seems that docs#Lean.importModules has some logic for this internally, but I can't find any standalone functions of this sort.

[Alex J. Best]

You want to update the environment in the current file? There is docs#Lean.setEnv, does that work in your situation?
Ah you want to combine them meaning union the declarations and such? That I don't know

[Adam Topaz]

Yeah I suppose I just want to add a bunch of declarations, so I could use docs#Lean.Environment.addDecl with setEnv and some for loop

[Kyle Miller]

Do you want to merge the entire environment, or are you just wanting to add in the "map₂" entries (i.e., the module-specific entries)?

[Adam Topaz]

To un-xy, what I want to do is to write a command that fetches some lean project from github, compiles a certain file to obtain an environment, and adds the necessary declarations from that environment to the current file's environment. I already have some code that obtains the environment, and I suppose docs#Lean.addDecl should suffice? I'm thinking of this as an "ad hoc" import. Kyle, I'm not sure what you mean by map_2...

[Joachim Breitner]

Can you un-xy further? Do you expect that everything works as if you import’ed the file normally (e.g. #eval etc), or do want to do something more narrow?

[Kyle Miller]

(The hash map env.constants.map₂ consists of the constants defined in the current module, and none of the constants that have been imported by the module.)

[Kyle Miller]

Do you just want the declarations? Or do you need attributes and environment extensions too? (My understanding is that you can't add any new environment extensions to the current environment -- they're finalized right after the import block.)

[Adam Topaz]

That's right Kyle, just the declarations, so it won't actually work in the same way as an import command.

[Adam Topaz]

I hope it would be possible to #eval, but I don't know the internals well enough to be sure. I guess I'll just try it out :)

[Adam Topaz]

Here's one use case I have in mind: When working on some file in mathlib and I want help from GPT37, I would call

import_git "https://github.com/leanprover-community/gpt37_ftw" "Main.lean" -- or something

and be able to use whatever tactics that file introduces without modifying the lakefile to add another dependency.

[Adam Topaz]

Once I'm done with that file, I would delete that line.

[Sebastian Ullrich]

The robust way to solve this would be some kind of user-wide plugin support in Lake that would automatically be loaded into any server process

[Adam Topaz]

Ok, that's way beyond my paygrade :)

[Sebastian Ullrich]

Ultimately I believe it's a far easier problem to solve than importing things in the middle of a file :)

[Adam Topaz]

Can you say more about what you envision such user-wide Lake plugins would look like?

[Sebastian Ullrich]

Effectively a plugin (as in lean --plugin) is just a package that injects code into the server -- such as a parser and elaborator for some helper command. The remaining task is to register and manage these plugins per user, and to load them into the server automatically after compiling them for that Lean version

[Adam Topaz]

Can you point me to an example of an existing plugin that I can look at?

[Adam Topaz]

I played around with the very naive approach of using docs#Lean.addAndCompile but, as expected, I hit an issue when some declaration depends on another one. Do we have some function which takes a docs#Lean.Declaration and returns all the declarations that it depends on, the ones those depend on, etc., organized in a tree-like structure?