Hi all, I'm experimenting with writing a custom frontend for Coq using blockly. In terms of using jscoq/wacoq for a backend, are there any resources on disabling the default javascript div injection and/or calling into the API directly? Cheers!
Hi! This is an ongoing shortcoming of jsCoq; the API exists but it is quite unstable and not documented. Here is a small snippet that showcases loading jsCoq and programmatically invoking some proof manipulation, that I created for a similar request in the past.
playful.html
it assumes jsCoq installed via NPM (npm install jscoq
from the same directory that contains playful.html
; then serve the directory over http).
Hi Shachar, thanks for this, that is very helpful! I'll give it a peruse.
Hi @Archibald Neil MacDonald , I'm busy today, I will get back to you with more detail soon, but someone did already implement a blocky frontend for jsCoq
let me contact them and see if the code is available already
Hello @Archibald Neil MacDonald! Sorry for the follow-up, I'm the person that @Emilio Jesús Gallego Arias was referring to. I did implement an online frontend for Coq using Blockly and jsCoq, and it's available at https://henblocks.github.io/. Not sure if this is super useful though, because I still made use of the default javascript div injection. The source code is available at https://github.com/henblocks/henblocks.github.io. This was part of a final year project for my undergrad, so it's very much just a prototype. Apologies for the lack of documentation/tutorials, I do hope to add them in the future if possible. Happy to chat more if you'd like to!
That is absolutely adorable!!
Last updated: Sep 15 2024 at 13:02 UTC