Better constants extraction from REPL

Stream: general

[Riyaz Ahuja]

Hey everyone!

I was trying to see if there's any way to "upgrade" the repl's usedConstants feature, where tactics also contain info on constants from the current or imported modules. Afaik, the repl does this by just extracting an Expr from the metavar context that is stored in the TacticInfo node of the InfoTree.

This is different from how ntp-toolkit and #general > Extracting proof dependencies did it, where we instead had to import+compile all the modules we're interested in through some CoreM instance, and then could just get the constants map via (← getEnv).constants.map₁. On one hand, the repl method is super efficient since I'm already trying to extract out the theorems anyways, and I don't like the idea of having to have a seperate lean script that compiles the module, and then having to filter through the potentially giant constants map. However, the repl method only lists the Names of the constants, whereas with the constants map, you can get a lot more information such as the source file/text of the dependency and the kind of constant (theorem, def, etc.).

My question is whether it's possible/how to modify the repl to also extract out the source file/text/kind of the constants extracted from the metavar context that it's already parsing through. I don't want to have to recompile the whole module to do this, but I'm still a bit of a novice in figuring out how to extract the current Environment and constant map in the repl.

Any help or advice on this would be super appreciated!

[Riyaz Ahuja]

Update: It seems that we can extract the environment (and therefore the constants map) via CmdState.env.constants, where CmdState : Command.State is half of a CommandSnapshot. That's enough to figure out the source module and kind (def, theorem, etc). Now I'm interested in figuring out if we can also get a syntax range from the source module, so that we can do a quick substring to get the actual contents of the definition/theorem/whatever constant we're looking at.

Obviously, you could just (<- CompileModule m).flatMap .trees to get a bunch of subsequent infotrees, figure out which one added the constant you're interested in, and extract the contents from that. But that's horribly inefficient. I'll play around and see if there's a faster way to do this extraction.

[Sebastian Ullrich]

That's docs#Lean.findDeclarationRanges?