coq-serapi
coq-serapi copied to clipboard
ejgallego
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
I'm working on packaging coq-serapi for Debian, and things are pretty annoying: - the main LICENSE file says LGPL-2.1+ and GPL-3+ for most things that looks pretty clear - but...
Hello, I'm using SerAPI to execute Coq code and extract the AST for each Coq command. I occasionally run into the following error: the returned AST is empty. ``` (Add...
Hi @ejgallego, FYI after the bump of opam to 2.1.2 in `coqorg/base` (coq-community/docker-base#17), I rebuilt all `coqorg/coq` images ([pipeline](https://gitlab.com/coq-community/docker-coq/-/pipelines/507529655)) but some jobs failed: https://gitlab.com/coq-community/docker-coq/-/jobs/2284076471 https://gitlab.com/coq-community/docker-coq/-/jobs/2284076472 with the same error: ```bash...
Hi, I am just forwarding an issue identified @Zimmi48 that I seem to have run into when testing alectryon. It seems to be an issue that arises by just loading...
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...
Hey @ejgallego, How hard would it be to expose parent-child relationships between goals in the API? At the moment SerAPI prints less information than `coqtop -emacs` (the latter has 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...
Hi! I'm trying to use SerAPI as an external module in a Coq plugin. On Zulip, Emilio gave me some pointers about using `Declare ML Module` in my plugin .v...
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...
`sercomp --mode=print ` produces a `.v` without the comments in the original.
