coq-serapi
coq-serapi copied to clipboard
ejgallego
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
I want to work with different proof branches. It seems that option `ontop` of `Add` command is designed specifically for this use case, however, when I try to use it...
Hi Emilio, Hope you're doing OK despite the crazy times. In the project I'm workig on, it would be very useful to be able to get comments boundaries in addition...
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...
The `!pinned` flag is currently used in the version-tracked opam package definition (`coq-serapi.opam`). However, this flag seemingly causes CI failures in the upstream opam repository, so it should never be...
I'm not sure what the proper way is to do this without breaking existing code. It's just a bit unfortunate that SerAPIs options are not spelled the same as Coq's
I'm trying to set up code for serialization via `sercomp` of some proof goal information, but am running into issues. Consider the following example (`pi.v`): ```coq From mathcomp Require Import...
I don't think this is coq-serapi's fault per se, but I find this behavior a little annoying to deal with: ``` (0 (Control (StmAdd () "Require Import List."))) (Answer 0...
The title says it all. This is a first step towards becoming a Jupyter kernel. The basic resources are: - https://github.com/akabe/ocaml-jupyter - https://github.com/andrewray/iocaml - http://jupyter-client.readthedocs.io/en/latest/kernels.html - https://github.com/dsblank/simple_kernel
https://github.com/google/kythe is an interesting framework we could make our tool talk to.