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):
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
Kevin Buzzard (Mar 18 2020 at 23:24):
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:
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
Iocta (Mar 18 2020 at 23:36):
frames-only-mode makes it work
Iocta (Mar 19 2020 at 00: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):
Last updated: May 10 2021 at 17:39 UTC