(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 (
However, "Intepreting to point" does not seem to work.
You can reproduce my experiments by going to
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.
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??
F1 -> step forward works.
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
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.
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...
Feel free to open a github issue so it's documented somewhere
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.
anyway, pulling nix from a docker image... scary but cool
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).
I had also attempted some stuff with gitpod before, but without this success.
My question is: how much does it cost?
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 ...
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: Jun 04 2023 at 23:30 UTC