4ever2

This can be reproduced reliably with VsCoq v0.3.6 by: 1) Set VSCode theme to any dark theme 2) Uninstall VsCoq 3) Completely close all running VSCode windows 4) Reopen VSCode...

@HaoYang670 Take a look at #613 and #614

This might be related to https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/Coq.20in.20VS.20Code Setting the bin path to `/snap/coq-prover/current/coq-platform/2022-04-1/bin/` rather than `/snap/bin/` solves the issue on my machine.

> * Could you report the output from `snap connections coq-prover` Permission for `home` is included in the output and is also specified in the snap config https://github.com/coq/platform/blob/7c6c45e52a4bbf48174f6089e660c383f55bbbd7/linux/snap/snapcraft.yaml.in#L61 > *...

@Blaisorblade I don't have much experience with `strace` or `ltrace`. I can try looking at it tomorrow. `coqidetop` and `coqtop` both exit with error code 2 without writing anything to...

I can reproduce this on both macOS and Windows. Looks like this could be a VSCode problem.

> which version of vscode you are running? VSCode 1.74.0 with VsCoq 0.3.6 I have a workaround which seems to work https://github.com/4ever2/vscoq/commit/4a1df3683c2ebd8efb0f1728abbae7bc892a315d. I can open a PR later once I...

> I suppose then there is not much we can do about this. This is definitely possible, probably even easy to do. Unsaved files have the URI scheme `untitled` and...

@gares I played around with implementing that in VsCoq1 not so long ago, I can share the code later if it is useful to you. The OCaml-platform extension doesn't expose...

The difference in the output is because of the Printing Matching setting. However, switching the setting does not solve the performance issue. I also noticed that VsCoq sometimes is very...