[sercomp] Print mode strips out comments from .v

[artagnon]

sercomp --mode=print <filename> produces a .v without the comments in the original.

[ejgallego]

Indeed, print mode relies on Coq printer; this means that for example the code may not parse back and formatting will almost likely be different.

We could try to preserve comments tho as Coq does indeed store a position-based comment table on the lexer, I'm not sure how accurate this will be but it should be better than nothing.

[ejgallego]

#205 made some progress towards this, however more work is needed, in particular as to integrate with Coq's special printer for comments.

When a comment does happen in the middle of an expression, the printer needs to be aware of the comments; Coq's printer will already try to do that if Flags.beautify is on; however there is an assymetry on the parse/print path w.r.t. to slices, unless you do everything in the same Add call (as coqc would kinda do)

So indeed, this has a change to work in sercomp .

There are several approaches to handle this, for now I think this will have to wait a bit more, tho we could experiment with the beautify flag.

[ejgallego]

In the coq-lsp model, we support hybrid documents and the workflow for clients should not have this problem.