Karl Palmskog (Dec 14 2021 at 16:16): Karl Palmskog (Dec 14 2021 at 16:16):Maybe? I think it's technically possible now, at least. https://twitter.com/cattheory/status/1470762265288785921
my advisor just said in a meeting: "Why is Coq not on the Steam platform, one should ask." https://twitter.com/cattheory/status/1031007434418974720
- joomy (@cattheory) Théo Zimmermann (Dec 14 2021 at 16:56):Before putting it on Stream, I would look into putting it in the Windows marketplace and the macOS App Store.
Tim Carstens (Dec 14 2021 at 22:01):hehe Andrew was teasing me about my winter plans, I don't think he was being serious (!)
Andrew Appel (Dec 15 2021 at 17:55):I was really referring to a sentence from a famous POPL paper: "Building [Coq proofs] is surprisingly addictive, in a videogame kind of way" https://dl.acm.org/doi/abs/10.1145/1111037.1111042
Karl Palmskog (Dec 15 2021 at 17:59):sure, but Steam does support multiple OSs and has a bunch of tools already on its store, so it may be a more realistic way of distributing Coq than one might think
Tim Carstens (Dec 15 2021 at 19:24):"first install steam, then install opam with ocaml 4.x, then install coq" :grimacing:
Karl Palmskog (Dec 15 2021 at 19:30):Steam is binary install, so similar to the Snap. The key point is that tens (hundreds?) of millions of people have already installed Steam.
Tim Carstens (Dec 15 2021 at 19:31):heh don't let me stop you :innocent:
Karl Palmskog (Dec 15 2021 at 19:32):Théo's point on priorities is reasonable though (Mac / Windows store first)
Paolo Giarrusso (Dec 15 2021 at 20:00):Coq might also be easier than some games (Dwarf Fortress comes to mind, I hear)
Michael Soegtrop (Dec 16 2021 at 08:38):Well I am familiar with Steam - mostly because for relaxing I from time to time do some SteamVR based 3D coding. And I think it is not a bad idea, but I would then do a specialized Coq Platform pick including a collection of brain teasers and SF.
Tim Carstens (Dec 16 2021 at 09:06):I’d caution against taking on more things to maintain before thinking about the user story/needs … if this falls under “reduce barrier to entry” then I have to ask how it would support someone adopting Coq; if this falls under “attract new people” then perhaps it could work, but I think it’d need to be more than CoqIDE/vscode/whatever to be truly “gamified”
Tim Carstens (Dec 16 2021 at 09:07):If the goal is to bring SF to the masses, then I’d think a statefull in-browser experience might be more attractive than Steam; etc
Enrico Tassi (Dec 16 2021 at 09:10):if we have a "game pick", I propose: https://coq-next.vercel.app/fun/coqoban.html
Karl Palmskog (Jan 23 2022 at 16:39):saw that other open source software (GPL-2.0) is on Steam: https://github.com/NVIDIA/Q2RTX
Karl Palmskog (Jan 23 2022 at 16:53):would be cool to run Coq on the Steam Deck, but I guess that will actually work fine outside of Steam (it's a Linux-based OS): https://www.steamdeck.com/en/
Last updated: Jun 05 2023 at 10:01 UTC