ejgallego / coq-serapi Goto Github PK

I'm seeing that in sertop, if I enter a very long command more than say 5,000 characters as a single line without line breaks, I'm seeing sertop hang with no response. If I then interrupt it, I can continue entering commands with no problems. I've also found that if I split my 5,000-character command up into multiple lines, then the command can be processed without a problem.

From further testing, it looks as though lines are getting truncated to 4,096 characters. I've found that commands split across lines shorter than that limit will succeed, and lines that are longer than that start producing errors. Further support for the line truncation theory: if I enter the full 5,000+ character command on a single line (so that sertop hangs), I can then enter a whole bunch of closing parentheses to trigger a Sexplib.Conv.Of_sexp_error, so sertop isn't really hanging per se; it's truncated the input and is still waiting for the end of the expression.

My specific example won't lend itself well to reproducibility due to dependencies, but all I'm doing is trying to use Print on a (very) large AST:

(Print () (CoqAst [large AST]))

where the CoqAst is a result of running (Query () (Ast [stateid])).

Ideally, it would be nice if sertop didn't have this line length limit at all, or if it could show an error message when the limit is exceeded.

Many Coq codebases use _CoqProject files so that an IDE can pass needed flags to coqtop. It would be nice if sertop could make use of the same resource.

One way to do this would be via a command-line flag, say, "-project-location". The Emacs interface should be able to query the user when sertop starts to be able to pass that to sertop (it could be an option whether to make that query or not).

I believe that PG just reads _CoqProject and inlines its contents to pass to coqtop directly.

SerAPI builds with coq/coq@4b7e1cc but not with coq/coq@bc5cdc6.

Pressing C-d to exit yields an extra message:

$ /build/coq-serapi/sertop.native
# Press C-d here

(Answer""Ack)
(Answer""Completed)

We would to support integration with
https://github.com/the-lambda-church/coquille

For now, the following are needed:

• OPAM support #25
• Reliable full document parsing #5

The build now fails with

File "serlib/plugins/ltac/ser_tacexpr.ml", line 79, characters 0-262:
Error: This variant or record definition does not match that of type
         'a Tacexpr.core_destruction_arg
       The types for field ElimOnIdent are not equal.

The commit that breaks the build is coq/coq@fc218c26c (and notably not the earlier commit that reorganizes API/API.ml).

Assume the following document:

Lemma a : True.
  idtac.
  urgh.
  idtac.

I run the following commands in sertop.el:

(add-lemma (Control (StmAdd 1 2 "Lemma a : True.")))
  (Answer add-lemma Ack)
  (Answer add-lemma
          (StmAdded 3
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 15))
                    NewTip))
  (Answer add-lemma Completed)
(add-idtac (Control (StmAdd 1 3 "\n  idtac.")))
  (Answer add-idtac Ack)
  (Answer add-idtac
          (StmAdded 4
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 3)
                     (ep 9))
                    NewTip))
  (Answer add-idtac Completed)
(add-urgh (Control (StmAdd 1 4 "\n  urgh.")))
  (Answer add-urgh Ack)
  (Answer add-urgh
          (StmAdded 5
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 3)
                     (ep 8))
                    NewTip))
  (Answer add-urgh Completed)
(add-idtac-2 (Control (StmAdd 1 5 "\n  idtac.")))
  (Answer add-idtac-2 Ack)
  (Answer add-idtac-2
          (StmAdded 6
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 3)
                     (ep 9))
                    NewTip))
  (Answer add-idtac-2 Completed)
(observe (Control (StmObserve 6)))
  (Answer observe Ack)
  (Feedback
   ((id
     (State 6))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 5))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 4))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 2))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 4))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 5))
    (contents
     (ErrorMsg
      ((fname "")
       (line_nb 1)
       (bol_pos 0)
       (line_nb_last 1)
       (bol_pos_last 0)
       (bp 3)
       (ep 7))
      "Error: The reference urgh was not found in the current environment."))
    (route 0)))
  (Answer observe
          (CoqExn
           ("Cerrors.EvaluatedError(_, 0)")))

At this point, how can I know which sentences are invalid? I tried EditAt:

