Hello everyone!
I want to implement Hackenbush in Rocq. I know about Coqoban, but that game manipulated the proof state and stuff. Is there a way to do this the normal fp way i.e. printing out to the screen and stuff?
Thank you!
I think the answer must be yes, e.g. there must be something to hook into the Qed/Defined or equivalent. But:
<< jsCoq’s main entry point is the CoqManager JavaScript object used for launching a Coq worker and embedding Coq functionality in your particular application, blog, or webpage. >>
If you find documentation for that CoqManager (maybe I have missed it but I cannot find it, as opposed to “running examples” or the “copy and adapt”), i.e. the actual JS/DOM API, I’d gladly give you a hand…
The short answer is no, Rocq is a purely functional programming language, but there are many possible workarounds depending on what you are trying to achieve.
For instance, when executing a tactic, idtac lets you print messages.
This library coq-io-system 2.4.1 (latest) · Rocq Package provides an effect system for Rocq that you can use to code effectful programs, but to run them, you need to extract the code to OCaml first.
Also relying on extraction to run the program, this library coq-coqffi 1.0.0~beta8 (latest) · Rocq Package gives you a way to bind Rocq code to OCaml libraries (so you could imagine using even graphical libraries).
Finally, if you are targeting a specific UI (like jsCoq), then you could try to use the Rocq notation system to generate, e.g., SVG code (some use it to generate C code!) and then have the interface display this in a particular way.
The short answer is yes even in CoqIDE, one can print to the message window, not to mention the way of plugins…
Anyway, the OP is apparently referring to this:
https://github.com/rocq-community/coqoban
https://coq.vercel.app/fun/coqoban.html
But then again, where is jsCoq/CoqManager documented? It isn’t, and that is a “no”… or a “maybe not”, maybe the OP is talking of something else…
If one is only concerned with Output and plays with tactic, Ltac2 could probably be extended with advanced printing abilities