Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias
As of today, when hovering over a notation in the goal buffer for example, jsCoq will detect that a notation is there and try show the definitions of such notation....
Support for `vm_compute` should be feasible by using [emscripten](https://github.com/kripken/emscripten) to compile the VM. This should be a fun project, a good place to start is at: https://github.com/ejgallego/jscoq/blob/196d2fbd8a3e62d2c8cd9c1c89531fe91960caee/lib-js/coq_vm.js Things broken due...
When using `Search` or `SearchAbout` with a large number of modules loaded, browsers produce a `Stack_overflow` exception. This is unfortunate and due to `js_of_ocaml` not optimizing tail calls, see: -...
After #117 is merged we should figure out a way to auto-deploy to jscoq.github.io There are some instruction on how to do that for Coq; we could even keep all...
The following tweet https://twitter.com/paf31/status/1228017902554505216 reminded me of one of the original goals of jsCoq. > I want there to be a way in GHC or PureScript to interactively explore error...
Currently, if the user requires a package such as `Coq.Lists.List` jscoq will fail unless the user manually loaded the package. It would be nice if we could intercept the Require...
Adding new theories to jscoq is kinda hard as you need to compile the `.vo` files with the same exact version of Coq. However, jsCoq can already compile `.vo` files...
[Original request and idea by @gares] We'd like JsCoq to implement a systematic a (possibly configurable) timeout to stop looping executions. IMO, the best approach may be to modify Coq...
It could be interesting to host our whole documents in a single editor instance, such as quill https://quilljs.com/
Our egg to indicate download progress is cool, but I'd be great to have also information on remaining megabytes.