Cyril Cohen (Mar 15 2021 at 14:04): Cyril Cohen (Mar 15 2021 at 14:04):(Fantastic news about the release 0.3.4 btw!!!)
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.
Cyril Cohen (Mar 15 2021 at 14:06):This works very well on my machine... Does someone see a reason why this would behave differently in theia and so specifically about this particular instruction??
Fabian Kunze (Mar 15 2021 at 14:11):F1 -> step forward works.
Fabian Kunze (Mar 15 2021 at 14:12):The "interprete to point" command does not even get passed down to coq, I'm not sure whats the problem. One would need to investigate this further
Fabian Kunze (Mar 15 2021 at 14:13):It could for example be the case that our/the vscode-model of "where is my cursor" is confused by the possibility for multiple cursors.
Cyril Cohen (Mar 15 2021 at 14:18):Thanks for this quick diagnostic. It's not really blocking for me, but I think it would be nice to investigate eventually, because this gitpod thing is a very promissing way to work with coq without installing it... and this "interpred to point" thing, is the only problem I encountered so far...
Fabian Kunze (Mar 15 2021 at 14:25):Feel free to open a github issue so it's documented somewhere
Cyril Cohen (Mar 15 2021 at 14:38): Enrico Tassi (Mar 15 2021 at 14:49):Here alt+up works, but alt+right is captured by the browser. I tried to change the binding, but still does not work. Maybe it's not the root cause, but it one.
Enrico Tassi (Mar 15 2021 at 14:51):anyway, pulling nix from a docker image... scary but cool
Théo Zimmermann (Mar 15 2021 at 14:56):Very cool indeed. I also have the keyboard shortcuts working (in Firefox) but go to point not working (but this is definitely beyond the keyboard shortcut issue).
Théo Zimmermann (Mar 15 2021 at 14:57):I had also attempted some stuff with gitpod before, but without this success.
Enrico Tassi (Mar 15 2021 at 14:58):My question is: how much does it cost?
Théo Zimmermann (Mar 15 2021 at 15:00):https://www.gitpod.io/pricing/
Bas Spitters (Jul 30 2021 at 09:20):I've started preparing my Coq course again, and I am planning to use github classroom with software foundations, as last year.
Has there been any progress on gitpod that I should consider? The issue above still seems open ...
Fabian Kunze (Aug 07 2021 at 13:17):I don't think there was progress on the vscoq-side, but I have not tried it again. Also, theia itself claims not to be ready for productive use.
I have not found the time to dive into that problem myself (setting up gitpod/theia etc., especially being able to debug then (at least printf-style-debugging)), but I'm very open to help someone who has that system set up in a collaborative zoom-debug-session.
Last updated: Apr 18 2024 at 22:02 UTC