ejgallego/coq-serapi

Issues

• [PATCH] Compilation with yojson >= 2.2

  #420 opened 3 months ago by SnarkBoojum
  3

• CoqSerapi Usage Question

  #418 opened 3 months ago by ana-brendel
  6

• Missing conversion functions for types for the extraction plugin?

  #371 opened 7 months ago by toku-sa-n
  3

• Support for 8.13?

  #227 opened 3 years ago by gmalecha
  4

• macOS: serapi loads Coq .vo from compile time path

  #382 opened 3 months ago by MSoegtropIMC
  5

• New versioning scheme.

  #400 opened 3 months ago by ejgallego
  1

• License issue

  #411 opened 4 months ago by SnarkBoojum
  1

• Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

  #396 opened 5 months ago by rtetley
  5

• Run tests with MC 2

  #395 opened 6 months ago by SnarkBoojum
  3

• Segmentation fault in coq/getDocument call

  #397 opened 6 months ago by Nfsaavedra
  4

• Licensing needs to be clarified

  #266 opened 7 months ago by SnarkBoojum
  18

• Windows PATH length (again)

  #377 opened 7 months ago by MSoegtropIMC
  21

• Expose Section Variable Determining API in SerAPI

  #339 opened 7 months ago by HazardousPeach
  6

• Incorrect goals when providing -topfile in sertop 8.10.0+0.7.2

  #348 opened 7 months ago by a-gardner1
  2

• Can't run `make test` due to an error related to `eqType`

  #373 opened 9 months ago by toku-sa-n
  4

• What is the purpose of coq-serapi's existance and why can't everything be done in coqtop?

  #332 opened 10 months ago by brando90
  5

• Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

  #364 opened a year ago by rtetley
  1

• Segfault on (Query () Goals) with sertop 8.15.0+0.15.3

  #331 opened a year ago by rwhender
  4

• Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

  #324 opened a year ago by MSoegtropIMC
  12

• [meta] General roadmap

  #252 opened 2 years ago by ejgallego
  11

• what version of coq serapi works with coq 8.10.2?

  #319 opened 2 years ago by brando90
  9

• what is the best version of coq-serapi that works with coq 8.12?

  #320 opened 2 years ago by brando90
  5

• installation

  #317 opened 2 years ago by ASamSam
  4

• Make sertop respond consistently to SIGINT

  #234 opened 2 years ago by elidupree
  2

• Missing build dependency on mathcomp's ssreflect

  #283 opened 2 years ago by SnarkBoojum
  2

• Is it possible to check if the sent coq statement is a tactic with serapi?

  #285 opened 2 years ago by brando90
  1

• Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

  #277 opened 2 years ago by MSoegtropIMC
  22

• How to handle "Needs option -impredicative-set."

  #287 opened 2 years ago by dhilst
  3

• Nix expression for coq-serapi

  #241 opened 3 years ago by raghnysh
  32

• Is sercomp broken in v8.16?

  #286 opened 2 years ago by artagnon
  2

• Querying proof state in coq-serapi `Query (PrettyStrings, Lists) Goals`

  #269 opened 2 years ago by brando90
  2

• Why don't the responses from coq-serapi corresponds to type definitions on the coq code?

  #273 opened 2 years ago by brando90
  2

• Do I always have to wrap anonymous functions in a definition for Coq Serapi to parse it for me?

  #272 opened 2 years ago by brando90
  1

• deps bug (`coq-serapi` incompatible with newest `cmdliner`, making some Docker-Coq builds fail) + question

  #267 opened 2 years ago by erikmd
  7

• How to have serapi return to me coq human strings from arbitrary subterms in a coq-ast?

  #274 opened 2 years ago by brando90
  5

• Serapi perhaps giving a strange human string of proof states after induction?

  #280 opened 2 years ago by brando90
  4

• Using SerAPI as an external module in a Coq plugin

  #247 opened 2 years ago by efirst
  1

• issues installing coq serapi? maybe it's due to m1 arm chip?

  #279 opened 2 years ago by brando90
  8

• issue when loading mathcomp/HB

  #260 opened 2 years ago by affeldt-aist
  9

• Querying proof term directly with `Query`

  #270 opened 2 years ago by brando90
  13

• Why does TacArg accepts a value of CAst.t type when it should only accept values of types

  #275 opened 2 years ago by brando90
  2

• Support for Coq 8.15

  #264 opened 2 years ago by erikmd
  10

• How does one transform a serapi expression into a normal human readable coq string?

  #268 opened 2 years ago by brando90
  3

• Support coq 8.14

  #263 opened 3 years ago by SnarkBoojum
  3

• Simple query prints raw Pretype_errors.Pretype error, produces 18MB of output

  #250 opened 3 years ago by cpitclaudel
  2

• [feature request] Ability to save .vo file from interactive session

  #238 opened 3 years ago by JasonGross
  3

• Missing newline between multiple goals for some format settings

  #231 opened 3 years ago by elidupree
  0

• [Regression] Anomaly: grounding a non evar-free term

  #228 opened 4 years ago by cpitclaudel
  2

• Protocol documentation link in the README is broken

  #226 opened 4 years ago by zhaoyu-li
  2

• Protocol documentation link in the README is broken

  #225 opened 4 years ago by shlevy
  2