(edit-at (Control (StmEditAt 4)))
  (Answer edit-at Ack)
  (Feedback
   ((id
     (State 4))
    (contents Processed)
    (route 0)))
  (Answer edit-at
          (StmEdited NewTip))
  (Answer edit-at Completed)

But I'm not sure how to interpret the result. Does this mean that everything after state 4 needs to be invalidated?

Thanks!

Version

Coq 8.7.1, CompCert 3.2

Operating system

macOS 10.13.3

The problem

If you use

sertop --implicit -R lib,compcert.lib -R common,compcert.common -R x86_64,compcert.x86_64 -R x86,compcert.x86 -R backend,compcert.backend -R cfrontend,compcert.cfrontend -R driver,compcert.driver -R flocq,compcert.flocq -R exportclight,compcert.exportclight -R cparser,compcert.cparser

and use ReadFile to read Parser.v in the cparser folder, and then use (Query () (Ast x)) to get the ASTs of its sentences one by one, the SerAPI process will freeze at a point, and Ctrl+C cannot end the process. This could result from the fact that Parser.v has more than 34,000 lines of code. However, could you fix this issue? Since coqc has no problem compiling the file.

Feedback has the capability to send Coq .glob information messages. However, I am not sure this is really useful, and it is very very verbose.

What do @cpitclaudel @Ptival think ?

It is enabled in the current build, but I dunno what to do.

edit: We will implement a feedback filter in SerAPI, so clients can opt-out to receive certain kinds of feedback.

Hello, I have a problem with the sertop REPL.
It gets stuck when I copy-and-paste a very long command into sertop. The same issue happens also when I try to interact with sertop using a pseudo-terminal in a Python program.
But it is OK if I pass the command via a pipe (echo $a_long_command | sertop) .
So I guess it's related to how keyboard input is handled. Any idea? Thanks.

An example command is :

(Add () "Check fun c : comparison => match c as c0 return (forall c' : comparison, ~ c0 <> c' -> c0 = c') with | Eq => fun c' : comparison => match c' as c0 return (~ Eq <> c0 -> Eq = c0) with | Eq => fun _ : ~ Eq <> Eq => eq_refl | Lt => fun H : ~ Eq <> Lt => let n : False := H (fun H0 : Eq = Lt => let H1 : False := eq_ind Eq (fun e : comparison => match e with | Eq => True | _ => False end) I Lt H0 in False_ind False H1) in match n return (Eq = Lt) with end | Gt => fun H : ~ Eq <> Gt => let n : False := H (fun H0 : Eq = Gt => let H1 : False := eq_ind Eq (fun e : comparison => match e with | Eq => True | _ => False end) I Gt H0 in False_ind False H1) in match n return (Eq = Gt) with end end | Lt => fun c' : comparison => match c' as c0 return (~ Lt <> c0 -> Lt = c0) with | Eq => fun H : ~ Lt <> Eq => let n : False := H (fun H0 : Lt = Eq => let H1 : False := eq_ind Lt (fun e : comparison => match e with | Lt => True | _ => False end) I Eq H0 in False_ind False H1) in match n return (Lt = Eq) with end | Lt => fun _ : ~ Lt <> Lt => eq_refl | Gt => fun H : ~ Lt <> Gt => let n : False := H (fun H0 : Lt = Gt => let H1 : False := eq_ind Lt (fun e : comparison => match e with | Lt => True | _ => False end) I Gt H0 in False_ind False H1) in match n return (Lt = Gt) with end end | Gt => fun c' : comparison => match c' as c0 return (~ Gt <> c0 -> Gt = c0) with | Eq => fun H : ~ Gt <> Eq => let n : False := H (fun H0 : Gt = Eq => let H1 : False := eq_ind Gt (fun e : comparison => match e with | Gt => True | _ => False end) I Eq H0 in False_ind False H1) in match n return (Gt = Eq) with end | Lt => fun H : ~ Gt <> Lt => let n : False := H (fun H0 : Gt = Lt => let H1 : False := eq_ind Gt (fun e : comparison => match e with | Gt => True | _ => False end) I Lt H0 in False_ind False H1) in match n return (Gt = Lt) with end | Gt => fun _ : ~ Gt <> Gt => eq_refl end end.")

