`nil` vs `()` about coq-serapi HOT 4 CLOSED

Indeed, this is handled by Sexplib, need to investigate more.

from coq-serapi.

I'm much afraid that Sexplib parser won't be easy to modify to support this use case. I'm sorry.

I propose to tag wontfix for now and try to workaround this bug.

from coq-serapi.

Sounds good. In fact, I'd say we can close this. Here's a small function that will do the trick:

(defun prin1-to-sexp (val)
  "Convert VAL to a sexp.
Crucially, renders nil as (), not nil."
  (if (listp val)
      (concat "(" (mapconcat #'prin1-to-sexp val " ") ")")
    (prin1-to-string val)))

It breaks if passed an improper list (such as (1 . 2)), but that would have confused the sertop side already :)

from coq-serapi.

Cool, thanks, even if it's a pity to have this minor difference.

Note that this could still be fixed in the future by rolling out our own parser once the whole thing is more stable, so feel free to reopen if needed.

For reference, here are Sexplib:

• parser: https://github.com/janestreet/sexplib/blob/master/src/parser.mly
• pretty printer: https://github.com/janestreet/sexplib/blob/master/src/pre_sexp.ml#L174

the last one is interesting as it will determine the escaping done by sertop's printing. I'm not opposed to rolling our own versions if we have good reasons.

from coq-serapi.