The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

That's very interesting Kevin! Does this works the same on all systems then (including Windows)?

When the Coq Platform becomes available as a Docker image, this could become the recommended installation / usage method if that's easy to use. That would simplify our work a lot to know this to work everywhere.

Théo

Le jeu. 15 oct. 2020 à 00:41, Kevin Sullivan <sullivan.kevinj AT gmail.com> a écrit :

In our work at UVa we're using VS Code, plugins including live share, and also docker. We've dockerized our shared development environment to include both proof checker but also other software integrated with our formal modeling and analysis. For us this software includes a custom build of Clang, ROS, C#, Lean, etc. Updates to our docker file trigger a build and upload of a new shared image. Collaborators just download that image update, start VSCode, and connect it to the new environment. Really works quite well for our group.

On Wed, Oct 14, 2020, 5:41 PM Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Bas,

I get: "You’re already on the waitlist for Codespaces! We’ll notify you
when we’ve enabled it on your account."

Do I need just more luck/patience?

Maxime.

On 10/14/20 9:07 PM, Bas Spitters wrote:
> The following works quite well:
> https://github.com/features/codespaces
> Getting Coq to run is actually easy. Open a terminal in github
> codespaces. Do the regular install, set the path and select "interpret
> to point".
>
> On Wed, Oct 14, 2020 at 6:23 PM Abhishek Anand
> <abhishek.anand.iitg AT gmail.com> wrote:
>>
>> When using vscode liveshare with coq (vscoq I guess), do all participants see the host's proof window? or each participant independently has coqtop running locally to produce the proof window in a non-synced manner?
>>
>> Thanks,
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/
>>
>>
>> On Wed, Jun 17, 2020 at 2:04 PM Bas Spitters <b.a.w.spitters AT gmail.com> wrote:
>>>
>>> My students are using vscode for this, and I understand it works well.
>>> I believe it only has a cloud based solution.
>>> https://visualstudio.microsoft.com/services/live-share/
>>>
>>> On Sat, Jun 13, 2020 at 9:50 PM Abhishek Anand
>>> <abhishek.anand.iitg AT gmail.com> wrote:
>>>>
>>>> At our company, people in different cities/countries often need to collaboratively edit Coq files.
>>>> We have been using tmux+ssh+emacs-console-mode+PG+company-coq solution for a few years and it works ok.
>>>> I have described our setup in the following wiki page:
>>>> https://github.com/coq/coq/wiki/Remote-Collaborative-Editing-of-Coq-Files
>>>>
>>>> Are there other ways people remotely collaboratively edit Coq files?
>>>> It would be great to add to that page and/or describe/discuss the setup in this email thread.
>>>>
>>>> Thanks,
>>>> -- Abhishek
>>>> http://www.cs.cornell.edu/~aa755/