Stream: General

Topic: VS Code


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 13:25):

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

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Jul 31 2019 at 14:15):

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

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:18):

emacs + LSP

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Jul 31 2019 at 14:20):

Interesting, I didn't know that that works.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Jul 31 2019 at 14:26):

Odd. What kinds of crashes? And what OS?

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:28):

Both Linux (archlinux) and macOS

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:29):

jEdit becomes completely unresponsive.

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:29):

Sometimes typing one character takes 20s to be registered

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:32):

calling sledgehammer makes the problem more likely to happen

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Jul 31 2019 at 14:40):

How much memory do you have?

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Jul 31 2019 at 14:42):

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

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:45):

Same RAM.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Jul 31 2019 at 14:48):

That might explain it. :D

view this post on Zulip 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)

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:49):

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

view this post on Zulip Mathias Fleury (Jul 31 2019 at 14:49):

Sledgehammer creates a lot of terms...

view this post on Zulip 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.

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 15:06):

750GB RAM, 32 cores. Very smooth experience.

"Minimum requirements" :computer:

view this post on Zulip Manuel Eberl (Jul 31 2019 at 15:12):

Don't give Makarius any ideas.

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Jul 31 2019 at 15:14):

750GB RAM, 32 cores. Very smooth experience.

"Minimum requirements" :computer:

Works on my machine

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Jul 31 2019 at 17:11):

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

view this post on Zulip 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. ;)

view this post on Zulip 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.

view this post on Zulip Simon Wimmer (Aug 02 2019 at 09:20):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Aug 02 2019 at 13:57):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Lukas Stevens (Sep 19 2019 at 14:26):

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

view this post on Zulip Kevin Kappelmann (Sep 19 2019 at 14:27):

yep pasted image

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Sep 20 2019 at 06:23):

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

view this post on Zulip 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)

view this post on Zulip 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: Jun 20 2024 at 12:31 UTC