Bas Spitters (Sep 06 2020 at 19:42): 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/
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.
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
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:15):Colla does indeed refers to the French version of Paste , _à la_ pastebin => collacoq
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 :/
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:17):Adding collaborative support wouldn't be hard if codemirror does already support it
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
Paolo Giarrusso (Sep 07 2020 at 10:18):It sounds like Bas wanted to use it as pastebin?
Paolo Giarrusso (Sep 07 2020 at 10:19):But e.g. “save” does not give you a permalink to the code?
Paolo Giarrusso (Sep 07 2020 at 10:20):nevermind, it does, once you actually add text
Paolo Giarrusso (Sep 07 2020 at 10:20):e.g. I get https://x80.org/oxegemokej.coq
Paolo Giarrusso (Sep 07 2020 at 10:20):which however 404s
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:21):Oh indeed the url is broken
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:21):for some reason the collacoq/ went away
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:22):https://x80.org/collacoq/oxegemokej.coq
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:22):I thought I had fixed this :S
Paolo Giarrusso (Sep 07 2020 at 10:22):right, that works
Paolo Giarrusso (Sep 07 2020 at 10:22):guess the web app must know the URL it runs at, many do for some reason.
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:23):yeah it was a silly thing
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:23):I dunno why the problem re-appeared
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:23):I'll do a fix later
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
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:26):Yup it should, it is a variable
Paolo Giarrusso (Sep 07 2020 at 10:26):since those usually involve 42 layers of generators feeding generators creating final configurations :-)
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:26):maybe I didn't indeed commit the fix
Emilio Jesús Gallego Arias (Sep 07 2020 at 10:26):the setup of hastebin is pretty simple fortunately :)
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.
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
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...
Emilio Jesús Gallego Arias (Sep 07 2020 at 11:31):@Bas Spitters I will push a SF build ASAP to collacoq
Emilio Jesús Gallego Arias (Sep 07 2020 at 11:31):we still have to automate jscoq deployment
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
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.
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.
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
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.
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:
Bas Spitters (Aug 03 2022 at 10:19):Does jscoq include all the collaborative features of collacoq now?
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.
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.
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.
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?
Théo Zimmermann (Aug 03 2022 at 16:51):Or even to provide a link to the ?share version from the homepage.
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)
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.
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?
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
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?
Emilio Jesús Gallego Arias (Aug 05 2022 at 00:15):@Théo Zimmermann Shachar just merged that precise functionality :octopus:
Bas Spitters (Aug 05 2022 at 09:24):Is it possible to connect hastebin to something more permanent (Google Drive?)
Last updated: Dec 07 2023 at 17:01 UTC