Stream: General

Topic: VS Code

Kevin Kappelmann (Jul 31 2019 at 11:30):

In a nutshell, does someone know the current state of using Isabelle with VS Code? Is the setup easy? Is it usable in practice? Would I need to use this or this plugin for the latest Isabelle release? etc.

Simon Wimmer (Jul 31 2019 at 12:46):

So... regarding the plugins, the first should be for the dev version, and the second is for Isabelle2019

Simon Wimmer (Jul 31 2019 at 12:50):

I've used it for a few months about a year ago. In vanilla state is not very practical to use.
But if you do a few customizations (specifically if you setup your own abbreviations), one can be productive with it.
See https://github.com/m-fleury/isabelle-snippets
However, it's clearly not as comfortable as Isabelle/jEdit at this point.

Simon Wimmer (Jul 31 2019 at 12:53):

Some specific problems that come to mind:
- It relies on https://marketplace.visualstudio.com/items?itemName=siegebell.prettify-symbols-mode, which has annoying bugs
- State output does not have highlighting
- Panels for e.g. search and sledgehammer do not exist
- No clickable code templates
- Cursor positions are not tracked as precisely as in jEdit, which can be annoying and sometimes run you in performance problems

Simon Wimmer (Jul 31 2019 at 12:54):

Note that all this info is from my experience from a year ago. The best person to answer this would be Mathias Fleury because to my knowledge he's the only real power user of it.

Kevin Kappelmann (Jul 31 2019 at 13:25):

Alright, that's a good starting point - thanks! :)

Mathias Fleury (Jul 31 2019 at 14:15):

I have actually stopped using VSCode (in favour of emacs), because of prettify-symbols-mode that is unmaintained and a huge hack (at least, this was the case last time I checked). I had developed a version of prettify-symbols-mode that fixed some of the performance problems, however.

Manuel Eberl (Jul 31 2019 at 14:15):

So what are you using for Isabelle now then? Presumably not emacs?

Mathias Fleury (Jul 31 2019 at 14:18):

emacs + LSP

Mathias Fleury (Jul 31 2019 at 14:19):

It has the same limitations as the VSCode stuff (in particular, no colours in the output panel). But it does not crash twice a day

Manuel Eberl (Jul 31 2019 at 14:20):

Interesting, I didn't know that that works.

Manuel Eberl (Jul 31 2019 at 14:20):

The last time I used the VSCode integration I found it absolutely unusable, but that was quite some time ago (and before your integration efforts, I think)

Manuel Eberl (Jul 31 2019 at 14:21):

I still wistfully remember ProofGeneral. I was probably one of the last people who still used it even when it became more and more broken.

Mathias Fleury (Jul 31 2019 at 14:25):

I have strange issues with jEdit to the point that it crashes even when I prepared exercises for my version of the concrete semantics course

Manuel Eberl (Jul 31 2019 at 14:26):

Odd. What kinds of crashes? And what OS?

Mathias Fleury (Jul 31 2019 at 14:28):

Both Linux (archlinux) and macOS

Mathias Fleury (Jul 31 2019 at 14:29):

jEdit becomes completely unresponsive.

Mathias Fleury (Jul 31 2019 at 14:29):

Sometimes typing one character takes 20s to be registered

Hanna Lachnitt (Jul 31 2019 at 14:30):

It happens to me all the time too. Both the being total unresponsive and the getting really slow thing. I use Linux.

Mathias Fleury (Jul 31 2019 at 14:31):

I believe it is a problem in the GC of polyml, because only one thread is running.

Mathias Fleury (Jul 31 2019 at 14:32):

calling sledgehammer makes the problem more likely to happen

Mathias Fleury (Jul 31 2019 at 14:33):

Now to be clear, there is no reason that this would be better with Isabelle/VSCode or emacs. I find it better, but I might just call sledgehammer less often

Manuel Eberl (Jul 31 2019 at 14:40):

How much memory do you have?

Manuel Eberl (Jul 31 2019 at 14:41):

I very occasionally experience jEdit to be a bit unresponsive, but that usually happens when I leave it running for an extremely long time or load a very large number of theories without using a session image.

Manuel Eberl (Jul 31 2019 at 14:42):

And I have 16 GB on my laptop and 32 GB on my desktop.

Mathias Fleury (Jul 31 2019 at 14:45):

Same RAM.

Mathias Fleury (Jul 31 2019 at 14:48):

My theories are huge (Peter Lammich style of theories), and I have one session that takes 30 minutes to build and cannot be split in something smaller that would be meaningful.

Manuel Eberl (Jul 31 2019 at 14:48):

That might explain it. :D

Manuel Eberl (Jul 31 2019 at 14:48):

I also use sledgehammer very rarely (although I cannot see why sledgehammer would cause such huge memory leaks)

Mathias Fleury (Jul 31 2019 at 14:49):

But my problem for the concrete semantics happened while importing only theories from HOL-IMP

