Zulip Chat Archive

Stream: new members

Topic: show tactic state

Iocta (Mar 18 2020 at 21:24):

When a tactic proof is complete, can I examine the tactic state at each step in emacs? The only way I've found to do this is just deleting the steps that follow the one I want to examine and looking at the flycheck buffer.

Kevin Buzzard (Mar 18 2020 at 21:25):

I'm not a Lean emacs user but there's definitely a better way. You can do it in VS Code so you can definitely do it in emacs -- you just move the cursor around but you need to be in the right "mode"

Iocta (Mar 18 2020 at 21:27):

C-c C-g brings up the "Lean goal" buffer but ... it's never got anything in it

Reid Barton (Mar 18 2020 at 21:27):

It should, if your cursor is in the middle of a tactic block

Reid Barton (Mar 18 2020 at 21:28):

There shouldn't be anything more to it than that...

Iocta (Mar 18 2020 at 21:29):

toggling lean-info mode or lean-debug mode doesn't seem to help

Reid Barton (Mar 18 2020 at 21:33):

I don't think I've ever witnessed this not working. Can you provide a screenshot just as a sanity check?

Iocta (Mar 18 2020 at 21:36):

what is the name of the buffer that the data appears in?

Reid Barton (Mar 18 2020 at 21:37):

*Lean Goal*

Iocta (Mar 18 2020 at 21:40):

Kevin Buzzard (Mar 18 2020 at 22:30):

Just to be clear, is your cursor in the middle of a multi-line tactic mode proof which has, say, one goal at all times?

Iocta (Mar 18 2020 at 23:20):

You can see the cursor box on the c of cases

Kevin Buzzard (Mar 18 2020 at 23:24):

vscode.png
VS Code with cursor in the same place. I'm 99.9% sure that when I tried emacs it was the same.

Kevin Buzzard (Mar 18 2020 at 23:25):

Oh I have Lean running in emacs on this computer:

emacs.png

Reid Barton (Mar 18 2020 at 23:27):

@Iocta Your emacs looks pretty customized, maybe something is interfering with lean-mode?

Iocta (Mar 18 2020 at 23:28):

Perhaps. that's an unpleasant rabbit hole but maybe necessary

Iocta (Mar 18 2020 at 23:29):

Do these look ok?
Lean (version 3.5.1, Release)
GNU Emacs 26.3
lean-mode-20191229.1613

Iocta (Mar 18 2020 at 23:36):

disabling frames-only-mode makes it work

Iocta (Mar 19 2020 at 00:23):

https://github.com/leanprover/lean-mode/pull/23

Iocta (Mar 19 2020 at 00:24):

Sent a PR to lean-mode

Iocta (Mar 19 2020 at 18:39):

Merged into master

Kevin Buzzard (Mar 19 2020 at 18:40):

Nice! Thanks.

Last updated: Dec 20 2023 at 11:08 UTC