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.
IIRC the proof state is part of the output panel, which you have to open at the bottom
(it is one of the tabs under isabelle
)
Yes I know, how ever it does not show anything when I'm writing a proof.
When writing a function, it will show e.g. the termination etc. Only the proof state is not shown
or do you mean something else?
Nothing is shown in this panel:
image.png
It does have some output when writing functions:
image.png
did you start isabelle with isabelle vscode
?
yes
odd, cannot reproduce image.png
It happens in all of my theories.
Somehow the state panel can show the proof state! But I still cannot understand why the output panel fails :(
wait, I have launched a slightly different isabelle
you need to set editor_output_state to true
but I have no idea how to do that in vscode
2022isabelle vscode -o "editor_output_state=true"
seems to do it
ok let me try it
Yeah! It worked! Thank you :) But why it isn't the default case?
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)
it is less important for apply-style proofs
The isar proof state were also not shown in the panel
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
Ok, thank you for the support :)
in vscode I miss the progress panel
Makarius doesn't like outputting the proof state like this; he thinks it goes against how you're supposed to use Isabelle.
I dare say most Isabelle users strongly disagree, myself included.
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)?
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?
Control P - isabelle state or something to open the panel
my second screenshot is indeed an emacs screenshot
Wolfgang Jeltsch said:
Related to that, is there a way to set
editor_output_state
totrue
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
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.
I think it should be Ctrl + Shift + P
then type something like isabelle state
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.
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:
You can drag the state panel to the bottom, but then you still have separate output and state panel taking up space.
At least, it wouldn’t take up vertical space then. However, I think I just stick to showing the state in the output.
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 07 2024 at 16:22 UTC