Another example:

(Add () "this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.")

Feedback objects seem to use symbols in places where strings could be more appropriate; for example, when starting sertop, I see the following:

  (Feedback
   ((id
     (State 2))
    (contents
     (FileLoaded Coq\.Init\.Notations /build/coq/theories/Init/Notations\.vo))
    (route 0)))
  (Feedback
   ((id
     (State 2))
    (contents
     (FileDependency
      (/build/coq/theories/Init/Prelude\.vo)
      Coq\.Init\.Logic))

I wonder if this wouldn't be better as

  (Feedback
   ((id
     (State 2))
    (contents
     (FileLoaded "Coq.Init.Notations" "/build/coq/theories/Init/Notations.vo"))
    (route 0)))
  (Feedback
   ((id
     (State 2))
    (contents
     (FileDependency
      ("/build/coq/theories/Init/Prelude.vo")
      "Coq.Init.Logic"))

What do you think?

We'd like to add support for evar querying.

The XML protocol already provides some support, see
https://github.com/coq/coq/blob/trunk/ide/ide_slave.ml#L223

Also, https://coq.inria.fr/bugs/show_bug.cgi?id=4504 seems very relevant.

We want to add a benchmarking mode to sercomp. We could gather statistics section, module and sentence. With a bit of help from the STM we could do quite well.

An open quesiton is what to use for analytics of the data, maybe Core_bench could help here?

We want to have a mode where sercomp can be a drop-in for coqc. We want to have our own modern set of options (see #19) but also for #32, we really want to support at least the most common options -Q and -R.

I tried to build the newest version of SerAPI today after not having touched it for some time. The instructions state that I should install opam install ocamlfind ocamlbuild ppx_import cmdliner core_kernel sexplib ppx_sexp_conv camlp5, which I did and worked gloriously but installed sexplib version 133.33 by default. This version seems to be missing a key method Conv.Exn_converter.add. Installing sexplib>=114.0 solved the issue.

I do not know if there is an analogue of package.json in OPAM, but this at least can be added to the docs.

Hey Emilio,

What does the new integer in StmAdd do?

(test (Control (StmAdd 0 2 "Goal forall n, n + 0 = n.")))
                       ^ this one
  (Answer test Ack)
  (Answer test Completed)

Also, does StmAdd no return the added state any more? It used to show the state id for the sentence that was just added. It still seems to do that if I pass it a number greater than 0 though :)

Thanks!

We want to identify and support the set of command line options that users need.

Ideally we'd like to break with current coqtop options, but we may add a compatibility layer where justified.

Hello,

I have an "Unable to locate library Cring" error when executing (Add () "Require Export Cring.") in sertop. But it's OK to run this command in Coq IDE, or in sertop using the full name ((Add () "Require Export Coq.setoid_ring.Cring.")).
Any idea? Thanks.

The full error message. Coq version 8.8.0

(Answer 0 Ack)
(Feedback
 ((doc_id 0) (span_id 2) (route 0) (contents (ProcessingIn master))))
(Feedback ((doc_id 0) (span_id 1) (route 0) (contents Processed)))
(Feedback
 ((doc_id 0) (span_id 2) (route 0)
  (contents
   (Message Error
    (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
      (bol_pos_last 0) (bp 15) (ep 20)))
    (Pp_box (Pp_hovbox 0)
     (Pp_glue
      ((Pp_string Unable) (Pp_print_break 1 0) (Pp_string to)
       (Pp_print_break 1 0) (Pp_string locate) (Pp_print_break 1 0)
       (Pp_string library) (Pp_print_break 1 0) (Pp_string Cring.))))))))
(Answer 0
 (CoqExn
  (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
    (bol_pos_last 0) (bp 15) (ep 20)))
  ((1 2)) (Backtrace ())
  (CErrors.UserError (locate_library "Unable to locate library Cring."))))
(Answer 0 Completed)

@cpitclaudel suggests:

Do you think we could extend Goals to take a state id?

I am not 100% sure how the async Stm interacts with the proof engine. My guess is that the current proof object corresponds to the current Stm reached state. This is basically the last observed state.

Thus, we could try something like observe + query, but keep in mind that this could be very expensive!
I don't know if there could be a better way. If you agree I can implement this thou.

An interesting alternative would be to cache the goals object for every reached state. But we would need an Stm callback to do this efficiently. I dunno if the current callbacks in stm.mli are enough.

(I guess I'll try to spam @gares again, if he makes me pay a beer for every mention I'll go broke XD)

It would be good for the rhino-hawk demo to come with instructions. Right now the only clue what to type comes from this repo's README, which starts with (Add () "Lemma addn0 n : n + 0 = n. Proof. now induction n. Qed."). But, this doesn't work in the online SerAPI demo.

> (Add () "Lemma addn0 n : n + 0 = n. Proof. now induction n. Qed.")

(Answer 0 Ack)

(Answer 0(CoqExn(((fname"")(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 18)(ep 19)))()(Backtrace())(Stream.Error"'.' expected after [vernac:gallina] (in [vernac_aux])")))

(Answer 0 Completed)

I don't think this is coq-serapi's fault per se, but I find this behavior a little annoying to deal with:

(0 (Control (StmAdd () "Require Import List.")))
(Answer 0 Ack)
(Feedback((id(State 1))(contents Processed)(route 0)))
(Feedback((id(State 2))(contents(ProcessingIn master))(route 0)))
(Feedback((id(State 1))(contents Processed)(route 0)))

(Feedback((id(State 2))(contents(Message Error(((fname"")(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 15)(ep 19)))(Element(_()((PCData"Error: Unable to locate library List."))))))(route 0)))

(Answer 0(CoqExn(Errors.UserError(locate_library"Unable to locate library List."))))
(Answer 0 Completed)

My issue is that I'd like to know to what input sentence the feedback message that's highlighted belongs to. Usually, I first receive a (Answer 0 (StmAdded 2 ...)) which lets me relate query 0 to state id 2. Then upon receiving the feedback message, I know that if it says id(State 2), the error location relates to the sentence 0.

But for such a failure, I see id(State 2) in the feedback message without ever having received any information linking command 0 to state id 2.

This looks like I'm going to have to be more "stateful", do you know if there's any way to go around this?

We want to compile SerApi to Javascript, Coq will run in a worker thread.

Thanks to jsCoq how to this is well understood. Once this is complete, jsCoq will just use SerAPI as its Coq implementation. For now, we will just communicate sending strings with the usual Sexp.

To do list is:

• Notifications for the library manager/redesign.
• Native JSON encoding of feedback.
• Add js makefile target, SerTop Worker object.
• Import library/fs manager.
• Investigate size reduction strategy. SerTop is 3MiB larger than jsCoq. Core is adding 1.8MiB so it is a large price to pay.

In sertop, if I issue an Add command containing vernacular like this for example:

> (Add () "Check true.")
(Answer 0 Ack)
(Answer 0(Added 2((fname"")(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 0)(ep 11))NewTip))
(Answer 0 Completed)

There is no Feedback entry for the output that would be generated by this. But if I follow this up with a Query command, then I get Feedback results for both the Add and the Query like this:

> (Query () (Vernac "Check 1."))
(Answer 1 Ack)
(Feedback((id 2)(route 0)(contents(ProcessingIn master))))
(Feedback((id 1)(route 0)(contents Processed)))
(Feedback((id 2)(route 0)(contents(Message Notice()(Pp_glue((Pp_tag constr.reference(Pp_string true))Pp_force_newline(Pp_string"     : ")(Pp_tag constr.reference(Pp_string bool))))))))
(Feedback((id 2)(route 0)(contents Processed)))
(Feedback((id 2)(route 0)(contents(Message Notice()(Pp_glue((Pp_string 1)Pp_force_newline(Pp_string"     : ")(Pp_tag constr.reference(Pp_string nat))))))))
(Answer 1(ObjList()))
(Answer 1 Completed)

You can see that in this output, I get two Messages both with the same id 2, which means that they aren't distinguishable, and only one of them is the output that corresponds to the Query.

Ideally, I would expect that the Message output for the Add command would either be included in the response from the Add, or dropped entirely, or given a different id if it must be included with a later Query.

I am using SerAPI installed via opam with ocaml 4.06.0, sertop 0.4.10, and coq (also installed with opam) 8.7.2.

@cpitclaudel and @JasonGross have requested to have whole Coq document parsing. This issue is to design and discuss how such a mechanism would work.

Current status [edit: updated, see below]

SerAPI provides a parsing command that will indicate where the current sentence ends:

(P (Parse "Lemma U n : n + n = n. Proof. intros."))
(Answer P Ack)
(Answer P
 (ObjList
  ((CoqLoc
    ((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0)
     (bp 0) (ep 22))))))
(Answer P Completed)

This was meant as a proof of concept but it is useful in itself.

Proposal 1: extend to lists of positions:

A first step towards improving this would be to support a (Parse Sentence "doc").
Such command would return a list of CoqLoc objects signalling the end of each sentence. It would be up to the ide to split the doc.

If the last sentence is not a valid one, I wonder what to return. We could fail the whole parsing, just ignore it, or return the list of valid positions plus an exception.

[Edit]

Current Status

This feature is mostly implemented, StmAdd now takes a parameter indicating the number of sentences to parse, and will try to parse as many as indicated. I a parse error occurs, it will still add the number of well-parsed sentences.

To close this issue, it remains to:

• Push coq/coq#204 upstream, adapt to it.
• Be sure that IDE implementors can validate the current design.

It seems sexplib sometimes omits quotes around PCData content when the string contains no whitespace.

This became a problem for me when the string was:

(PCData ,) -- for (PCData ",")

As my s-expression parsing library of choice ( https://www.npmjs.com/package/s-expression ) seems to expect the comma to be an unquote.

Who is to blame here, if anyone? :-)

I'm not sure whether this is a coq-serapi bug as much as a Coq protocol bug, but here it is.

When I enter the following sentence in CoqIDE-8.5pl1:

Theorem test : let (x, y) = (1, 2) in x.

I get an error message, and the = sign gets highlighted as the location of the error.

Now, when I enter the same sentence in sertop, all I get is a CoqExn with the same error message, but I don't get a Message with error location.

I'm not sure where I'm supposed to get this error location from...

(Control (StmAdd () "Theorem test : let (x, y) = (1, 2) in x."))
(Answer 51 Ack)
(Answer 51(CoqExn(Stream.Error"[return_type] expected (in [constr:binder_constr])")))
(Answer 51 Completed)

Help! :-)

We'd like to do correct location reporting for UTF-8 scripts. See https://coq.inria.fr/bugs/show_bug.cgi?id=4965 for more details.

I get the following message:

+ ocamlfind ocamldep -package cmdliner -package coq.intf,coq.stm,sexplib -modules sertop/sercomp.ml > sertop/sercomp.ml.depends
ocamlfind: Package `cmdliner' not found

I can solve it by adding :$(OCAMLPATH) to the sercomp: target in the Makefile, like it is in the other targets. Any reason why it wasn't there? Any reason not to include it?

We should provide a Python binding for SerAPI as this is what many people actually use.

In principle, we should have a doc object, with add and cancel methods, as well as a coqObject one with the proper subclasses.

I am not sure what is the best way to proceed here, I guess some help from Python experts would be welcome.

SerAPI should support the async proof mode. Experimental support is already in place, however more testing is needed. Remaining tasks are:

• Teach our internal document mode of focus operations.
• Document better Coq's upstream API / Flags for async, check we are using the API correctly.
• Fix our handling of command line parameters [needs upstream help]
• Provide worker control commands in the Stm* family.

Notes will be taken in notes/async-support.md

I am using Coq 8.7.1, OCaml 4.06.0. After compiling CompCert 3.2, if I run

sertop -R lib,compcert.lib -R common,compcert.common -R x86_64,compcert.x86_64 -R x86,compcert.x86 -R backend,compcert.backend -R cfrontend,compcert.cfrontend -R driver,compcert.driver -R flocq,compcert.flocq -R exportclight,compcert.exportclight -R cparser,compcert.cparser

and then (Add () "From compcert Require Import Ordered."), an error appears:

(Feedback((id 2)(route 0)(contents(Message Error(((fname"")(line_nb 17)(bol_pos 999)(line_nb_last 17)(bol_pos_last 999)(bp 999)(ep 1058)))(Pp_box(Pp_hovbox 0)(Pp_glue((Pp_string while)(Pp_print_break 1 0)(Pp_string loading)(Pp_print_break 1 0)(Pp_string /Users/wolf/.opam/4.06.0/lib/coq/plugins/micromega/micromega_plugin.cmxs:)(Pp_print_break 1 0)(Pp_string"error loading shared library: dlopen(/Users/wolf/.opam/4.06.0/lib/coq/plugins/micromega/micromega_plugin.cmxs, 10): Symbol not found: _camlBig_int\n  Referenced from: /Users/wolf/.opam/4.06.0/lib/coq/plugins/micromega/micromega_plugin.cmxs\n  Expected in: flat namespace\n in /Users/wolf/.opam/4.06.0/lib/coq/plugins/micromega/micromega_plugin.cmxs"))))))))

This looks like a linking problem in SerAPI, as coqtop doesn't have the problem.
If I run

coqtop -R lib compcert.lib -R common compcert.common -R x86_64 compcert.x86_64 -R x86 compcert.x86 -R backend compcert.backend -R cfrontend compcert.cfrontend -R driver compcert.driver -R flocq compcert.flocq -R exportclight compcert.exportclight -R cparser compcert.cparser

Then From compcert Require Import Ordered., I got

[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file extraction_plugin.cmxs ... done]
[Loading ML file recdef_plugin.cmxs ... done]
[Loading ML file romega_plugin.cmxs ... done]
[Loading ML file r_syntax_plugin.cmxs ... done]
[Loading ML file fourier_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]

which looks fine.

Is it possible for SerAPI to expose the tokenizer of Coq? It can help a lot in understanding the Coq ASTs. Thank you so much!

Hey Emilio,

IIUC, the current design is that when sending a query the IDE immediately gets an Ack with a number. This allows it to track (potentially multiple) future responses to that query.

I wonder if we could do a bit better here. Two suggestions:

• Wouldn't it be nice if one passed an id with each query, and responses used that? This would allow IDEs to fully disconnect query sending and response processing. Concretely, I mean that one could say

  (Query 15 (((Prefix "Debug")) None PpSexp) Option)

  And get

  (Answer 15 Ack)
  (Answer 15 ...)

• Do I understand correctly that responses can come in chunks? If so, maybe we could have an extra (Answer 15 Completed) to indicate that no more output will be produced for a given query (I see there's a Completed constructor in answer_kind)? Otherwise, how does one know that all output has been received for a query?

  (It could be that I misunderstood and that in fact there's only one reply per message, in addition to the Ack)

• Finally, assuming we let the IDE pick the query ID, could we do entirely without Acks?

Clément.

I'm getting the following message on OCaml 4.02.3:

File "sertop/sertop_protocol.ml", line 336, characters 4-612:
Warning 44: this open statement shadows the value identifier || (which is later used)
File "sertop/sertop_protocol.ml", line 336, characters 4-612:
Warning 44: this open statement shadows the value identifier @@ (which is later used)
File "sertop/sertop_protocol.ml", line 1:
Error: Some fatal warnings were triggered (2 occurrences)
Command exited with code 2.

TL;DR: can we get a special ID for the root state? Currently I need to attach to state 2 when sending the first sentence (I guess this is because SerAPI sends two commands before giving me control?)

Background: When I need to Add a new sentence, I need to know the ID of the immediately preceding sentence. With the XML protocol I do an EditAt(stateid)and then I add to that same state stteid. With SerAPI, IIUC, I'll just do an Add (there won't be a stateful notion of "current tip", yay!). ((Of course I'll get an error if that state wasn't a leaf of the DAG.))

Now the question is: how do I figure out which ID to Add to? It's pretty easy to just look at the previous sentence if there is one, but for the very first sentence? I can currently get it using a synchronous (Control StmState) query, but hopefully this very notion of "current state" will go away at some point (right? I hope I'm not missing anything here).

As of today, SerAPI creates a new document by default, with standard loadpaths, libraries, etc...

This can be overridden to some point using cmdline parameters, but we would like to have proper protocol support for that, as well as for document ids and for output formats. Thus, the init call should support as parameters:

Pending

• Packages, in the jsCoq style.
• Output format the Feedback about a particular document should be sent back / extra printing / feedback channels.

Fixed by #69

• Extra Load Paths Bindings
• Set of libraries to load by default.
• Initial name [will be ignored for now, should fix #14]

Hey Emilio,

This is more of an Stm question, but here it goes :) If I understand correctly, IDEs are roughly expected to chunk up the document, and send it bit by bit using StmAdd commands.

Each such StmAdd returns a state id, which can be used to track the processing of the corresponding region.

Unlike serapi, the Stm doesn't let users pick state IDs; thus, one needs to wait for a feedback message to know which id is associated to a particular span. This would work fine if the Stm returned that ID immediately, but it seems not to; am I doing something wrong?

Practical example:

(adding-goal (Control (StmAdd 2 "Goal forall n, n + 0 = n.")))
  (Answer adding-goal Ack)
  (Answer adding-goal
          (StmInfo 3
                   (NewTip)))
  (Answer adding-goal Completed)
(infinite-loop (Control (StmAdd 3 "do 1000 (do 1000 (do 1000 idtac)).")))
  (Answer infinite-loop Ack)
  (Answer infinite-loop
          (StmInfo 4
                   (NewTip)))
  (Answer infinite-loop Completed)
(observing (Control (StmObserve 4)))
  (Answer observing Ack)
  (Feedback
   ((id
     (State 4))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 2))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents Processed)
    (route 0)))
(adding-idtac (Control (StmAdd 2 "idtac aaa.")))

That last command does not return. Is that expected? I hinted at this issue in a mailing list post, but it's not obvious that this is something that SerAPI can fix... OTOH, maybe I'm just misunderstanding something :)

Thanks for your help!

We should support LSP to some degree.

https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md

Could you explain how SerAPI handles errors, and the types of its error messages? Thanks!

Hey Emilio,

I'm trying to resurrect PeaCoq's code base, and am puzzled by how to replace the old LibAdd.

I can seem to get my plugin to start loading, by having -Q /path/to/plugin,PluginName, but unfortunately, my plugin.ml4 opens a file in the same directory, that is compiled as a .cmxs, and Coq fails to know how to load it by default.

But, using CoqIDE, I can add -I /path/to/plugin, and then everything works well.

This is minor but when you provide an invalid coq_location in myocamlbuild.ml, the error message is a bit unclear.

I wonder if there is a way for you to detect and complain that the directory does not exist.

Hi @ejgallego, I just followed the build instruction on readme, and everything worked fine until I got to the final step. When I run make, it will produce Unbound module Feedback building error. At first, I use OCaml 4.04, so I assume maybe it is a version confliction, but when I downgrade to 4.02.3 as you suggested on readme, this error was still standing there, here is the error log.

In sertop/sertop_sexp.ml, there are calls to Conv.Exn_converter.add, which doesn't seem to exist in recent versions of sexplib. In OPAM, OCaml 4.03 and 4.04 use sexplib 113.33.00. So SerAPI won't build with those versions of OCaml in OPAM.

Instead, sexplib now has add_auto and add_slow.

If I add a small example proof like this:

(Add () "Example test_orb1: (orb true false) = true. Proof. simpl. reflexivity. Qed.")
(Query () (Ast 4))

at the beginning of a sertop session, I see Added responses with IDs 2-6. So ID 2 is the definition, 4 is the simpl tactic, etc. I would expect to be able to use the Ast query command to see which tactics were used. However, if I issue this command:

I see this result:

(Answer 1 Ack)
(Answer 1(ObjList((CoqAst((((fname"")(line_nb 2)(bol_pos 44)(line_nb_last 2)(bol_pos_last 44)(bp 51)(ep 57)))(VernacExtend(VernacSolve 0)("XXX Raw GenARG""XXX Raw GenARG""XXX Raw GenARG""XXX Raw GenARG")))))))
(Answer 1 Completed)

In place of "XXX Raw GenARG", I would like to see something about the simpl tactic somewhere in the result. Is that something that could be fixed? Or is there an alternative way to access information about tactics used in a proof?

In the "issues with serializing to sexps" family, I've just run into the following problem: many lisps do not distinguish between '() and nil, and thus serialize () to nil.

For example in common lisp:

[7]> (format t "~a" '())
NIL

And in Emacs Lisp:

(format "%S" `()) ;; => nil 

