coq-serapi
coq-serapi copied to clipboard
ejgallego
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
As of today, we have a few parts of the Ast that are using piercing due to Coq not exporting the necessary definitions. We should add tests for each piece...
Fixes #339 Example: ```lisp (Add () "Section foo. Variable (a : nat). Definition b : nat. Proof. exact a. Qed. End foo.") (Exec 7) (Query ((sid 7)) (SecVars b)) (Answer...
The ML API has a mechanism to determine which section variables were used by a proof. Ideally, SerAPI would also allow this. Emilio's comment on Zulip here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Determining.20section.20variables.20used/near/365974818
I'm working with @rwhender (see https://github.com/ejgallego/coq-serapi/issues/331) in a project using `sertop` to interact with old commits of various Coq projects as part of data collection for AI/ML proof engineering datasets...
After some thinking, I have decided to implement the `coq-lsp` versioning model for Coq SerAPI. This has a lot of advantages, in particular w.r.t. change tracking. That means that we...
The file sertop/sertop.el is licensed under GPL-3+ and isn't mentioned in LICENSE. (and I didn't see it either, so my Debian package got rejected)
See https://github.com/ejgallego/coq-lsp/pull/698
Adapt to https://github.com/coq/coq/pull/19310 This should be merged in sync with the upstream PR
Compiling coq-serapi with yojson >= 2.2 means running `find serlib -type f |xargs sed -i -e "s/Result.result/Result.t/g"` ; I just fixed the issue in Debian.