feat(command): Add #where command, dumping environment info

[khoek]

Add the #where command.

The command tells you your current namespace (wherever you write it),
the current includes, and the current variables (variables must have been
used at least once).

Some spurious name manipulation and lean.parser code-generation facilities have been added to tactic/basic.lean for this purpose. (Maybe a tactic/parser.lean file will be eventually be warranted?)

We also add a few useful parser library functions (at the bottom of tactic.where): e.g. If you're in the lean.parser monad you can just call get_namespace to retrieve the name of the current namespace. If you're defining a tactic, you can add (p : interactive.parse lean.parser.get_namespace) to its parameters to parse the name p of the current namespace.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[jcommelin]

I gave this a little spin, and I think it is going to be really useful. But I couldn't fully understand the results. Here is what I did.
I went to data/nat/basic.lean, and added import tactic.where on line 9. On line 17 I added #where.
This printed

namespace: nat
variables: {m : ℕ} {n : ℕ} (m : ℕ) (n : ℕ) {k : ℕ} (k : ℕ) (n : less_than_or_equal #4 #0) (n : less_than_or_equal #2 #0)

The namespace is as expected, but there is a lot of duplication in the variables. Also, I have no idea what the less_than_or_equal stuff means.
So, kudos for giving us this information! Because this is already going to help me quite often when I'm totally lost about the environment I'm in. But this test got me thinking, and maybe there is some room for improvement. (But I don't know if this is feasible...)
What would be really useful is if one could just copy paste the variables line to setup an environment. (In particular I suggest removing the colons after namespace and variables.)
Typical use case: I want to add something about categorical limits, but the file about categorical limits is currently being PR'd. I don't want to add to this PR, so I want to add it in some misc file. If I could just type #where at the point in the limits file where I would have liked to add my stuff, and then copy paste the environment to the misc file, that would be very useful! It just reduces the mental effort of thinking which variables etc I need to add. And in the parts that are higher up in the hierarchy you sometimes need to set up some 10 variables before you can make useful statements.
Please let me know if something like this is possible!

[khoek]

Hi @jcommelin sorry, I didn't think of this. The problems + garbage in there is highly fixable. I'll try to do it today.

[khoek]

@jcommelin Should be all fixed now. You should now see exactly what you expected (and was intended---plus your nice "namespace" suggestion).

[rwbarton]

Could we make this exported by tactic.interactive? Then it will be available in almost all mathlib files by default, which would be more convenient.

[khoek]

Done

[jcommelin]

Here's a typical piece of output that I got

namespace category_theory.limits

variables {K : Type ?} {C : Type ?} {J : Type ?} [𝒞 : category C] [𝒦 : small_category K] [_inst_1 : small_category J]
include C 𝒞 K 𝒦



end category_theory.limits

I think this is really helpful. However, as you can see, it didn't figure out the universe parameters. Is that within reach?
(Also, you could consider hiding the "_inst_1 : " string, but I don't know if that is actually a good idea or not.)

[robertylewis]

@johoelzl @digama0 This PR looks good to me. @khoek were you planning to add anything else?

[khoek]

@robertylewis No, everything should be in there now. Just so that it is recorded here, I fixed Johan's problem and added the [_inst_1 : xxx] feature he suggested in the force push after his comment.

[rwbarton]

I don't think this should be imported with the default set. It's a transitory command, so it won't be needed in most of mathlib. Perhaps we should have an import set for transitory commands like #find and #where but they shouldn't be imported in basic files that don't need them.

Hmm, I think this will significantly hamper the convenience of #where. Instead of just editing the file at the point I care about, now I have to add an import at the top at the file as well (possibly triggering a bunch of recompilation which Lean otherwise wouldn't do?) and also remember to remove it when I'm done. I mostly imagine using this temporarily in mathlib files I'm not editing, but where I want to understand the types of the lemmas, or set up the same variable environment in my own files.

I also predict that if this command is not imported by default, then you will start receiving PRs with import tactic.where in them and have to tell people to delete that line. This alone makes it worthwhile to import by default I think.

[digama0]

I agree that people will accidentally import tactic.where, but that doesn't make it a good reason to import by default. It's like adding debugging imports - they should be removed before going into "production". Conceivably lean could support these kinds of imports through a command line --debug option, but currently the easiest way to express this kind of thing is through imports.

[jcommelin]

I completely agree with Reid. I understand Mario's objections, but they are in some sense ideological, I think. From a practical point of view, #where should always be available, immediately.

[rwbarton]

#check is the same kind of transient debugging command as #where yet it doesn't require an import. Sure, #check is a native Lean command while #where is implemented as a user command, but that's only because we didn't have the option to implement it natively in C++ (I'm sure it would have been easier!)

If you were implementing #where as a built-in command, wouldn't you make it always available, without requiring any imports or anything? In that case, why should we not try to approximate that hypothetical situation as closely as we can given the options which are open to us?

[khoek]

It'd be cool to be able to tell VSCode to import some files by default which change how some pieces of the environment work

[jcommelin]

Wouldn't those new imports trigger massive recompilation?

[khoek]

Sure
But they could be your own personal like debug-imports
Just an idea

[khoek]

All fixed up now. :)