Could we add an option to SerAPI to accept nil as a synonym for ()? Currently I get this:

(97 (Query (() None PpStr) Goals))
  (Answer 97 Ack)
  (Answer 97
          (ObjList nil))
(97 (Query (nil None PpStr) Goals))
  (SexpError
   (Sexplib\.Conv\.Of_sexp_error
    (Failure "Sertop_protocol.cmd_of_sexp: unexpected sum tag")
    (97
     (Query
      (nil None PpStr)
      Goals))))

In the meantime, I'll look at whether I can make the Emacs lisp printer produce '().

Looking at Emacs' source code, there doesn't seem to be a way to make it print () instead of nil, but it's pretty easy to write a decent workaround, so I'd call this low priority.

https://github.com/google/kythe is an interesting framework we could make our tool talk to.

Hey Emilio,

I've just finished a tiny POC for getting Emacs to talk to SerAPI! I was hoping that this experiment could help clarify what options we have to port Proof General to support async processing, and more generally the STM. The whole experience was very nice, btw; congrats on SerAPI!

Here are a few questions that popped up while working on the prototype. If you have time, your opinion on these would be most welcome :)

• In a previous thread, you wrote:

  Regarding the sockets part, by default Coq is fully synchronous and will emit all the feedback messages before returning from the call. Feedback.set_feeder is called, note however than a ML pluging/toplevel may chose to queue the messages.

  Am I right to think that SerAPI will evolve to fully support asynchronous processing? In that case, am I right to think that some feedback messages will come independently of an Observe query? (currently all feedback messages are between an Ack and a Completed, it seems)

