Stream: Miscellaneous

Topic: Collacoq


view this post on Zulip Bas Spitters (Sep 06 2020 at 19:42):

Collacoq seems very nice, but I cannot seem to figure out how to share it with another user. Did anyone have success using it?
https://x80.org/collacoq/

view this post on Zulip Théo Zimmermann (Sep 06 2020 at 20:27):

What do you mean "share it with another user"? Since this is code running in the browser, it's not really done for collaborative editing.

view this post on Zulip Bas Spitters (Sep 06 2020 at 20:36):

Thanks. I misread colla as collaborative ...

So, repl.it could be useful. 8.6 is running now, and they seem to be happy to improve support:
https://repl.it/talk/ask/Adding-the-Coq-language/52498

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:15):

Colla does indeed refers to the French version of Paste , _à la_ pastebin => collacoq

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:16):

also there is a non-intended Coq-style pun in the French phonetics of colla for Spanish people :/

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:17):

Adding collaborative support wouldn't be hard if codemirror does already support it

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:17):

I don't have the cycles sadly, but any person with web dev skills should be able to add it

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:18):

It sounds like Bas wanted to use it as pastebin?

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:19):

But e.g. “save” does not give you a permalink to the code?

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:20):

nevermind, it does, once you actually add text

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:20):

e.g. I get https://x80.org/oxegemokej.coq

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:20):

which however 404s

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:21):

Oh indeed the url is broken

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:21):

for some reason the collacoq/ went away

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:22):

https://x80.org/collacoq/oxegemokej.coq

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:22):

I thought I had fixed this :S

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:22):

right, that works

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:22):

guess the web app must know the URL it runs at, many do for some reason.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:23):

yeah it was a silly thing

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:23):

I dunno why the problem re-appeared

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:23):

I'll do a fix later

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:26):

I’m sure you know, but as a reminder, maybe check if the fix survives a reboot and a redeploy

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:26):

Yup it should, it is a variable

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:26):

since those usually involve 42 layers of generators feeding generators creating final configurations :-)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:26):

maybe I didn't indeed commit the fix

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:26):

the setup of hastebin is pretty simple fortunately :)

view this post on Zulip Bas Spitters (Sep 07 2020 at 11:03):

@Emilio Jesús Gallego Arias Thanks. That indeed does what I was looking for.
For my course I'm moving to Github Classroom. That currently uses repl.it, although I'm not entirely sure what kind of integration it supports.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 11:17):

Let me know if you need help to integrate Coq with repl.it or with jupyter

view this post on Zulip Bas Spitters (Sep 07 2020 at 11:20):

They have the Debian version of Coqtop running already. jscoq is much nicer!
https://repl.it/talk/ask/Adding-the-Coq-language/52498

Is there anyway to get the imports for SF to work with Collacoq ? I understand it's not the initial use case, but it could be a nice collaborative tool in these corona times...

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 11:31):

@Bas Spitters I will push a SF build ASAP to collacoq

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 11:31):

we still have to automate jscoq deployment

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 11:31):

unfortunately we still do a lot of manual steps, but Shachar has been doing great progress towards an automatic seutp

view this post on Zulip Bas Spitters (Sep 09 2020 at 15:11):

@Emilio Jesús Gallego Arias They've giving up on Coq integration for now, as they are using an old ubuntu version.
Also, I'm not entirely sure whether repl.it has the right interaction model for Coq.

view this post on Zulip Bas Spitters (Sep 09 2020 at 15:16):

I guess github will integrate vscode (coqspaces https://github.com/features/codespaces) into classroom when it releases. I imagine integration with vscode should be easier.

view this post on Zulip Bas Spitters (Aug 03 2022 at 09:21):

I'm preparing for my Coq course this autumn and I'm updating some links. @Emilio Jesús Gallego Arias is CollaCoq still worth mentioning? I seems to be running Coq 8.11

view this post on Zulip Théo Zimmermann (Aug 03 2022 at 10:10):

@Bas Spitters You are probably using an outdated link. https://jscoq.github.io/ gives you a Coq 8.15 based-version.

view this post on Zulip Théo Zimmermann (Aug 03 2022 at 10:11):

And thanks BTW, because my own course materials also used an outdated link with Coq 8.11! :sweat_smile:

view this post on Zulip Bas Spitters (Aug 03 2022 at 10:19):

Does jscoq include all the collaborative features of collacoq now?

view this post on Zulip Théo Zimmermann (Aug 03 2022 at 10:34):

Oh, that's a good point. I don't see any save/share buttons. Maybe @Shachar Itzhaky can answer.

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 13:34):

Hi! Yes, the hastebin functionality has been integrated into the jsCoq scratchpad on the website. You can find instructions here.

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 16:29):

@Emilio Jesús Gallego Arias I wonder if we should retire the old collacoq page at https://x80.org/collacoq/ or have it redirect to coq.now.sh/scratchpad.html?share.

view this post on Zulip Théo Zimmermann (Aug 03 2022 at 16:50):

Great, although the feature is unfortunately not very discoverable. It could make sense to document the Ctrl+Shift+S keyboard on the jsCoq homepage, wouldn't it?

view this post on Zulip Théo Zimmermann (Aug 03 2022 at 16:51):

Or even to provide a link to the ?share version from the homepage.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 03 2022 at 17:19):

@Shachar Itzhaky yes, please open a ticket and I'll add a redirect (eventually)

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 17:23):

Théo Zimmermann said:

Great, although the feature is unfortunately not very discoverable. It could make sense to document the Ctrl+Shift+S keyboard on the jsCoq homepage, wouldn't it?

Yes, the keyboard combinations used to be on the homepage. I decided that it's not the place for them so I moved them to the manual. However, what I do intend to do (just never got around to it) is display a quick help screen when opening the scratchpad, and add a "quick help" option to the ellipsis menu so that users can go back to that screen later. That would make it discoverable. We did want to minimize the clutter in the UI, and I agree that it makes the app a bit spartan. There are definitely some tradeoffs to consider going forward.

view this post on Zulip Théo Zimmermann (Aug 03 2022 at 17:29):

Remember that perfect is the enemy of good. Maybe in the meantime you could just add a link to the ?share version from the homepage?

view this post on Zulip Bas Spitters (Aug 04 2022 at 10:38):

Apparently, collacoq is still better than vscoq with live share, as vscoq will not allow both parties to run coq, IIUC.
https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/.E2.9C.94.20VSCoq.20LiveShare.20ProofView/near/270677497

view this post on Zulip Théo Zimmermann (Aug 04 2022 at 19:32):

But collacoq does not allow sharing a buffer and having two people edit it, does it?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 05 2022 at 00:15):

@Théo Zimmermann Shachar just merged that precise functionality :octopus:

view this post on Zulip Bas Spitters (Aug 05 2022 at 09:24):

Is it possible to connect hastebin to something more permanent (Google Drive?)


Last updated: Aug 14 2022 at 12:03 UTC