Stream: Beginner Questions

Topic: No proof state in vscode


view this post on Zulip Zhiliang Chen (Nov 08 2022 at 17:42):

Hi, I installed the 2022 version of Isabelle. However, the vscode does not show proof state, but other things seem fine. Does anyone have an idea how I can resolve this problem? Jedit does not have this problem, but I want to use vscode :(.
I use ArchLinux btw.

view this post on Zulip Mathias Fleury (Nov 08 2022 at 17:45):

IIRC the proof state is part of the output panel, which you have to open at the bottom

view this post on Zulip Mathias Fleury (Nov 08 2022 at 17:45):

(it is one of the tabs under isabelle)

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 17:49):

Yes I know, how ever it does not show anything when I'm writing a proof.

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 17:50):

When writing a function, it will show e.g. the termination etc. Only the proof state is not shown

view this post on Zulip Mathias Fleury (Nov 08 2022 at 17:59):

image.png

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:00):

or do you mean something else?

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:01):

Nothing is shown in this panel:
image.png

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:02):

It does have some output when writing functions:
image.png

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:03):

did you start isabelle with isabelle vscode?

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:04):

yes

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:08):

odd, cannot reproduce image.png

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:09):

It happens in all of my theories.

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:11):

Somehow the state panel can show the proof state! But I still cannot understand why the output panel fails :(

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:12):

wait, I have launched a slightly different isabelle

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:14):

you need to set editor_output_state to true

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:14):

but I have no idea how to do that in vscode

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:15):

2022isabelle vscode -o "editor_output_state=true"

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:15):

seems to do it

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:16):

ok let me try it

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:18):

Yeah! It worked! Thank you :) But why it isn't the default case?

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:19):

I think it is the same idea as Isabelle/jEdit: in the state panel you have the current global goal (the show ?thesis) and in the output you have the current goal (the have)

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:19):

it is less important for apply-style proofs

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:21):

The isar proof state were also not shown in the panel

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:21):

image.png
Here is a screenshot where you can see the difference: output (bottom) is just some information and the state (top) is the interesting part

view this post on Zulip Zhiliang Chen (Nov 08 2022 at 18:23):

Ok, thank you for the support :)

view this post on Zulip Mathias Fleury (Nov 08 2022 at 18:24):

in vscode I miss the progress panel

view this post on Zulip Manuel Eberl (Nov 08 2022 at 19:26):

Makarius doesn't like outputting the proof state like this; he thinks it goes against how you're supposed to use Isabelle.

view this post on Zulip Manuel Eberl (Nov 08 2022 at 19:27):

I dare say most Isabelle users strongly disagree, myself included.

view this post on Zulip Wolfgang Jeltsch (Jan 05 2023 at 00:13):

I just started trying out Isabelle/VSCode. I’d like to give the Makarius way of doing things a try.

However, I have no clue how you guys got VSCode to show the “State” panel. I only have the part below the source code with panels “Problems”, “Output”, “Debug Console”, “Terminal”, and “Isabelle: Output”, but nothing to the right of the source code. Also, I cannot find any option to enable that part on the right side, where i could have a state panel.

Well, it looks to me that the above screenshot is actually from Emacs, not from VSCode. Is Isabelle/VSCode lacking things like the “State” panel completely? If yes, doesn’t that mean that without changing what goes into the “Output” panel, as described above, Isabelle/VSCode will never show you the proof state (which would make it close to useless)?

view this post on Zulip Wolfgang Jeltsch (Jan 05 2023 at 00:16):

Related to that, is there a way to set editor_output_state to true in the Isabelle/VSCode configuration, so that I don’t have to pass a corresponding option at the command line?

view this post on Zulip Mathias Fleury (Jan 05 2023 at 08:51):

Control P - isabelle state or something to open the panel

view this post on Zulip Mathias Fleury (Jan 05 2023 at 08:51):

my second screenshot is indeed an emacs screenshot

view this post on Zulip Mathias Fleury (Jan 05 2023 at 08:52):

Wolfgang Jeltsch said:

Related to that, is there a way to set editor_output_state to true in the Isabelle/VSCode configuration, so that I don’t have to pass a corresponding option at the command line?

IIRC set it in ~/.isabelle/Isabelle2022/etc/preferences

view this post on Zulip Wolfgang Jeltsch (Jan 05 2023 at 13:36):

Mathias Fleury said:

Control P - isabelle state or something to open the panel

Ctrl + P is about searching files by name, according to what it says in the pop-up, and consequently I get only file results.

view this post on Zulip Lukas Stevens (Jan 05 2023 at 13:38):

I think it should be Ctrl + Shift + P then type something like isabelle state

view this post on Zulip Lukas Stevens (Jan 05 2023 at 13:43):

I don't know if there is an option anologous to Show state in JEdit for the output panel in Isabelle/VSCode. According to Makarius the output and the state should be separate.

view this post on Zulip Wolfgang Jeltsch (Jan 05 2023 at 13:45):

Yes, Ctrl + Shift + P works. Thank you.

Any chance of having the state panel below the source code? I need my vertical space almost completely for the code.

Finally, what’s the advantage of having the state in a separate state panel, when I can just have it in the output panel, such that no space for an extra panel is needed? I mean, If it’s shown in the output panel, it’s also to a certain degree separate: the state is shown at the beginning of the output, the rest at the end. :man_shrugging:

view this post on Zulip Lukas Stevens (Jan 05 2023 at 13:52):

You can drag the state panel to the bottom, but then you still have separate output and state panel taking up space.

view this post on Zulip Wolfgang Jeltsch (Jan 05 2023 at 13:55):

At least, it wouldn’t take up vertical space then. However, I think I just stick to showing the state in the output.

view this post on Zulip Jonathan Lindegaard Starup (Feb 17 2023 at 13:28):

I'm on windows and started vscode with Cygwin-Terminal.bat. Both isabelle vscode -o "editor_output_state=true" and ctrl+shift+p > Isabelle: Show State doesn't work for me


Last updated: Feb 27 2024 at 08:17 UTC