Stream: VsCoq devs & users

Topic: VsCoq in gitpod, issue coq-community/vscoq#219


view this post on Zulip 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.

view this post on Zulip 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??

view this post on Zulip Fabian Kunze (Mar 15 2021 at 14:11):

F1 -> step forward works.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Fabian Kunze (Mar 15 2021 at 14:25):

Feel free to open a github issue so it's documented somewhere

view this post on Zulip Cyril Cohen (Mar 15 2021 at 14:38):

coq-community/vscoq#219

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Mar 15 2021 at 14:51):

anyway, pulling nix from a docker image... scary but cool

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Mar 15 2021 at 14:57):

I had also attempted some stuff with gitpod before, but without this success.

view this post on Zulip Enrico Tassi (Mar 15 2021 at 14:58):

My question is: how much does it cost?

view this post on Zulip Théo Zimmermann (Mar 15 2021 at 15:00):

https://www.gitpod.io/pricing/

view this post on Zulip 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 ...

view this post on Zulip 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: Jan 30 2023 at 18:04 UTC