search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
64 stars 28 forks source link

mention tactic state in README #63

Closed lambdaofgod closed 5 months ago

lambdaofgod commented 5 months ago

It might be useful to avoid confusion like in #62

bustercopley commented 5 months ago

Did you notice that the keybinding is already mentioned, in the "Key Bindings and Commands" section of README.txt?

lambdaofgod commented 5 months ago

Yes.

That's not the point though - as a first time user I didn't know what command should I run. I'd wager I'm not the only person who faced this problem.

bustercopley commented 5 months ago

A new user might not know what "show tactic state" means, either. Can you write something a bit longer, that will make the user think it is something they should try, and give them a clue about what will happen?

By the way, in VS Code, and in the video you linked in #62, "Tactic state" is a section heading, not the name of the tab/pane. In Emacs the buffer's name is *Lean Goals*, and the corresponding section heading is "Goals". I think we should talk about "showing the infoview".

lambdaofgod commented 5 months ago

While we're at it, maybe add a screenshot so people would see how it should look like? WDYT?

bustercopley commented 5 months ago

Maybe in a separate PR? I'm hesitant though, because the maintainers don't put much time into this repo and my guess is that easy, uncontroversial changes have a better chance of getting merged.

I don't know, maybe I'm being overcautious. @urkud?

urkud commented 5 months ago

I can review PRs on weekends and sometimes in the evening. Please ping me on zulip (mention or dm) when the pr is ready for review.