Stream: General

Topic: Isabelle/VSCode in Isabelle2025-RC0

Simon Wimmer (Jan 22 2025 at 21:47):

After many years, I've tried to give Isabelle/VSCode another shot with Isabelle2025-RC0.
I mainly want to give a quick user report (mostly of things I found cubersome or missing).
But I was hoping that some of these things are known issues, for which people already have workarounds.

First, it's great to have the improved state panel, which brings Isabelle/VSCode much closer to productive usage for me. Completions are also a great improvement.

Second, I was wondering how people work without the theories panel?
I can see that I find errors in the Problems view, which is good, but not knowing how far my theories have been checked and whether there is a non-terminating proof somewhere bothers me quite a bit.

Issues

State Panel

• Hovering doesn’t display type information, only the location of the link destination; this is a really important feature in my Isabelle/jEdit usage
• Locate button does not work for me
• Sometimes it takes minutes to open?

Editor

• Popups display things like command strangely
• Popups do not have coloring
• Popups do not have mouse-over features
• Completions seem to be a lot more dependent on the current context than in Isabelle/jEdit:
  - Within a text block I can type \` to complete to ‹›, but not outside of it
  - Somehow if a part of a theory isn’t fully checked correctly yet, completions like @{thm} do not work properly: they will complete to something like @{thm}} because VSCode prematurely adds the second curly brace
• Clicking things in the editor is sometimes very erratic; some terms simply cannot be clicked, and trying to click them or even hovering over them seems to reload the current buffer; I couldn't make out the exact conditions under which this is happening yet

Moritz R (Feb 18 2025 at 11:51):

but not knowing how far my theories have been checked

do you have the red markings in the minimap? i think they show where errors are.
Another vscode extension i found extremely useful is "Error Lens" from "usernamehw". It inlines the error messages in red font.

Moritz R (Feb 18 2025 at 11:55):

I also use the extension "Hypersnips" which lets you define snippets that auto-insert e.g. ∨ on typing "\or" or a pair of ‹› when typing "cite".

Moritz R (Feb 18 2025 at 11:57):

I find the state panel opens more reliably if i put the cursor at a point where there is a nontrivial proof state

Moritz R (Feb 18 2025 at 12:06):

i have also put

 "editor.tokenColorCustomizations": {



    "textMateRules": [
      {
        "scope": [
          "source.isabelle"
        ],
        "settings": {
          "foreground": "#53a5a8f8"
        }
      },
      {
        "name": "String",
        "scope": "string",
        "settings": {
          "foreground": "#c2aa22"
        }
      },
      {
        "name": "Class name",
        "scope": "entity.name.type, entity.name.class, entity.name.namespace, entity.name.scope-resolution",
        "settings": {
          "fontStyle": "underline"
        }
      }
    ]
  },

into my settings.json (while using the color theme Default Light+)
(one can search in the settings menu for Editor: Token Color Customizations and click Edit in settings.json to find this file). This changes the color and style of some of the keywords. I honestly don't remember to what these correspond, but i believe these might be worth tinkering with. In particular this defines a different color for theorem names and yet unparsed contents of a thy file.

Moritz R (Feb 18 2025 at 12:07):

The underlining thingy is for isar keywords like "obtain"

Moritz R (Feb 18 2025 at 12:09):

Maybe other vscode users can share their settings/extensions etc. for making the vscode experience better aswell?

Last updated: Feb 28 2025 at 08:24 UTC