Mathias Fleury (Jul 31 2019 at 14:49):

Sledgehammer creates a lot of terms...

Mathias Fleury (Jul 31 2019 at 14:51):

I switched to a server recently (750GB RAM, 32 cores). Very smooth experience. No need to restart ever morning and wait for 10 minutes. Very nice experience.

Kevin Kappelmann (Jul 31 2019 at 15:06):

750GB RAM, 32 cores. Very smooth experience.

"Minimum requirements" :computer:

Manuel Eberl (Jul 31 2019 at 15:12):

Don't give Makarius any ideas.

Manuel Eberl (Jul 31 2019 at 15:13):

I'm currently waiting for AMD to get their act together and finally deliver those juicy 16 cores in the 3900X so I can upgrade my machine at home.

Lukas Stevens (Jul 31 2019 at 15:14):

750GB RAM, 32 cores. Very smooth experience.

"Minimum requirements" :computer:

Works on my machine

Mathias Fleury (Jul 31 2019 at 15:33):

JEdit does not provide a smooth experience with the same machine, but this is due to X-forwarding.

Mohammad Abdulaziz (Jul 31 2019 at 16:23):

And I have 16 GB on my laptop and 32 GB on my desktop.

16 GB is certainly not enough. After a few days on my machine, it somehow occupies more than 21GB of memory.

Mohammad

Mathias Fleury (Jul 31 2019 at 17:11):

Polyml uses as much memory as possible (I have seen it using >60GB on the server)

Manuel Eberl (Aug 01 2019 at 07:26):

Yeah, how much memory it "occupies" doesn't really tell you all that much. The air in an air-tight container also occupies the entire container, no matter how big the container is. ;)

Simon Wimmer (Aug 02 2019 at 09:19):

It's still surprising to me that so many people seem to have such significant problems with jEdit.
I've been a Mac user for the last 4 years and while in the beginning, I encountered these problems very frequently, things have improved for me over the last few versions. My machines were also never extremely powerful (2 cores and 8 gigs, now 4 cores and 16 gigs).

What got better, in particular, was the perceived amount of memory leaking on the jEdit side. So I think Mathias' analysis is right that nowadays problems are mainly on the Poly side. I still recommend giving both ML, and Java sufficient amounts of initial memory. The defaults are still rather low (I think). Also, it helps to put as many things in the session image as possible.

Simon Wimmer (Aug 02 2019 at 09:20):

Sad to here you also had to give up on VS Code Mathias.

Lukas Stevens (Aug 02 2019 at 13:19):

I think for many people (myself included) the problem with jEdit is not necessarily its stability, but rather that it is a poor text editor.

Mathias Fleury (Aug 02 2019 at 13:37):

Let me expand a bit on the problem of VSCode. There are two main problems:
1. Understanding the actual PIDE code.
2. Printing symbols.

Mathias Fleury (Aug 02 2019 at 13:39):

Issue 1 is nearly impossible to solve. I now basically understand the LSP interface, but it relies on so many levels of PIDE and Isabelle internals, that it is impossible to understand what is happening how and where.

Mathias Fleury (Aug 02 2019 at 13:46):

Issue 2 is the most critical one. There are two solutions for it:
A. The jEdit way: the file is stored twice: once as it is one the hard drive and once with the nice utf8 characters. Only the latter is shown. This explains why pasted symbols (e.g., \forall) are not replaced: the paste happens in the wrong buffer. This mechanism is extremely intrusive and requires patches over the original editor.
B. The Other way: replace the symbols while printing them. This is for example done for ligatures, except that the length is kept (“==“ will be replaced by a longer equal of length 2 characters). This mechanism is not sufficient for Isabelle (the forall symbol and \forall have a very different length). However, some editors provide a way to this without patching them.

Mathias Fleury (Aug 02 2019 at 13:49):

In VSCode, prettify-symbols-Mode does the following: it hides the symbol (e.g., \forall) and prints instead the symbol. This requires to capture ever call to left and right arrow to make sure, the user does not end in the middle of an invisible symbol. Hiding symbols is a hack and capturing the arrow symbols is too slow sometimes.

Kevin Kappelmann (Aug 02 2019 at 13:53):

Naive question: How horrible would it be to change Isabelle such that UTF8 symbols like ∀, ヨ. etc. are natively supported in the source files?

Mathias Fleury (Aug 02 2019 at 13:53):

