Unclear how to use SerAPI demo about coq-serapi HOT 3 CLOSED

Wonderful. Thank you!

from coq-serapi.

Hi @joelburget indeed there are two problems here:

1. Coq's Prelude is not loaded by the web version. [hence the parsing error].
2. The documentation of the protocol itself is poor.

Point 1 should be solved the next time I update the web build, as it was due to a limitation of the old library pre-loading API that was solved in 8.8. The workaround is to do (Add () "From Coq Require Import Prelude.") first.

Regarding point 2, documentation for the protocol is indeed incomplete as a major revision is expected for Coq 8.9. The new protocol revision will indeed pretty well documented and expected to be "stable", so I didn't bother to write a lot about the current one.

I'll try to improve the README tho. The command line help for sertop is a bit better in this regard. Anyways, most of the relevant information can be extracted from the mli file:

type answer_kind =
    Ack
  | Completed
  | Added     of Stateid.t * Loc.t * [`NewTip | `Unfocus of Stateid.t ]
  | Canceled  of Stateid.t list
  | ObjList   of coq_object list
  | CoqExn    of Loc.t option * (Stateid.t * Stateid.t) option * Printexc.raw_backtrace * exn

type cmd =
  | Add        of add_opts  * string
  | Cancel     of Stateid.t list
  | Exec       of Stateid.t
  | Query      of query_opt * query_cmd
  | Print      of print_opt * coq_object

The Help command is also supported and should provide some help, but it is sadly outdated.

from coq-serapi.

Ok the demo is updated, most problems should be fixed. I'll also push a release build to jscoq-builds under the proper branch.

from coq-serapi.