ejgallego/coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
CoqNOASSERTION
Issues
- 3
[PATCH] Compilation with yojson >= 2.2
#420 opened by SnarkBoojum - 6
CoqSerapi Usage Question
#418 opened by ana-brendel - 3
- 4
Support for 8.13?
#227 opened by gmalecha - 5
- 1
New versioning scheme.
#400 opened by ejgallego - 1
License issue
#411 opened by SnarkBoojum - 5
- 3
Run tests with MC 2
#395 opened by SnarkBoojum - 4
Segmentation fault in coq/getDocument call
#397 opened by Nfsaavedra - 18
Licensing needs to be clarified
#266 opened by SnarkBoojum - 21
Windows PATH length (again)
#377 opened by MSoegtropIMC - 6
- 2
- 4
- 5
What is the purpose of coq-serapi's existance and why can't everything be done in coqtop?
#332 opened by brando90 - 1
- 4
- 12
- 11
[meta] General roadmap
#252 opened by ejgallego - 9
what version of coq serapi works with coq 8.10.2?
#319 opened by brando90 - 5
- 4
installation
#317 opened by ASamSam - 2
Make sertop respond consistently to SIGINT
#234 opened by elidupree - 2
Missing build dependency on mathcomp's ssreflect
#283 opened by SnarkBoojum - 1
- 22
- 3
How to handle "Needs option -impredicative-set."
#287 opened by dhilst - 32
Nix expression for coq-serapi
#241 opened by raghnysh - 2
Is sercomp broken in v8.16?
#286 opened by artagnon - 2
- 2
Why don't the responses from coq-serapi corresponds to type definitions on the coq code?
#273 opened by brando90 - 1
Do I always have to wrap anonymous functions in a definition for Coq Serapi to parse it for me?
#272 opened by brando90 - 7
deps bug (`coq-serapi` incompatible with newest `cmdliner`, making some Docker-Coq builds fail) + question
#267 opened by erikmd - 5
How to have serapi return to me coq human strings from arbitrary subterms in a coq-ast?
#274 opened by brando90 - 4
Serapi perhaps giving a strange human string of proof states after induction?
#280 opened by brando90 - 1
Using SerAPI as an external module in a Coq plugin
#247 opened by efirst - 8
- 9
issue when loading mathcomp/HB
#260 opened by affeldt-aist - 13
Querying proof term directly with `Query`
#270 opened by brando90 - 2
Why does TacArg accepts a value of CAst.t type when it should only accept values of types
#275 opened by brando90 - 10
Support for Coq 8.15
#264 opened by erikmd - 3
How does one transform a serapi expression into a normal human readable coq string?
#268 opened by brando90 - 3
Support coq 8.14
#263 opened by SnarkBoojum - 2
Simple query prints raw Pretype_errors.Pretype error, produces 18MB of output
#250 opened by cpitclaudel - 3
- 0
- 2
- 2
Protocol documentation link in the README is broken
#226 opened by zhaoyu-li - 2
Protocol documentation link in the README is broken
#225 opened by shlevy