Stream: Beginner Questions

Topic: No proof state in vscode

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.

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

Mathias Fleury (Nov 08 2022 at 17:45):

(it is one of the tabs under isabelle)

Zhiliang Chen (Nov 08 2022 at 17:49):

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

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

Mathias Fleury (Nov 08 2022 at 17:59):

image.png

Mathias Fleury (Nov 08 2022 at 18:00):

or do you mean something else?

Zhiliang Chen (Nov 08 2022 at 18:01):

Nothing is shown in this panel:
image.png

Zhiliang Chen (Nov 08 2022 at 18:02):

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

Mathias Fleury (Nov 08 2022 at 18:03):

did you start isabelle with isabelle vscode?

Zhiliang Chen (Nov 08 2022 at 18:04):

yes

Mathias Fleury (Nov 08 2022 at 18:08):

odd, cannot reproduce image.png

Zhiliang Chen (Nov 08 2022 at 18:09):

It happens in all of my theories.

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 :(

Mathias Fleury (Nov 08 2022 at 18:12):

wait, I have launched a slightly different isabelle

Mathias Fleury (Nov 08 2022 at 18:14):

you need to set editor_output_state to true

Mathias Fleury (Nov 08 2022 at 18:14):

but I have no idea how to do that in vscode

Mathias Fleury (Nov 08 2022 at 18:15):

2022isabelle vscode -o "editor_output_state=true"

Mathias Fleury (Nov 08 2022 at 18:15):

seems to do it

Zhiliang Chen (Nov 08 2022 at 18:16):

ok let me try it

Zhiliang Chen (Nov 08 2022 at 18:18):

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

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)

Mathias Fleury (Nov 08 2022 at 18:19):

it is less important for apply-style proofs

Zhiliang Chen (Nov 08 2022 at 18:21):

The isar proof state were also not shown in the panel

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

Zhiliang Chen (Nov 08 2022 at 18:23):

Ok, thank you for the support :)

Mathias Fleury (Nov 08 2022 at 18:24):

in vscode I miss the progress panel

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.

Manuel Eberl (Nov 08 2022 at 19:27):

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

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)?

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?

Mathias Fleury (Jan 05 2023 at 08:51):

Control P - isabelle state or something to open the panel

Mathias Fleury (Jan 05 2023 at 08:51):

my second screenshot is indeed an emacs screenshot

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

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.

Lukas Stevens (Jan 05 2023 at 13:38):

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

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.

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:

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.

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.

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: Dec 21 2024 at 16:20 UTC