Commas in s-expressions: string or unquote? about coq-serapi

[cpitclaudel]

Hmm. I think only quote, backslash, comma, backtick, and #'.

[ejgallego]

Indeed, sexplib serializes data in a particular way. The base data type, quoting from: https://github.com/janestreet/sexplib/blob/master/src/type.ml is

type t = Atom of string | List of t list

Thus, the choice is really what to do with strings!

For that, sexplib uses the code at
https://github.com/janestreet/sexplib/blob/master/src/pre_sexp.ml#L22
to guess when it should add quotes, as to make the output more "sexpy"-friendly.

Unfortunately the comma is not there, so I wonder what would the best solution be on our part; I am not an expert on S-expressions myself, but I will definitively try to bring this issue with sexplib developers.

[ejgallego]

@cpitclaudel , do you know if this comma thing will create problems in emacs?

[ejgallego]

Ok, a53964e should provide a more sensible escaping if --custom-escape is passed: we now treat every Atom as a UTF-8 string. Also, naked commas should not be produced.

Would you mind testing the comma part? Thanks

[cpitclaudel]

I think it will be an issue in Emacs as well, yes; , is taken by the lisp reader to be a reader macro expanding to unquote.

Then again, it shouldn't be very hard to write a separate parser in list; but it would be nice to use the off-the-shelf one. The surprising thing is that Sexplib doesn't distinguish between symbols and strings.

[ejgallego]

@cpitclaudel , any other special character we should keep in mind?

--custom-escape should solve the comma issue. I'm happy having our own printer.

Indeed sexplib makes the choice of "symbols == strings".

[ejgallego]

Cool thanks, I'm gonna ask upstream about the quoting. It seems that double quote and backslash are OK.

The rest don't seem OK, I'll fix them in --custom-escape, while I get an answer from sexplib upstream.

Comma, quote, and backtick should be escaped only if at the beginning of a symbol, right?
What about #'?

I couldn't find an elisp grammar/lexical conventions.

[ejgallego]

How to test sexplib quoting

Install utop and sexplib using OPAM, then:

$ utop 
# #require "sexplib";;
# let p x = Sexplib.Sexp.(Format.(printf "@[%a@]@\n" pp (Atom x)));;
# p ",";;

[cpitclaudel]

Comma, quote, and backtick should be escaped only if at the beginning of a symbol, right?
What about #'?

No, anywhere in a symbol. Same for #' (and there's actually #< and ## as well apparently, though just escaping # would fix that too.

[cpitclaudel]

I wonder why sexplib doesn't simply use quotes for everything that is a string on the OCaml side, and symbols for the rest.

[ejgallego]

What do you mean by "everything that is a string on the OCaml side" ?

For sexplib, everything is a string, so it would then print ("Control" ("StmAdd" () "Command")), etc...

[cpitclaudel]

Is Control a string? I thought it was the name of a constructor.

[ejgallego]

At the sexp-level, Control is indeed a string. Recall the sexp syntax:

type t = Atom of string | List of t list

so sexplib expressions are just possibly nested lists of strings.

[cpitclaudel]

Ah, right.

Maybe it would be simpler to just quote everything?

[ejgallego]

Maybe we should quote everything, would that be a problem for emacs?

The new printer has been committed, I will close this once I add the proper documentation.

[cpitclaudel]

Quoting everything would be totally fine :)

[Ptival]

I no longer have a problem with (PCData ,), but I have a problem with (PCData fold').

[ejgallego]

@Ptival understood, will fix.

[riswords]

Can square braces also be quoted? In (Query () (Vernac "Print nat.")) for example, I see (Pp_string ]) which causes an error for the emacs parser.

[ejgallego]

@riswords , sure, I'll take of it.

[ejgallego]

Should be better now, note that we currently depend on coq/coq#822 due to them having broke its linking spec.

[ejgallego]

See e2982c1 if you need to tweak escaping more, and of course submit a pull request!

[riswords]

Great, thank you!

[ejgallego]

NP, let me know if you have any additional trouble, note also that we have a gitter channel that may work well for concrete questions.

[Ptival]

Ha, just got bit by (PCData [) and (PCData ]) myself!

[ejgallego]

Yup at some point we'll make the custom quoting the default.