which namespace am I in?

Stream: general

[Kevin Buzzard]

I'm using a mathlib library extensively today, with lots of namespaces, and I never know which one I'm in. I just edit my copy of _target/deps/mathlib, after lemma X : ... I write #print X and then I see the full name in the output, and then I ctrl-Z back to normality. Is there a better way of doing this?

[Johan Commelin]

import tactic.where at the top and then #where at the place you are interested in. Thanks to @Keeley Hoek.
It's too bad that the import is still necessary...

[Johan Commelin]

You were editing the file anyway, so apparently you aren't scared of triggering yellow bars in mathlib...

[Kevin Buzzard]

It's not ideal :-)

[Johan Commelin]

It would be awesome if one could inspect Lean without triggering a recompile

[Johan Commelin]

In theory this should be possible... all the info is in the .olean. But it would require interaction between VScode and Lean server mode that might not currently be possible...

[Johan Commelin]

@Gabriel Ebner Do you have any idea how hard it would be to implement such a thing?

[Kevin Buzzard]

I think my solution of #print [name] is easier than putting the import at the top

[Kevin Buzzard]

in my context

[Kevin Buzzard]

I can see that where is useful in other situations though :-) (e.g. when I get lost in my own file :-) )

[Jesse Michael Han]

TIL about #where, but I usually just do

run_cmd tactic.open_namespaces >>= tactic.trace

[Johan Commelin]

I guess that is part of what #where does. It still triggers yellow bars though...

[Kevin Buzzard]

I've realised I also want to know what variables have been declared and which namespaces are open!

[Kevin Buzzard]

What is happening is that I want to write a lemma in mathlib, and then take that lemma out of the mathlib file and rewrite it in a file of my own, with a note to add it to mathlib one day

[Kevin Buzzard]

All these things are issues for when I'm doing the porting.

[Kevin Buzzard]

I guess there's an argument for #where :-)

[Johan Commelin]

Right... #where tries to output code that is ready to copy and paste for exactly those situations

[Kevin Buzzard]

Yes I get it now :-) Thanks!

[Johan Commelin]

Sometimes it messes up the variable order...