Nikola Katić (Nov 24 2022 at 19:38): Nikola Katić (Nov 24 2022 at 19:38):Not sure if this is the right place for the question, so if there is a stream for IDE-related questions, please do tell me :smile:
Is there any tutorial/example of how isabelle-emacs should be used?
I think I installed it correctly (including dependencies), did "M-x lsp-install-server" at the beginning of the file, but don't know how to use its features.
Mathias Fleury (Nov 24 2022 at 20:57):Mmm seems pictures in the Readme are broken. But lsp-install-server does not install isabelle (at least I never implemented that).
Mathias Fleury (Nov 24 2022 at 21:00):Normally, when you start (and that isabelle has started), you should see the buffer being split into 3 (theory panel, state panel, and output panel)
Mathias Fleury (Nov 24 2022 at 21:03):I will add a new screenshot tomorrow (the old ones: here and there )
Mathias Fleury (Nov 24 2022 at 21:03):(but I am probably not the most qualified person to give a tutorial, because I am the main developer of isabelle-emacs)
Nikola Katić (Nov 24 2022 at 22:15):Thanks for the response! I did read instructions from the main page, so I took care of steps 1 and 2 - not sure what is missing.
Mathias Fleury (Nov 25 2022 at 05:09):What happens when you run M-x lsp?
Nikola Katić (Nov 30 2022 at 18:34):Sorry for the delay. This is the feedback I'm getting:
lsp-isabelle.png
There is a file 211.thy in /home/nikola/thys/ directory.
In ~/.isabelle/Isabelle2022-vsce/etc/settings I've modified AFP line to this:
AFP=/home/nikola/thys/
Am I doing something wrong here?
Mathias Fleury (Nov 30 2022 at 18:37):Do you really have the afp directly in /home/nikola/?
Mathias Fleury (Nov 30 2022 at 18:38):and not /home/nikola/afp-2022/ or something like that?
Nikola Katić (Nov 30 2022 at 18:49):This is complete content of the file afp.png and thys dir fs.png
Mathias Fleury (Nov 30 2022 at 18:55):Okay so you do need the AFP
Mathias Fleury (Nov 30 2022 at 18:57):you should set the emacs variable lsp-isabelle-options to (list )
Nikola Katić (Nov 30 2022 at 19:39):Thank you! We've made it work :smile:
The only issue I'm facing now is regarding *lsp-isar-output* which is empty all the time - not sure what's its purpose tbh. I'm attaching screenshot to show what it looks like after sladgehammering.
I will try to use this mode on a regular basis and see if it can be permanent replacement for JEdit.
Mathias Fleury (Nov 30 2022 at 19:51):That is not expected
Mathias Fleury (Nov 30 2022 at 21:26):Can you check in the lsp-log buffer what is executed. It should be of the form:
Command "path-to-isabelle-release/bin/isabelle vscode_server -o vscode_pide_extensions -o vscode_caret_perspective=10 -m do_notation" is present on the path.
but that should not be the source of the problem
Mathias Fleury (Nov 30 2022 at 21:31):There is one more thing that is weird in your screenshot: no syntax highlighting
Mathias Fleury (Nov 30 2022 at 21:32):I guess that the thy folder from /home/nikola/thy a soft link?
Mathias Fleury (Nov 30 2022 at 21:38):but that issue does not explain why sledgehammer output is not in the output buffer :thinking:
Nikola Katić (Dec 01 2022 at 08:16):Mathias Fleury said:
Can you check in the lsp-log buffer what is executed. It should be of the form:
Command "path-to-isabelle-release/bin/isabelle vscode_server -o vscode_pide_extensions -o vscode_caret_perspective=10 -m do_notation" is present on the path.
I do have that line -- only difference is that path-to-isabelle-release is my actual path on the system.
Nikola Katić (Dec 01 2022 at 08:17):Mathias Fleury said:
I guess that the
thyfolder from/home/nikola/thya soft link?
Well, /home/nikola/thys/ is a real directory I've made, not a soft link
Nikola Katić (Dec 01 2022 at 08:19):Could it be the problem that I cloned git repository (isabelle-emacs) in a directory that is a soft link?
Last updated: Apr 25 2024 at 20:15 UTC