• Are there things in the current Coqtop that you definitely don't want in SerAPI?

• Will SerAPI support _CoqProject files, or something similar?

• How can I pass Coq flags (essentially, the contents of a _CoqProject file) to SerAPI?

• Will SerAPI be compatible with 8.5, or will it only start working with trunk/8.6?

• Is there a chance that SerAPI will be merged into Coq trunk? If not, how hard will it be to run it on Windows? (Will Coq itself be distributed using Opam on Windows? If not, can we add SerAPI to the Windows installer?). My concern is to not require too much from people installing PG.

• Closely related: can we distribute a pre-built copy of SerAPI with Proof General, or do users need to build it locally? Does building locally require Coq's sources? What about on Windows?

Thanks a lot for your help :) I've also posted a mini-CEP to coqdev regarding EditAt.

Cheers,
Clément.

Looking at the code and at Coq pr/204 I think I should clarify.
Today Stm.add is able to add 1 and only 1 sentence, even you pass to it a stream.
Today the grammar of Coq has no entry for a document, so you have to iterate parsing a sentence.

The big problem is that parsing is context dependent. If a sentence is Notation then the following sentence needs the parser to be updated (by executing, at least partially the Notation sentence).
The Stm uses a classification of commands to know which ones alter the parser (labelled as VtNow).

In my, still empty, CEP1 I'd like to propose a document format where phrases altering the parser are
all in the header (Reseve Notation, Import, ...).

JFTR, Isabelle has the (frankly ugly) restriction that terms are written between quotes, as "f x + 3".
These /strings/ can be parsed later on, so the document structure can be fully parsed without altering the parser (the global structure is fixed).

The title says it all. This is a first step towards becoming a Jupyter kernel. The basic resources are:

• https://github.com/akabe/ocaml-jupyter
• https://github.com/andrewray/iocaml
• http://jupyter-client.readthedocs.io/en/latest/kernels.html
• https://github.com/dsblank/simple_kernel

Hi Emilio,

Your repository does not currently contain licensing information.
I've had a look at source files which contain copyright information but no licensing information either.
It would be good if you could add a license to your project, especially as other open source projects (such as @Ptival's PeaCoq) depends already on it.
It will also help for future packaging of SerAPI in Opam, nixpkgs and elsewhere.

Thanks!