"Interpret to point" does not work on gitpod (while forward, backward and to end work)

[CohenCyril]

I was playing a bit with gitpot recently and I tried it on https://github.com/math-comp/math-comp. Interpreting forward, backward and to the end of a file works perfectly (~although I did not manage to make keyboard shortcuts work in theia~ I did, I had to deactivate some extension shortcuts (chrome://extensions/shortcuts)).

However, "Intepreting to point" does not seem to work. You can reproduce my experiments by going to https://gitpod.io/#https://github.com/math-comp/math-comp Then waiting for the initialization to finish and typing

cachedMake
etc/utils/setup_gitpod.sh
code mathcomp/field/galois.v

Scroll down to some proof... then either right-click + "interpret to point" or F1 + "Interpret to Point" (synchronous or not) does not work.

CC: @fakusb cf Zulip discussion

[gares]

Is it possible to run theia on the deasktop? Last time I tried, I could not find it "prebuilt"

[fakusb]

Note: One can apparently drag-and-drop the packaged ".vsix" extension into the editor to install it, allowing for printf-debugging.

[CohenCyril]

Note: One can apparently drag-and-drop the packaged ".vsix" extension into the editor to install it, allowing for printf-debugging.

Yes, that's how I "found" the correct hashes

[Zimmi48]

FTR, gitpod has just announced Coq (opam-based) and Nix templates:

• https://github.com/gitpod-io/template-coq
• https://www.gitpod.io/docs/quickstart/nix

I have played with the Nix template to get a good working environment for a project which makes use of the Coq Nix Toolbox and I have not encountered any issue with interpret to point or anything else like that. I think that what solved the issue is probably that gitpod switched the default editor from Theia to VsCode.