Implementing A in VSCode is not easy (this whole thread https://github.com/Microsoft/vscode/issues/2402#issuecomment-230427921 talks about solving the problem) and requires more time than I want to spend on it.

Mathias Fleury (Aug 02 2019 at 13:55):

@Simon Wimmer AFAIK, the only problem about more theory is that the PIDE part is supposedly asynchronous and therefore should never slow down jEdit.

Mathias Fleury (Aug 02 2019 at 13:56):

@Kevin Kappelmann actually it already works, except that “Isabelle build” does not support it. It took me forever to debug that issue.

Mathias Fleury (Aug 02 2019 at 13:57):

(Just imagine: jEdit works and prints the right thing, but Isabelle build mysteriously fails...)

Kevin Kappelmann (Aug 02 2019 at 13:58):

Oh, so wouldn't the obvious thing then be to make Isabelle build work with UTF-8 symbols?

Mathias Fleury (Aug 02 2019 at 14:00):

I have never tried, but I guess that it would work with the “pide” Option of Isabelle build (I don’t remember how it is called)

Mathias Fleury (Aug 02 2019 at 14:02):

I don’t want to have a strange version of Isabelle (as a reviewer, would you trust that?) and Makarius does not believe in utf8 for files

Kevin Kappelmann (Aug 02 2019 at 14:05):

I don’t want to have a strange version of Isabelle (as a reviewer, would you trust that?) and Makarius does not believe in utf8 for files

Uff, I mean, just have a look at, for example, this and compare the isabelle and lean version. so much nicer with utf8; no weird text transformations need to be done by your editor.

Mathias Fleury (Aug 02 2019 at 14:06):

I agree. No need to convince me ;) But I don’t want to fight for including that in Isabelle.

Kevin Kappelmann (Aug 02 2019 at 14:07):

haha, just dropping it here; maybe some people read it and eventually, it's gonna happen :eyes:

Mathias Fleury (Aug 02 2019 at 14:16):

But actually I could try to make a git hook that replaces all the utf8 when committing and replaces them back when pulling.

Mathias Fleury (Aug 02 2019 at 14:17):

But basically, I think it is faster to wait for Makarius to retire from Isabelle that convincing him of anything. Except that then the PIDE stuff is dead

Manuel Eberl (Aug 05 2019 at 15:29):

I have no idea how LSP works, but would it not be possible to just have a hook that replaces all Isabelle symbols with UTF-8 on loading the file and the other way round upon saving?

Mathias Fleury (Aug 06 2019 at 08:13):

(Sorry for the late answer. I am on vacation)
That should be handled mostly by the editor, not so much by the LSP protocol. But that could work.

I see a few drawbacks: a crash of the editor leaves the file in UTF–8 (not so nice); it becomes impossible to use git within the editor; and it will to very fun to debug (saving in LSP can be interesting and weird).

But I am not sure that I will ever implement it. If there are volunteers out there that understand JavaScript/Typescript and VSCode...

Lukas Stevens (Aug 06 2019 at 12:32):

This also has the drawback that one needs to implement this for each editor. Ideally, we shouldn't force anyone to use a specific text editor.

Mathias Fleury (Aug 06 2019 at 13:48):

The LSP needs several extensions to work with Isabelle anyway. Work per editor is required anyway (e.g., syntax highlighting is very different from programming)

Josh Chen (Aug 11 2019 at 15:37):

Adding my vote: I'm waiting for the day UTF8 finally comes to Isabelle too. Having been just recently introduced to Agda, I think these anachronistic features of Isabelle could contribute to it eventually getting left in the dust.

Kevin Kappelmann (Sep 19 2019 at 14:22):

I tried to install the VSCode extension (I am using Ubuntu), but opening the state panel returns an exception in the output console:

*** Consumer thread failure: "Session.dispatcher"
*** Consumer failed: "isabelle.vscode.State_Panel"
*** java.util.NoSuchElementException: key not found: IsabelleDejaVuSans.ttf

I installed the Isabelle Deja Vu Sans font on my system (I can select it in other programs). Any idea how to fix this? Do I need to add some additional settings in VSCode?

Lukas Stevens (Sep 19 2019 at 14:26):

Does the font show up when executing fc-list | grep IsabelleDejaVuSans.ttf?

Kevin Kappelmann (Sep 19 2019 at 14:27):

yep pasted image

Kevin Kappelmann (Sep 19 2019 at 14:28):

There is a bullet point in "Known limitations" of the isabelle VSCode plugin:

Lack of specific support for the Isabelle fonts: these need to be manually installed on the system and configured for VSCode (see also $ISABELLE_FONTS within the Isabelle environment).

Note: As the Isabelle fonts continue to evolve, installed versions need to be updated according to each new Isabelle version.

But it does not mention how to configure it for VSCode :sweat_smile:

Kevin Kappelmann (Sep 19 2019 at 14:35):

If I add "editor.fontFamily": "'Isabelle DejaVu Sans'" to my settings, VSCode is even picking up the font, but the state panel still errors

Mathias Fleury (Sep 20 2019 at 06:23):

that looks like the font problem Lars talked about on the mailing-list

Mathias Fleury (Sep 20 2019 at 06:26):

Ah no sorry (https://github.com/AdoptOpenJDK/openjdk-build/issues/693 was the error on the java side)

Kevin Kappelmann (Sep 22 2019 at 19:44):

FYI Makarius patched that issue - but it seems that there are some more issues showing up now. See this e-mail here

Last updated: Dec 21 2024 at 12:33 UTC