Karl Palmskog (Sep 09 2021 at 05:54): Karl Palmskog (Sep 09 2021 at 05:54):To compete with Lean's various web games, would be cool to have a jsCoq version of Coqoban with some bells and whistles on top: https://github.com/coq-community/coqoban
Will at least put this on my list of "projects to try first when figuring out jsCoq toolchain"
Shachar Itzhaky (Sep 09 2021 at 07:00):Haha, sounds like loads of fun! I think this would be a wonderful opportunity to test the experimental "project mode" (multi-file developments), with two files from this repo + one file for running the game.
Enrico Tassi (Sep 09 2021 at 08:33):I wonder if one can hack the notations to spit <img src="box.png"> rather than #...
Shachar Itzhaky (Sep 09 2021 at 12:34):@Enrico Tassi I love your suggestion! I'll see what I can do :happy:
Emilio Jesús Gallego Arias (Sep 09 2021 at 15:46):The new printer should allow to do this kind of stuff very easily, I'm actively working on it I promise :)
Shachar Itzhaky (Sep 18 2021 at 12:02):@Karl Palmskog @Enrico Tassi @Emilio Jesús Gallego Arias I have created a preview of 0.13.3 and it includes Coqoban. Here is a demo: https://coq-p-wr.vercel.app/scratchpad.html?share=hb-onipalasuh
Karl Palmskog (Sep 18 2021 at 12:10):wow, that looks amazing! :package: :gift:
Shachar Itzhaky (Sep 18 2021 at 13:23):yay :octopus:
Shachar Itzhaky (Sep 18 2021 at 15:32):Should we tweet it? @Karl Palmskog want to do the honors?
Karl Palmskog (Sep 18 2021 at 15:33):ah, I try to stay away from public social media. I think we should get @CoqLang to do it (ping @Emilio Jesús Gallego Arias)
Shachar Itzhaky (Sep 18 2021 at 15:34):lol good for you :D
Shachar Itzhaky (Sep 18 2021 at 15:34):we should add another Goal command to the snippet to show how to access the levels in Coqoban_levels.
Karl Palmskog (Sep 18 2021 at 15:34):maybe you can also generate a more permanent link first?
Karl Palmskog (Sep 18 2021 at 15:35):I think this stuff fits very well with a recent PL community tweet btw: https://twitter.com/chrisamaphone/status/1438162512642519042
would it be possible to encode chess in coq such that an interactive proof of the existence of an end state (i.e. a constructive proof that "wins(white) V wins(black) V stalemate") corresponds to playing the game?
- Chris Martens (@chrisamaphone) Shachar Itzhaky (Sep 18 2021 at 15:37):well for twitter, definitely a transient link is enough; but yeah I was thinking about creating some more pages in our website, perhaps showcasing different things, and some kind of menu linking to them from the front page.
Karl Palmskog (Sep 18 2021 at 15:39):hmm, that's strange, when I open the link now the code is shown for a moment, then I just get a blank editor with one line
Shachar Itzhaky (Sep 18 2021 at 15:39):oh no!
Karl Palmskog (Sep 18 2021 at 15:39):happens both in Firefox and Chrome on Ubuntu
Shachar Itzhaky (Sep 18 2021 at 15:40):this hastebin code has never been tested actually :face_with_thermometer:
Shachar Itzhaky (Sep 18 2021 at 15:41):is it possible that the eviction duration is just a few hours?..
Shachar Itzhaky (Sep 18 2021 at 15:47):looks like it's 24 hours. Which is indeed a bit short, but should have still been there.
Shachar Itzhaky (Sep 18 2021 at 15:58):Looks like it's a Heroku thing. I am on the free tier unfortunately, so I don't really have persistent storage right now.
Shachar Itzhaky (Sep 18 2021 at 17:47):Ok, I switched Hastebin to use Postgres. Was painful! Here is a link that would hopefully last longer: https://coq-p-wr.vercel.app/scratchpad.html?share=hb-aqonifatos
Théo Zimmermann (Sep 19 2021 at 09:50):Testing on Firefox with this new link, I see a serious problem: the notations do not have the same width and therefore the grid doesn't align well.
Théo Zimmermann (Sep 19 2021 at 09:52):Ah same problem in Chromium. I guess the browser is not the problem, the system is. As you wrote, I should comment them out.
Théo Zimmermann (Sep 19 2021 at 09:54):Another problem IMHO is that this is too slow. If we can't manage to optimize Coqoban a little bit to be faster, I'm not sure how good the publicity would be for Coq.
Théo Zimmermann (Sep 19 2021 at 09:55):I was going through Level_274 (the example from the Coqoban README) and each move takes way to long to be really enjoyable.
Shachar Itzhaky (Sep 19 2021 at 12:30):Yes, it's definitely on the slow side. There is the WebAssembly version (https://coq-p-wr.vercel.app/wa/scratchpad.html?share=hb-aqonifatos , basically just add /wa to the URL), but there's no reason to believe it to be faster. I have plans on activating the bytecode compiler in WASM (which is not smt we can do in JS), which will speed it up I guess. Do you support that would positively affect Coqoban?
Shachar Itzhaky (Sep 19 2021 at 12:31):As for the widths, it's a font issue. As my comment above the code explains, on my Mac they happen to have the same width, but YMVW.
Shachar Itzhaky (Sep 19 2021 at 12:31):We can perhaps hack something into jsCoq to force them to align.
Théo Zimmermann (Sep 19 2021 at 13:12):Do you support that would positively affect Coqoban?
I suppose, since it's much faster when running Coq locally. But still, it's not blazing fast either. What I had in mind was that there may be some optimization to do on the Coqoban-side to make it faster on all platforms.
Théo Zimmermann (Sep 19 2021 at 13:13):Something else that would be very useful to make it accessible would be to add buttons for inserting the arrow signs.
Shachar Itzhaky (Sep 19 2021 at 17:23):Yes, I was thinking of having a separate page with a little bit of background, a small menu to select levels, and a few shortcuts for move entry and backtrack. Soon enough we can forget about the fact that it runs Coq underneath :laughter_tears:
Shachar Itzhaky (Sep 23 2021 at 22:22):I made a page for Coqoban: https://coq-next.vercel.app/fun/coqoban.html
I used CSS to format the board instead of Notation. That should be less brittle.
Sometimes it gets stuck in some state where the arrow keys don't work... no idea why.
Théo Zimmermann (Sep 24 2021 at 13:04):It's really cool! Maybe when you win the level, it could suggest typing in Qed into the editor.
Karl Palmskog (Sep 24 2021 at 13:05):yeah, and maybe add a HTML-level comment that more problems are available by changing definition numbers
Théo Zimmermann (Sep 24 2021 at 13:08):It's the case now.
Karl Palmskog (Sep 24 2021 at 13:09):ah, I might have looked at an earlier version.
Karl Palmskog (Sep 24 2021 at 13:09):anyway, I think this is @CoqLang tweet ready :bird:
Théo Zimmermann (Sep 24 2021 at 13:09):Yes, agreed!
Karl Palmskog (Sep 24 2021 at 13:10):be sure to credit @existsshachar and @ejgallego
Théo Zimmermann (Sep 24 2021 at 13:11):@Shachar Itzhaky Do you prefer to tweet from your account and get retweeted by @CoqLang or do you want a tweet originating from @CoqLang?
Shachar Itzhaky (Sep 24 2021 at 13:11):oh I already tweeted from my account and tagged @CoqLang
Shachar Itzhaky (Sep 24 2021 at 13:11):so whatever you like
Karl Palmskog (Sep 24 2021 at 13:13):now we just have to convince Erik to implement the "impossibility checker" for Sokoban that they did in Lean
Shachar Itzhaky (Sep 24 2021 at 13:14):ah lol. how does it work? surely they cannot enumerate all moves..?
Karl Palmskog (Sep 24 2021 at 13:15):no idea, but here's the project: https://github.com/mirefek/sokoban.lean
Karl Palmskog (Sep 24 2021 at 13:15):https://twitter.com/derKha/status/1386315203642630145
@BasspittersBs @XenaProject Without the unsolvability part though it looks like, which seems like the most interesting part!
- Sebastian Ullrich (@derKha) Shachar Itzhaky (Sep 26 2021 at 16:20):Man the Coqoban tweet got fewer likes than Talia's "Normal, Illinois."
The future is weird.
Karl Palmskog (Sep 26 2021 at 16:24):I wonder if a screenshot might have helped?
Oh well, there are more Coq-based games out there for future tweets, you may already have seen Sudoku, which currently uses js_of_ocaml directly with a custom HTML page.
Shachar Itzhaky (Sep 26 2021 at 16:26):yeah although it's OCaml code that was extracted from Coq; it's not that you can solve a puzzle in proof mode like in Coqoban.
Shachar Itzhaky (Sep 26 2021 at 16:27):I really wish I could understand sokoban.lean; it seems that they visualize the proofs as well as the boards. But there is no explanation, not even what each symbol means in their HTML.
Karl Palmskog (Sep 26 2021 at 16:28):yeah, one needs to do some work on top of Sudoku to make it jsCoq friendly, but to my knowledge the extracted functions work fine within Coq as well in their pre-extracted form.
Shachar Itzhaky (Sep 26 2021 at 16:29):fair point
Karl Palmskog (Sep 26 2021 at 16:31):in the same vein, but probably not as straightforward as Sokoban (since likely needs gamified goals/levels): https://github.com/thery/hanoi
Shachar Itzhaky (Sep 26 2021 at 16:36):looks familiar. I might have reviewed the paper at some point :whale:
Emilio Jesús Gallego Arias (Sep 26 2021 at 18:49):@Shachar Itzhaky I didn't have time to go thru this paper, but Lean may likely be using this https://drops.dagstuhl.de/opus/volltexte/2021/13899/pdf/LIPIcs-ITP-2021-4.pdf
Karl Palmskog (Sep 26 2021 at 18:58):that's a pretty idiosynchratic design choice to put the whole GUI framework inside the ITP. How soon will bitrot set in? ITP GUIs probably comprise the most consistent software elephant graveyard I know of...
Emilio Jesús Gallego Arias (Sep 26 2021 at 19:10):I need to read the paper before we comment, but to some point you want to have nice access inside Coq for a rich system of UI stuff. We have notations, but they have their limitations. I have a branch with a new printer for Coq that is about to get published, so hopefully we can experiment a bit more w.r.t. display
Shachar Itzhaky (Sep 26 2021 at 19:36):Emilio Jesús Gallego Arias said:
Shachar Itzhaky I didn't have time to go thru this paper, but Lean may likely be using this https://drops.dagstuhl.de/opus/volltexte/2021/13899/pdf/LIPIcs-ITP-2021-4.pdf
That one I clearly remembering bidding on but did not get a chance to review. Guess it was popular...
Laurent Théry (Sep 27 2021 at 09:39):Karl Palmskog said:
in the same vein, but probably not as straightforward as Sokoban (since likely needs gamified goals/levels): https://github.com/thery/hanoi
there is also another game T2048 that could also be beautified https://github.com/thery/T2048
Julien Narboux (Apr 25 2022 at 13:10):Hi, the Coqoban example is very nice. More generally, it would be nice to have beautiful maths notations, but just for display like in maple, not for input. Would that be possible to use jscoq with mathjax or mathml ?
Shachar Itzhaky (Apr 25 2022 at 16:11):We are working in that exact direction! @Emilio Jesús Gallego Arias is developing a new pretty-printer that will allow much better customization. If you can provide example cases with perhaps a mockup or some accompanying graphics that would be very helpful for mapping potential needs.
Emilio Jesús Gallego Arias (Apr 26 2022 at 16:51):Yes @Julien Narboux , it'd be great. Now we are a bit limited as notations in particular are not printed in a structured way, so for example for \sum_(i in S) i^2 you get <notation>\sum_(</notation><var>i</var><notation> in </notation>.... with makes hard for the HTML frontend to recognize and refine. Indeed we have a prototype of a printer that prints notations respecting structure, there is a branch coq-layout in the jsCoq repos. I hope we can make progress soon.
Emilio Jesús Gallego Arias (Apr 26 2022 at 16:52):Once that branch is ready we will have <notation key="_ = _"><args> .... </args> ... etc so indeed we could replace that in the frontend with a table to mathjax or other useful stuff. Do you have ideas / examples of in-production tech doing this? It would be good to have some proper related work to be able to anticipate problems.
Last updated: May 31 2023 at 02:31 UTC