Open CohenCyril opened 3 years ago
Is it possible to run theia on the deasktop? Last time I tried, I could not find it "prebuilt"
Note: One can apparently drag-and-drop the packaged ".vsix" extension into the editor to install it, allowing for printf-debugging.
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
FTR, gitpod has just announced Coq (opam-based) and Nix templates:
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.
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
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