Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias
As discussed in chat rooms, we would like to provide a JSON interface to SerAPI; more generally, we would like to make the main code parametric w.r.t. serialization method so...
We update JS library manager to newer jsCoq code. This almost works, however, there are some API deficiencies in jsCoq that must be solved before we can make this function...
Since the inception of SerAPI providing a way to query dependency data was a goal. In fact, this is possible to do now by clients and you can dump the...
We want to add a benchmarking mode to sercomp. We could gather statistics section, module and sentence. With a bit of help from the STM we could do quite well....
We want to compile SerApi to Javascript, Coq will run in a worker thread. Thanks to [jsCoq](https://github.com/ejgallego/jscoq) how to this is well understood. Once this is complete, jsCoq will just...
Since the beginning, the manual override / re-export of Coq's type using `ppx_import` has been done manually [with the help of some hacky scripting]. It was planned to use a...
I'm opening this issue [would a discussion be better, tho it overlaps with Zulip] to keep track of the general road-map for SerAPI. Thanks to tools like https://github.com/cpitclaudel/alectryon , and...
As witnessed by #68, we have a very important problem with the current situation of generic arguments in Coq. As of today, we need to add manually the serializers, which...
We should support LSP to some degree. https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
SerAPI should support the async proof mode. Experimental support is already in place, however more testing is needed. Remaining tasks are: - [ ] Teach our internal document mode of...