Are the # commands listed and documented somewhere?

Stream: new members

[Ching-Tsun Chou]

I know of #check, #eval, #synth, #print, and #simp. Is there a central place where all these # commands are listed and documented?

[Mario Carneiro]

Does #help command "#" do what you want?

[Edward van de Meent]

do note that not all commands start with #

[Edward van de Meent]

for example: whatsnew in

[Mario Carneiro]

#help command shows all commands, the ones with # are for "temporary" use (although arguably whatsnew should also be in that category)

[Edward van de Meent]

i seem to recall a different conversation where the distinction was suggested to be the fact that those with don't "alter the environment" or something like that?

[Edward van de Meent]

basically, i don't think this is very clear cut

[Mario Carneiro]

that's certainly not the case for #eval

[Mario Carneiro]

or example

[Mario Carneiro]

I think the intention of the convention is clear, but the execution isn't perfect

[Edward van de Meent]

i was thinking of #lean4 > why `whatsnew`?

[Mario Carneiro]

(I know that this is the meaning of the # because I have heard it said by the people who designed the syntax in the first place)

[Edward van de Meent]

something something descriptive/prescriptive language

[Edward van de Meent]

reading the conversation again, they do seem to agree that the commands with # are the ones which shouldn't stick around in non-testing code

[Mario Carneiro]

tests break this convention because it's not that strange to use an explicitly diagnostic-use-only command in a test

[Mario Carneiro]

almost all # commands also produce output via info messages

[Mario Carneiro]

which is another reason whatsnew seems like it should have a #

[Ching-Tsun Chou]

Thanks! I actually didn't know about #help. It is not mentioned in #mil or #tpil.

[Mario Carneiro]

you would have found it in the output of #help :upside_down:

[mars0i]

#help doesn't seem to work in nvim with lean.nvim. Why not document these on the web?

[Kevin Buzzard]

Probably because the naive approach ("just dump the output to a file and put it somewhere on the community website") leaves a maintenance burden (i.e. someone has to keep it up to date) and the clever way (keep running #help and posting the output to a file on the community website) requires someone to get the set-up working.

[Ching-Tsun Chou]

On the other hand, it would be nice if the #help command itself is mentioned in the introductory literature on Lean. So far as I can tell, it is not mentioned in any of the books listed here:

https://leanprover-community.github.io/learn.html

Indeed, I can find only a single mention of #synth in those books (in sec.7.1 of #mil) which does not make it clear that #synth is the command one can use to figure out what the type class system is doing.

[Mario Carneiro]

mars0i said:

#help doesn't seem to work in nvim with lean.nvim. Why not document these on the web?

I don't see any reason why that would be. Most likely you just don't have it imported (it's in Batteries.Tactic.HelpCmd)

[Mario Carneiro]

unfortunately lean core is rather cagey about documenting tactics that aren't shipped with lean itself, which IMO harms discoverability of things in mathlib

[Mario Carneiro]

books like #mil don't have the same constraints, but they are also aimed at a higher level of abstraction and kind of delegate some of the responsibility to document lower level things to lean core

[mars0i]

Thanks @Mario Carneiro. I didn't know #help needed an import. It does indeed work with that import. Another thing that I wish was noted in an obvious place!

For my own sake , I've been compiling a series of tips of various kinds for use and setup of Lean. Maybe I ought to clean it up and see whether various parts would be welcome somewhere on the wiki.