Gergely Buday (Aug 04 2023 at 12:23): Gergely Buday (Aug 04 2023 at 12:23):I started
$ isabelle vscode MyTheory.thy
and it did load the theory file but without syntax highlighting. What shall I do?
I do this on Ubuntu 22.04.2 .
Kevin Kappelmann (Aug 04 2023 at 14:06):Is it working besides the syntax highlighting?
Gergely Buday (Aug 04 2023 at 15:03):Does not seem so. Is there a documentation for the Visual Studio Code extension, how can I open the Output panel and things? I have not found one.
Kevin Kappelmann (Aug 05 2023 at 07:53):press Ctrl+Shift+P to open vscode's command palette. Then type "isabelle" to find all available commands. output is shown when selecting "focus on output view"
Gergely Buday (Aug 08 2023 at 13:27):@Kevin Kappelmann it does not find any isabelle command.
Kevin Kappelmann (Aug 11 2023 at 13:18):I just tried it with the newest Isabelle development version and it works for me.
isabelle vscode -l HOL
Matthew Pocock (Aug 22 2023 at 20:18):It isn't working very well for me with the 2022 release. Do I need to use the RC3 build? If so, how do I download that?
Wolfgang Jeltsch (Aug 22 2023 at 20:42):Regarding your second question, have a look at https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/.
Matthew Pocock (Aug 22 2023 at 20:59):Wolfgang Jeltsch said:
Regarding your second question, have a look at https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/.
Thanks. I've grabbed that. The vscode session with the plugin starts up with isabelle vscode -l HOL . and the highlighting and the preview panel renders as expected, but I don't seem to be able to get the "show state" action to show anything.
Wolfgang Jeltsch (Aug 22 2023 at 21:18):Not sure whether this is related, but does passing -o editor_output_state to isabelle vscode help? Also, I don’t think you need to specifically activate HOL: it should be the default.
Matthew Pocock (Aug 22 2023 at 21:40):
I get this far. I've tried both with and without -o editor_output_state but can't see any obvious difference. Not sure where to look for any logging or debug info. I was expecting there to be something that interactively shows me the state of the proof as I step through the file.
Mathias Fleury (Aug 23 2023 at 04:43):Your files should be named XXX.thy not XXX.ML
Mathias Fleury (Aug 23 2023 at 04:43):and the theory name must match exactly the file name (Scratch vs scratch)
Wolfgang Jeltsch (Aug 23 2023 at 11:07):Apparently, a picture sometimes really says more than 1000 words. :grinning:
Matthew Pocock (Aug 23 2023 at 14:14):Mathias Fleury said:
Your files should be named
XXX.thynotXXX.ML
Thanks! That's got me going. I'm working through the Mipkow, Paulson & Wenze tutorial 2022 now.
Wolfgang Jeltsch (Aug 23 2023 at 14:19):Mipkow → Nipkow, Wenze → Wenzel. Always remember to spell the names of the important people correctly. :wink:
Wolfgang Jeltsch (Aug 23 2023 at 14:20):Which tutorial are you referring to, by the way?
Mathias Fleury (Aug 23 2023 at 17:21):If you are following the old intro (https://isabelle.in.tum.de/dist/Isabelle2022/doc/intro.pdf), please don't
Mathias Fleury (Aug 23 2023 at 17:22):The prog-prove (https://isabelle.in.tum.de/dist/Isabelle2022/doc/prog-prove.pdf) is much better
Mathias Fleury (Aug 23 2023 at 17:23):and if you are following the thing called (old-)tutorial (https://isabelle.in.tum.de/dist/Isabelle2022/doc/tutorial.pdf), don't. Use the prog-prove
Mathias Fleury (Aug 23 2023 at 17:25):in the old tutorial, "the rules of the games" is very interesting… but not for beginners. Only for intermediate people.
Wolfgang Jeltsch (Aug 23 2023 at 19:21):Yes, prog-prove is probably by far the best way to get into Isabelle.
Last updated: Apr 27 2024 at 16:16 UTC